Bewijzen en semantische tableaus

1. Wat een bewijs is

Een argument is de bewering dat een conclusie volgt uit bepaalde premissen. Een bewijs is wat die bewering beslecht: een eindig, controleerbaar geheel dat iedereen regel voor regel kan nalezen en beamen, zonder u op uw woord te hoeven geloven. Het punt van een bewijs is niet dat het overtuigt - dat doet een goede toespraak ook - maar dat elke stap erin niet anders had kunnen uitvallen.

Dat is een strengere eis dan het klinkt. «Het regent, dus de grond is nat» is een redelijke uitspraak, maar ze leunt op wat u over regen en grond weet. De formele logica laat dat weg en stelt een nauwere vraag: is er, louter gelet op de vorm van de zinnen, enige manier waarop de premissen waar en de conclusie onwaar zijn? Is die er niet, dan is het argument geldig, en het bewijs is het verslag van waarom die er niet is.

Deze gids gaat over één manier om dat verslag te maken: de methode van de semantische tableaus, ook wel waarheidsbomen genoemd. Het is de methode die deze site gebruikt zodra u een argument in de rekenmachine typt, en wie haar één keer heeft gevolgd, kan met niets dan een pen een argument op papier controleren.

2. Geldig, en hoe u dat zou weten

Schrijf een argument met een gevolgtrekkingsteken: de premissen links, de conclusie rechts. De bewering p → q, ¬q ⊨ ¬p zegt dat uit een implicatie en de ontkenning van haar consequens de ontkenning van haar antecedens volgt. Het gevolgtrekkingsteken is geen extra connectief. Het is een bewering over de formules aan weerszijden, en die is juist of onjuist.

De definitie van geldigheid wijst meteen op een manier om haar te toetsen: loop elke toekenning van waar en onwaar aan de variabelen af en kijk of er één is die alle premissen waar en de conclusie onwaar maakt. Dat is wat een waarheidstabel doet, en bij twee of drie variabelen voldoet dat prima. Het probleem is dat de tabel groeit als 2ⁿ. Tien variabelen vragen duizend rijen, twintig een miljoen, en de tabel zegt niets over welke rijen ertoe deden.

Een tableau valt dezelfde vraag van de andere kant aan. In plaats van elke mogelijkheid op te sommen en naar een slechte te zoeken, neemt het aan dat er een slechte bestaat en probeert die te bouwen. Stort die poging op elke route die zij kon nemen in tegenspraak in elkaar, dan bestaat zo'n toekenning niet en is het argument geldig. Slaagt de poging, dan is wat zij bouwde een tegenvoorbeeld dat u rechtstreeks kunt aflezen.

3. De tableaumethode

Een tableau is een boom van getekende formules. Elke regel is een formule met een T of een F ervoor, en het teken zegt wat de tak over die formule aanneemt - niet wat haar waarheidswaarde is, maar wat die zou moeten zijn wil het argument falen. De hele methode bestaat uit vier stappen:

1. Schrijf elke premisse met een T. U veronderstelt dat alle premissen van het argument gelden.
2. Schrijf de conclusie met een F. U veronderstelt dat zij tóch faalt - dat is de aanname die u wilt weerleggen.
3. Neem een regel die nog geen atoom is en pas de regel voor haar hoofdconnectief en teken toe; wat die regel oplevert komt achter aan elke tak die er doorheen loopt.
4. Sluit een tak zodra hij zowel T A als F A voor dezelfde formule A bevat. Stop wanneer elke tak gesloten is, of wanneer er geen regel meer te ontleden valt.

Niets in die lus vraagt vernuft of een keuze van strategie. Bij elke regel hoort precies één regel, en ze in welke volgorde dan ook toepassen geeft hetzelfde oordeel - daarom kan een machine het doen, en daarom mag u de uitkomst vertrouwen als zij het doet.

4. De regels

Er is één regel per connectief per teken - tien in totaal. Ze vallen in twee soorten uiteen, en het verschil tussen die soorten is de hele reden dat een tableau een boom is en geen lijst. Een α-regel zegt dat meerdere dingen samen moeten gelden en stapelt haar resultaten de tak af. Een β-regel zegt dat één van twee dingen moet gelden, splitst de tak dus in tweeën en laat elk geval zijn eigen weg gaan.

Elke regel is niet meer dan de waarheidsvoorwaarde van haar connectief, achterstevoren gelezen. Een conjunctie is alleen waar als beide zijden dat zijn, dus stapelt T (A ∧ B) zowel T A als T B. Een conjunctie is onwaar als minstens één zijde dat is, maar de formule zegt niet welke, dus moet F (A ∧ B) beide proberen: zij splitst. Dezelfde asymmetrie loopt andersom bij de disjunctie, en een onware implicatie betekent dat het antecedens gold en het consequens faalde - het ene geval waarin een implicatie breekt.

Let op wat de regels nooit doen: ze verzinnen nooit een formule. Alles wat een regel oplevert is een stuk van de regel waaruit zij kwam. Die eigenschap - de deelformule-eigenschap - maakt de methode eindig, en daar komen we hieronder op terug.

5. Een tak sluiten

Een tak is één redenering: lees van de wortel tot een blad en u hebt één volledige verzameling aannames. Een tak sluit wanneer die aannames elkaar regelrecht tegenspreken, dat wil zeggen wanneer hij zowel T A als F A voor één en dezelfde formule draagt. Hoe ingewikkeld A is of hoe ver de twee regels uit elkaar staan doet er niet toe - vraagt een tak dat een formule tegelijk waar en onwaar is, dan voldoet niets eraan.

