Bewijzen en semantische tableaus

1. Wat een bewijs is

Een argumentargumentPremissen die ter ondersteuning van een conclusie worden aangevoerd.Lees het hele lemma is de beweringpropositieEen bewering die waar of onwaar is, maar niet allebei.Lees het hele lemma dat een conclusieconclusieDe bewering die een argument wil vestigen.Lees het hele lemma volgt uitlogisch gevolgDe conclusie geldt in elke interpretatie waarin de premissen gelden.Lees het hele lemma bepaalde premissenpremisseEen bewering die een argument aanneemt om bij zijn conclusie te komen.Lees het hele lemma. 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 geldiggeldigheidGeen interpretatie maakt de premissen waar en de conclusie onwaar.Lees het hele lemma, 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 implicatieimplicatiep → q, alleen onwaar als p waar en q onwaar is.Lees het hele lemma en de ontkenningnegatieKeert een waarheidswaarde om: ¬p is waar precies als p onwaar is.Lees het hele lemma van haar consequens de ontkenning van haar antecedens volgt. Het gevolgtrekkingsteken is geen extra connectieflogisch connectiefEen symbool dat uit eenvoudiger proposities een samengestelde bouwt.Lees het hele lemma. 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 toekenninginterpretatieEén toekenning van waarheidswaarden aan alle variabelen van een formule.Lees het hele lemma van waar en onwaar aan de variabelenpropositievariabeleEen letter als p of A die voor een willekeurige propositie staat.Lees het hele lemma af en kijk of er één is die alle premissen waar en de conclusie onwaar maakt. Dat is wat een waarheidstabelwaarheidstabelEén rij per toekenning van waarden, met de waarde van de formule.Lees het hele lemma 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 tegenspraakcontradictieEen formule die onder elke interpretatie onwaar is.Lees het hele lemma in elkaar, dan bestaat zo'n toekenning niet enNANDDe negatie van een conjunctie: waar tenzij beide invoeren waar zijn.Lees het hele lemma is het argument geldig. Slaagt de poging, dan is wat zij bouwde een tegenvoorbeeldtegenmodelEen interpretatie die de premissen waar en de conclusie onwaar maakt.Lees het hele lemma 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 waarheidswaardewaarheidswaardeEen van de twee waarden die een propositie kan aannemen: waar of onwaar.Lees het hele lemma 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 atoomatomaire propositieEen propositie zonder enig connectief erin.Lees het hele lemma 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 conjunctieconjunctieAlleen waar als beide delen waar zijn: p ∧ q.Lees het hele lemma 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 disjunctiedisjunctieWaar wanneer minstens één deel waar is: p ∨ q.Lees het hele lemma, 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 ongerijmdebewijs uit het ongerijmdeNeem het tegendeel aan, leid een tegenspraak af, concludeer het origineel.Lees het hele lemma, zo uitgelegd dat geen geval kan worden gemist.

6. Een bewijs, regel voor regel

Neem modus tollensmodus tollensUit p → q en ¬q volgt ¬p.Lees het hele lemma: 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 bewijssysteemnatuurlijke deductieEen conclusie bewijzen door stap voor stap regels toe te passen.Lees het hele lemma 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 ponensmodus ponensUit p → q en p volgt q.Lees het hele lemma 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 clausulesclausuleEen disjunctie van literalen, zoals p ∨ ¬q ∨ r.Lees het hele lemma 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.