Beweren en bewijzen/de zuilen/Formalisering/5. Systematisch vertalen

literatuur ...

Wie slaapt, snurkt

We verkennen de samenhang tussen een stukje natuurlijke taal - in dit geval het woord je "wie" - en onze formele taal, predikaatlogica, aan de hand van een zeer eenvoudig voorbeeld.

Verkenning

Wie slaapt, snurkt.
Hoe pakken we zoiets aan? Stel we hebben predicaten slaapt en snurkt in ons domeinmodel, dan zal het toch iets moeten zijn van:
	slaapt ...		snurkt ...
Om wie gaat het? In elk geval in beide gevallen om dezelfde persoon, laten we ze x noemen:
	slaapt x		snurkt x
Hoe moeten we de twee delen verbinden? Er zijn niet zo veel mogelijkheden: ∧ ∨ → x slaapt en snurkt? x slaapt of snurkt? Nee: Als x slaapt, dan snurkt x.
	slaapt x	→	snurkt x
Maar x is nog niet gedefinieerd? Er zijn niet zo veel mogelijkheden om een naam te definieren. Is het een parameter? Nee. Ook geen constante. Het gaat om een universele uitspraak:
∀ x:M,	slaapt x	→	snurkt x

Dit kunnen we beter systematisch aanpakken:

Systematisch

We kijken aan de hand van hetzelfde zeer eenvoudige voorbeeld hoe we zoiets systematisch kunnen vertalen.

Wie slaapt, snurkt.
Wordt hier gepraat over één bepaald persoon? Of over een zeker (maar niet bekend) persoon? Nee, er wordt over iedereen gepraat. Het is een universele bewering.
(kwantor)formule
∀ x:M,	(	Als x slaapt, snurkt x. implicatie ( x slaapt. term slaapt x ) → ( x snurkt. term snurkt x )	)

Dus de uiteindelijke formule wordt:

∀ x:M, ( ( slaapt x ) → ( snurkt x ) )

Door bij elk nieuw blok haakjes te zetten, weten we zeker dat alles goed afgebakend is. Helaas levert dat vaak meer haakjes op dan noodzakelijk volgens de grammatica. In dit geval kunnen we deze formule reduceren naar de equivalente formule:

∀ x:M, slaapt x  → snurkt x

Algoritme

• Organisatiestap: Teken een rechthoek, waarbinnen je alles uitvoert.

1. Verduidelijken.
   • Verander de zin op zo'n manier dat het duidelijker wordt wat de (logische) structuur van de zin eigenlijk is, maar natuurlijk zonder de betekenis van de zin te veranderen. Voorbeelden:
     • Als je denkt dat de zin een negatie is, maak er dan van: „Het is niet het geval dat ...”
     • Als je denkt dat de zin een kwantorformule is, maak er dan van: „Voor alle ... geldt: ...” of „Er bestaat een ... waarvan geldt: ...”
     • Een disjunctie kun je ook opschrijven als: „Minstens één van de volgende eigenschappen is waar: 1. ...; 2. ...”
2. Kies één operator en vertaal die naar een formule.
   • Schrijf ook op welke operator je nu aan het vertalen bent in de terminologie van de grammatica, dus (kwantor)formule, conjunctie, negatie, negatief, term etc.
3. Teken tussen de haakjes een nieuwe rechthoek, schrijf daar bovenin nieuwe hoofzinnen en pas op die hoofdzinnen nog eens dit algoritme toe.
4. Na afloop schrijf je de hele formule nog eens op, maar nu zonder overbodige haakjes.

Wiens vader iedereens vader is, die heeft elke man tot broer.

We oefenen dit algoritme op een complex voorbeeld.

Versie op 1 regel, verlangt een breed scherm

Wiens vader iedereens vader is, die heeft elke man tot broer.
(kwantor)formule
∀ x:M,	(	Als de vader van x iedereens vader is, dan is elke man een broer van x. implicatie ( De vader van x is iedereens vader. (kwantor)formule ∀ v:M, ( Als v de vader van x is, dan is v iedereens vader implicatie ( v is de vader van x. term isVaderVan v x ) → ( v is iedereens vader (kwantor)formule ∀ i:M, ( v is de vader van i. term isVaderVan v i ) ) ) ) → ( Elke man is een broer van x. (kwantor)formule ∀ m:M, ( Als m een man is, dan is m een broer van x. implicatie ( m is een man. term isMan m ) → ( m is een broer van x. term isBroerVan m x ) ) )	)

Versie voor kleinere schermen

Wiens vader iedereens vader is, die heeft elke man tot broer.
(kwantor)formule
∀ x:M,	(	Als de vader van x iedereens vader is, dan is elke man een broer van x. implicatie ( De vader van x is iedereens vader. (kwantor)formule ∀ v:M, ( Als v de vader van x is, dan is v iedereens vader implicatie ( v is de vader van x. term isVaderVan v x ) → ( v is iedereens vader (kwantor)formule ∀ i:M, ( v is de vader van i. term isVaderVan v i ) ) ) ) → ( Elke man is een broer van x. (kwantor)formule ∀ m:M, ( Als m een man is, dan is m een broer van x. implicatie ( m is een man. term isMan m ) → ( m is een broer van x. term isBroerVan m x ) ) )	)