Markeer een gesloten tak met ×, noem de twee regels die hem sloten, en werk er niet verder aan. Uit een aanname die al onmogelijk was valt niets meer te leren.

Sluit elke tak, dan is het tableau gesloten, en dat is het bewijs. Het laat zien dat de veronderstelling waarmee u begon - alle premissen waar, conclusie onwaar - op elke route die zij kon nemen tot tegenspraak leidt. Omdat er geen route overbleef, bestaat zo'n toekenning niet en is het argument geldig. Dit is een bewijs uit het ongerijmde, zo uitgelegd dat geen geval kan worden gemist.

6. Een bewijs, regel voor regel

Neem modus tollens: p → q, ¬q ⊨ ¬p. Regels 1 en 2 zijn de premissen, waar verondersteld. Regel 3 is de conclusie, onwaar verondersteld - en omdat de conclusie ¬p is, betekent haar onwaar veronderstellen p waar veronderstellen, wat regel 5 vastlegt. Regel 4 komt van de negatieregel toegepast op regel 2: is ¬q waar, dan is q onwaar. De implicatie op regel 1 is de enige regel die nog een connectief heeft, en het is een β-regel, dus vertakt de boom:

De linkertak veronderstelt dat de implicatie gold omdat haar antecedens faalde - maar regel 5 heeft p al waar, dus spreekt de tak zichzelf tegen en sluit. De rechtertak veronderstelt dat zij gold omdat haar consequens waar was - maar regel 4 heeft q al onwaar, dus sluit hij ook.

Beide takken sloten, dus is er geen manier om p → q en ¬q waar te hebben met ¬p onwaar. Het argument is geldig, en de boom is de reden. Merk op dat het bewijs regen noch grond noemt, noch waar p en q voor staan. Dat was niet nodig.

7. Wanneer een tak open blijft

Niet elk argument is geldig, en hier verdient de methode haar plaats. Bewerkt u een tak tot niets erop verder ontleed kan worden - er blijven alleen atomen en ontkende atomen over - en is hij nog steeds niet gesloten, dan is die tak verzadigd en open. Hij is niet ongesloten gebleven doordat u te vroeg stopte. Er valt niets meer te proberen.

Een open tak is meer dan het oordeel «ongeldig». Lees de tekens van zijn atomen af en u hebt een toekenning: elk atoom met een T is waar, elk atoom met een F is onwaar. Die toekenning maakt elke premisse waar en de conclusie onwaar, en dat is precies wat een tegenvoorbeeld is. Logici noemen het een tegenmodel, en het is een concreet antwoord op «waarom niet?» in plaats van een weigering.

Het bevestigen van het consequens, p → q, q ⊨ p, is het standaardgeval. Het tableau ervan laat een tak open met p onwaar en q waar - een situatie waarin de implicatie geldt en haar consequens geldt, en het antecedens toch niet. Die ene toekenning weerlegt het argument in haar eentje.

8. Waarom het altijd eindigt

Elke regel vervangt een formule door haar eigen deelformules, en elke deelformule is strikt korter dan de formule waaruit zij kwam. Geen enkele tak kan dus eeuwig groeien: elke stap daalt een eindige ladder van stukken van het oorspronkelijke argument af, en die ladder heeft een bodem. Uiteindelijk is elke regel op een tak een atoom of de ontkenning daarvan, en valt er niets meer te doen.

Dat is een echte garantie, geen hoop. Het betekent dat de methode een beslissingsprocedure voor de propositielogica is: laat haar op welk argument dan ook los en zij stopt, met een gesloten boom of met een open tak, en nooit met een schouderophalen. De bewijzer op deze site legt daarbovenop een knopenbudget op, maar alleen als bescherming tegen een pathologische formule die een browsertabblad uitput - de wiskunde heeft zo'n grens niet nodig.

9. Andere bewijssystemen

Tableaus zijn één bewijssysteem van meerdere, en zij zijn het weerleggingsvormige: ze werken door falen uit te sluiten. De natuurlijke deductie doet het omgekeerd en bouwt de conclusie voorwaarts op uit de premissen, met regels als modus ponens en het voorwaardelijke bewijs, en leest veel meer zoals een wiskundige in proza redeneert. Een bewijs in natuurlijke deductie is doorgaans korter; het vinden ervan vergt doorgaans meer vindingrijkheid.

De sequentencalculus formaliseert het gevolgtrekkingsteken zelf en behandelt gevolgtrekkingsbeweringen als objecten, wat haar tot het aangewezen middel maakt om uitspraken over bewijzen te bewijzen. Resolutie brengt alles terug tot clausules en één enkele regel, wat weinig verheffend leest en buitengewoon snel draait - daarop zijn de meeste automatische bewijzers en SAT-solvers gebouwd.

Ze zijn het alle eens over welke propositionele argumenten geldig zijn; ze verschillen in hoe een bewijs eruitziet en in wat gemakkelijk te vinden is. Tableaus zijn het vriendelijkst om van te leren, omdat een mislukt bewijs geen doodlopende weg is - het overhandigt u het tegenvoorbeeld.

10. Oefenen

De snelste manier om de methode te leren is haar uit te voeren. Typ een argument in de rekenmachine met ⊨, ⊢ of |= en het tableau wordt naast de waarheidstabel getekend, zodat u de boom tegen de rijen kunt houden. Werk daarna een paar bewijzen op papier uit voordat u kijkt.