Hulp
Deze pagina aan uw boek toevoegen
Boek weergeven (27 pagina's)
Pagina's suggererenBeweren en bewijzen/de zuilen/Zekerheid/5. Natuurlijke deductie/P of niet P
| literatuur
... |
Dat is Latijn voor: „Een derde is niet gegeven.” In andere woorden: „Iets is waar of niet waar. Een derde mogelijkheid bestaat niet.”
Dit is zowaar het moeilijkste van de kleine bewijzen.
Inhoud
Hier enige mogelijke bewijzen met uitleg
We willen „uit het niets”, d.w.z. zonder aannames, P ∨ ¬P bewijzen. Neem papier en pen of start Coq en werk de volgende stappen begrijpend door. Het heeft geen zin de uitleg hieronder te lezen zonder tegelijk het bewijs op te schrijven.
| ⊢ P ∨ ¬P |
Men heeft de neiging om met ∨I te beginnen, tenslotte komt in de formule een ∨ voor. Maar dat zou in dit geval een verkeerde afslag zijn. P noch ¬P zijn altijd onwaar, daarom mogen we in het bewijs niet op één concentreren en de andere weglaten. De bewijsstrategie waarschuwt voor deze fout.
Als we niets beters kunnen bedenken, raadt de bewijsstrategie een bewijs uit het ongerijmde aan: ¬E*. We nemen aan dat ¬(P ∨ ¬P) geldt en proberen daaruit een tegenspraak te construeren. Nu moeten we een creatieve keuze maken voor ... (merkop dat hier een P staat in de ¬E*-regel, maar dit is een andere P!)
| ¬(P ∨ ¬P) ⊢ ... | ¬(P ∨ ¬P) ⊢ ¬... | ¬E* |
| ⊢ P ∨ ¬P | ||
We mogen invullen wat we willen, bijvoorbeeld A → B, maar als we een tegenspraak willen construeren, vullen we beter iets in wat met de formule te maken heeft waaruit we de tegenspraak willen construeren. Bijvoorbeeld P. Of juist ¬P. Of de oorspronkelijke formule P ∨ ¬P. Of iets nog ingewikkelders. Hier helpt alleen puzzelen, en als we al puzzelen, beginnen we liever eenvoudig.
De eenvoudigste mogelijkheid
In een college hadden we P ingevuld, maar daarmee kwamen we na een tijd niet verder.
| ¬(P ∨ ¬P) ⊢ P | ¬(P ∨ ¬P) ⊢ ¬P | ¬E* |
| ⊢ ¬(P ∨ ¬P) | ||
Was dit een verkeerde afslag? Ja en nee. Als je de twee bewijzen hieronder begrijpt, zal je zien dat ook dit begin tot een bewijs uitgebreid kan worden, zij het met een onnodig hoge boom. Een verkeerde afslag kan soms, maar niet altijd, na een omweg alsnog tot het doel leiden.
De op een na eenvoudigste mogelijkheid
We proberen ¬P, de op één na eenvoudigste mogelijkheid. Dat betekent dat we nu uit ¬(P ∨ ¬P) twee dingen moeten bewijzen: enerzijds ¬P en anderzijds ¬¬P.
| ¬(P ∨ ¬P) ⊢ ¬P | ¬(P ∨ ¬P) ⊢ ¬¬P | ¬E* |
| ⊢ ¬(P ∨ ¬P) | ||
In beide gevallen begint de te bewijzen formule met een ¬, en in beide gevallen kunnen we de ¬I-regel toepassen: om te bewijzen dat iets niet het geval is, nemen we aan dat het wel het geval is en construeren daaruit een tegenspraak.
Leidt ¬(P ∨ ¬P) samen met P tot een tegenspraak? Ja: Als P waar is, dan ook „P of iets anders”, bv. P ∨ ¬P. En dat hebben we nu juist als onwaar aangenomen! We vullen dus P ∨ ¬P in. Het enige wat we in deze tak nu nog moeten bewijzen is dat P ∨ ¬P uit onze aannames volgt. We hebben P, dus lukt dat met ∨I.
|
¬(P ∨ ¬P) ⊢ ¬¬P | ¬E* | ||||||||||||||
| ⊢ ¬(P ∨ ¬P) | ||||||||||||||||
De tweede tak loopt volgens hetzelfde stramien.
De oorspronkelijke formule
Wat als we de oorspronkelijke formule P ∨ ¬P invullen? De rechter tak sluit dan meteen:
| ¬(P ∨ ¬P) ⊢ P ∨ ¬P |
| ¬E* | |||
| ⊢ P ∨ ¬P | |||||
Met de open tak zijn we terug bij af, maar we mogen nu wel ¬(P ∨ ¬P) als aanname gebruiken. Marc Schoolderman kwam erop dat men het alternatief ¬P kan bewijzen op de hierboven aangegeven manier, met een ∨I als tussenstap:
|
| 7: ¬E* | ||||||||||||||||||||
| ⊢ P ∨ ¬P | ||||||||||||||||||||||
De nummers in deze bewijsboom komen overeen met de nummers in het voorbeeld van de Fitch-stijl. Deze bewijsboom is dus wat hoger dan de vorige, maar minder breed.
Waarom is dit bewijs zo moeilijk?
Alle logici en wiskundigen zijn het eens over de regels voor natuurlijke deductie m.u.v. ¬E*. De logica die zonder deze regel uitkomt, wordt ook constructieve of intuïtionistische logica genoemd. In deze logica geldt het tertium non datur niet. Er geldt evenmin dat ¬¬P gelijk is aan P. De oosterse filosofie vindt overigens ook dat er veel meer is dan P en ¬P.
De westerse „klassieke” logica en daarmee het merendeel van de wiskundigen en logici neemt het tertium non datur daarentegen wél als waar aan. Zij breiden het stel van deductieregels waar iedereen het over eens is uit. Dit kan op verschillende manieren.
- Door P∨¬P als axioma aan te nemen. (Een axioma is iets dat een wiskundige voor waar aanneemt zonder het te bewijzen.)
- Door deze regel toe te voegen aan het systeem van natuurlijke deductie:
| Σ ⊢ ¬¬α | ¬¬E |
| Σ ⊢ α |
- Door de ¬E*-regel toe te voegen zo als Van Benthem het doet. Als je goed kijkt, is dit een combinatie van ¬I en ¬¬E.
Ons bewijs gaat dus ten eerste over dingen die sommige logici en filosofen niet als waar accepteren. Ten tweede wordt hier bewezen dat één mogelijke uitbreiding (¬E*) ten minste even krachtig is als een andere (het tertium non datur als axioma). Redeneren op het scherp van de snede op de uiterste rand van de logica. Dit soort bewijzen kunnen erg moeilijk zijn.
Hoe gaan we hiermee om in deze cursus?
Zo als uitgelegd in 5. Natuurlijke deductie en in de bewijsstrategie moet men in sommige bewijzen een gevalsonderscheiding over P en ¬P maken. Als 1e tak van de ∨-eliminatieregel moet je dan P∨¬P bewijzen. In tentamens en het werkstuk vinden we het goed als je daarboven een streep trekt met de vermelding „axioma”.
Het Coq-interface voor deze cursus (Over het gebruik van Coq) heeft dit axioma ingebouwd onder zijn Engelse afkorting LEM (law of excluded middle).
Zijn er meer zulke moeilijke bewijzen?
Zeker. Maar zolang je correctheidsstellingen over fysiek bestaande dingen bewijst, zul je dit probleem niet tegen komen. De natuur zorgt ervoor dat je deze uithoeken van de logica niet opzoekt.
Bewijzen van correctheidsstellingen kunnen ook moeilijk zijn, maar dan omdat de stelling complex en het bewijs omvangrijk is, niet omdat het zulke artistiek met dubbele negaties vergt. Dit zijn bewijzen waar een tool als Coq of PVS echt helpt: ze bewaren je voor fouten bij de manipulatie van veel grote formules.
