Eliminatie versus introductie

Stel je wilt met natuurlijke deductie bewijzen dat

EX x. P(x) \/ Q(x) ("op een dag sneeuwt het of staat er een regenboog")

een logisch gevolg is van

(EX x. P(x)) \/ (EX x. Q(x)) ("op een dag sneeuwt het of op een, mogelijk andere, dag staat er een regenboog, al weet ik niet wat het wordt").

Je werkt van beneden naar boven. Het lijkt voor de hand te liggen te beginnen met EX-introductie. Dan moet je vervolgens P(t)\/Q(t) bewijzen. Voor de hand te liggen lijkt nu \/-introductie. En dan loop je vast.

Als je meedenkt wat je aan het doen bent, is dat ook logisch: om EX-introductie toe te kunnen passen moet je een speciaal geval noemen. Welke precieze dag bedoel je? Dis is dus nog niet bekend.

Begin niet met het schijnbaar meest voor de hand liggende; begin met een van de andere regels die passen. In dit geval is \/-ELIMINATIE de goede kandidaat: om de \/ uit de aanname (EXISTS x. P(x)) \/ (EXISTS x. Q(x)) kwijt te raken. Je levert daarmee twee bewijzen, een voor het geval van sneeuw, een voor het geval van de regenboog. Daarmee is duidelijk wat je voor alpha, phi en psi moet invullen.

Vervolgens gebruik je in beide takken de EXISTS-eliminatie. Daarmee krijg je namen voor de twee mogelijke dagen.

De rest loopt dan als een trein.

Conclusie: het is altijd goed om bij elke stap te inventariseren welke regels überhaupt in aanmerking komen.

Meestal is het goed, \/- en EXISTS-eliminatie zo vroeg mogelijk toe te passen. Bij \/ en FORALL is het precies omgekeerd! Wat is hier aan de hand?

Existentieel versus universeel

In twee gevallen gooit men informatie weg die men niet nodig heeft.

EX-introductie laat in het midden over welk specifiek geval precies men iets weet. Als je iets hebt bewezen voor een zeker geval, bv. voor 2*y-4 in:

2*y-4 > 0

dan heb je ook bewezen dat er zo'n ding bestaat:

EX x. x>0

AL-eliminatie gaat over van universele kennis op een enkel specifiek gevalletje. Als je bewezen hebt:

AL x. P(x)

dan mag je voor x elk speciaal geval invullen dat je nodig hebt:

P(2*y-4)

De toepassing van beide regels is technisch niet moeilijk (er staan geen restricties in de "kleine lettertjes"). Maar het heeft pas zin ze toe te passen als het nodige specifiek geval al bekend is. Als je deze regels te vroeg toepast, loop je vast omdat je de nodige kennis nog niet hebt.

In de complementaire gevallen werkt men met onvolledige informatie.

De essentie van deze regels zit in de kleine lettertjes. Deze regels worden vaak verkeerd toegepast. Jape controleert goed of je je houdt aan de kleine lettertjes en tikt je genadeloos op de vingers.

EX-eliminatie. De regel met de bijbehorende kleine lettertjes is zo gemaakt dat men voor dat onbekende geval een "onbesproken" naam krijgt, die nooit gelijk kan zijn aan iets anders. "Er is iets, laten we dat dan x noemen" - dat mag je alleen doen als nergens anders in je redenering een x voorkomt, want anders zou je per ongeluk twee dingen gelijk maken die waarschijnlijk niet gelijk zijn.

ALL-introductie is daarmee verwant. Ik moet iets bewijzen voor alle x. De spelregel is dan dat ik het moet bewijzen voor een "onbesproken" variabele, die nergens anders voorkomt - een variabele over die men NIETS WEET. Als ik het daarvoor kan bewijzen, zal het voor alles gelden.

Het is daarom meestal een goed idee, EX-el. en AL-intr. zo vroeg mogelijk toe te passen. In de rest van het bewijs heb je dan een paar quantoren minder, in plaats daarvan heb je een aantal verschillende variabelen waarover je verder niets weet maar die je gewoon mag gebruiken.

Voorbeeld

{AL x. P(x)->Q(x), EX x. P(x)} |- EX x. Q(x)

Verzeker jezelf dat je voor zulke stellingen ook voorbeelden in natuurlijke taal kunt bedenken! Een interpretatie in de echte wereld helpt je altijd, redeneerfouten te vorkomen.

"Elke Nijmegenaar is dol op voetbal. Er bestaat een Nijmegenaar. Een logisch gevolg hiervan is dat er iemand bestaat die dol op voetbal is."

In de aannames staat: "Er bestaat een Nijmegenaar." De EX-eliminatieregel komt neer op: "nemen we aan dat deze Nijmegenaar Pietje heet". Je moet dan bewijzen dat er iemand is die dol op voetbal is. Dat zal dan wel Pietje zijn. (Schrijf het bewijs nu onmiddellijk uit met EX-el. als eerste stap, als je dit niet begrijpt!)

Als je helemaal aan het begin EX-intr. probeert, ben je daarmee te vroeg. Je moet bewijzen dat er iemand bestaat die dol op voetbal is. Laat dat dan Jantje zijn en probeer te bewijzen dat Jantje dol op voetbal is. - Maar Jantje is misschien helemaal geen Nijmegenaar en je hebt niets aan de andere aanname.