Bevis och semantiska tablåer

1. Vad ett bevis är

Ett argument är påståendet att en slutsats följer av vissa premisser. Ett bevis är det som avgör det påståendet: ett ändligt, kontrollerbart föremål som vem som helst kan läsa rad för rad och instämma i, utan att behöva ta dig på orden. Poängen med ett bevis är inte att det övertygar - det gör ett bra tal också - utan att vart och ett av dess steg inte kunde ha blivit annorlunda.

Det är ett strängare krav än det låter. »Det regnar, alltså är marken våt« är rimligt att säga, men det lutar sig mot vad du vet om regn och mark. Den formella logiken skalar bort det och ställer en snävare fråga: finns det, enbart utifrån satsernas form, överhuvudtaget något sätt för premisserna att vara sanna och slutsatsen falsk? Finns det inget, är argumentet giltigt, och beviset är protokollet över varför det inte gör det.

Den här guiden handlar om ett sätt att framställa det protokollet - metoden med semantiska tablåer, även kallade sanningsträd. Det är den metod webbplatsen använder så snart du skriver ett argument i kalkylatorn, och har du följt den en gång kan du kontrollera ett argument på papper med ingenting annat än en penna.

2. Giltigt - och hur man vet det

Skriv ett argument med ett följdtecken: premisserna till vänster, slutsatsen till höger. Påståendet p → q, ¬q ⊨ ¬p säger att av en implikation och negationen av dess konsekvens följer negationen av dess antecedent. Följdtecknet är inte ännu en konnektiv. Det är ett påstående om formlerna på var sida om det, och det är antingen rätt eller fel.

Definitionen av giltighet pekar direkt på ett sätt att pröva den: gå igenom varje tilldelning av sant och falskt till variablerna och se om någon av dem gör alla premisser sanna och slutsatsen falsk. Det är vad en sanningstabell gör, och med två eller tre variabler duger det utmärkt. Problemet är att tabellen växer som 2ⁿ. Tio variabler kräver tusen rader, tjugo kräver en miljon, och tabellen säger ingenting om vilka rader som spelade roll.

En tablå angriper samma fråga från andra hållet. I stället för att räkna upp varje möjlighet och leta efter en dålig antar den att det finns en dålig och försöker bygga den. Rasar försöket samman i motsägelse längs varje väg det kunde ta, finns ingen sådan tilldelning och argumentet är giltigt. Lyckas försöket är det som byggdes ett motexempel som du kan läsa av direkt.

3. Tablåmetoden

En tablå är ett träd av tecknade formler. Varje rad är en formel med ett T eller ett F framför sig, och tecknet säger vad grenen antar om den formeln - inte vilket sanningsvärde den har, utan vilket den skulle behöva ha för att argumentet skulle brista. Hela metoden är fyra steg:

1. Skriv varje premiss med ett T. Du förutsätter att argumentets premisser alla håller.
2. Skriv slutsatsen med ett F. Du förutsätter att den brister ändå - det är antagandet du vill vederlägga.
3. Ta en rad som inte redan är en atom och tillämpa regeln för dess huvudkonnektiv och tecken; det regeln ger läggs sist på varje gren som löper genom den.
4. Stäng en gren så snart den bär både T A och F A för samma formel A. Sluta när varje gren är stängd, eller när ingen rad återstår att bryta ned.

Ingenting i den slingan kräver fyndighet eller ett val av strategi. Varje rad har exakt en regel, och att tillämpa dem i vilken ordning som helst ger samma utslag - därför kan en maskin göra det, och därför kan du lita på resultatet när den gör det.

4. Reglerna

Det finns en regel för varje konnektiv under varje tecken - tio sammanlagt. De faller i två slag, och skillnaden mellan slagen är hela skälet till att en tablå är ett träd och inte en lista. En α-regel säger att flera saker måste hålla tillsammans, så den staplar sina resultat nedför grenen. En β-regel säger att en av två saker måste hålla, så den delar grenen i två och låter vartdera fallet gå sin egen väg.

Varje regel är bara sanningsvillkoret för sin konnektiv, läst baklänges. En konjunktion är sann endast när båda sidor är det, så T (A ∧ B) staplar T A och T B. En konjunktion är falsk när minst en sida är det, men formeln säger inte vilken, så F (A ∧ B) måste pröva båda: den förgrenar. Samma asymmetri löper åt andra hållet för disjunktionen, och en falsk implikation betyder att antecedenten höll och konsekvensen brast - det enda fall där en implikation går sönder.

Lägg märke till vad reglerna aldrig gör: de hittar aldrig på en formel. Allt en regel ger är en bit av den rad den kom från. Den egenskapen - delformelegenskapen - är det som gör metoden ändlig, och vi återkommer till den nedan.

5. Att stänga en gren

En gren är en enda tankegång: läs från roten ned till ett löv och du har en fullständig uppsättning antaganden. En gren stängs när de antagandena motsäger varandra rakt av, alltså när den bär både T A och F A för en och samma formel. Det spelar ingen roll hur invecklad A är eller hur långt ifrån varandra de två raderna står - kräver en gren att en formel är både sann och falsk finns inget som uppfyller den.

Märk en stängd gren med ×, nämn de två rader som stängde den, och sluta arbeta på den. Det finns inget mer att lära av ett antagande som redan var omöjligt.

När varje gren stängs är tablån stängd, och det är beviset. Det visar att förutsättningen du började med - alla premisser sanna, slutsatsen falsk - leder till motsägelse längs varje väg den kunde ta. Eftersom ingen väg återstod finns ingen sådan tilldelning, och argumentet är giltigt. Detta är ett motsägelsebevis, upplagt så att inget fall kan missas.

6. Ett bevis, rad för rad

Ta modus tollens: p → q, ¬q ⊨ ¬p. Rad 1 och 2 är premisserna, antagna sanna. Rad 3 är slutsatsen, antagen falsk - och eftersom slutsatsen är ¬p innebär att anta den falsk att anta p sann, vilket rad 5 antecknar. Rad 4 kommer av negationsregeln tillämpad på rad 2: är ¬q sann, är q falsk. Implikationen på rad 1 är den enda rad som har kvar en konnektiv, och den är en β-regel, så trädet delar sig:

Den vänstra grenen antar att implikationen höll därför att dess antecedent brast - men rad 5 har redan p sann, så grenen motsäger sig själv och stängs. Den högra grenen antar att den höll därför att dess konsekvens var sann - men rad 4 har redan q falsk, så även den stängs.

Båda grenarna stängdes, alltså finns inget sätt att ha p → q och ¬q sanna med ¬p falsk. Argumentet är giltigt, och trädet är skälet. Lägg märke till att beviset aldrig nämner regn, mark eller vad p och q står för. Det behövde inte.

7. När en gren förblir öppen

Alla argument är inte giltiga, och här gör metoden verklig nytta. Arbetar du en gren tills ingenting på den kan brytas ned vidare - endast atomer och negerade atomer återstår - och den ändå inte har stängts, då är den grenen mättad och öppen. Den förblev inte ostängd för att du slutade för tidigt. Det finns inget mer att pröva.

En öppen gren är mer än utslaget »ogiltigt«. Läs av tecknen på dess atomer och du har en tilldelning: varje atom märkt T är sann, varje atom märkt F är falsk. Den tilldelningen gör varje premiss sann och slutsatsen falsk, vilket är precis vad ett motexempel är. Logiker kallar det en motmodell, och det är ett konkret svar på »varför inte?« i stället för ett avslag.

Att bejaka konsekvensen, p → q, q ⊨ p, är standardfallet. Dess tablå lämnar en gren öppen med p falsk och q sann - en situation där implikationen håller och dess konsekvens håller, och antecedenten ändå inte gör det. Den enda tilldelningen vederlägger argumentet på egen hand.

8. Varför den alltid tar slut

Varje regel ersätter en formel med dess egna delformler, och varje delformel är strikt kortare än den formel den kom från. Ingen gren kan därför växa i evighet: varje steg går nedför en ändlig stege av bitar av det ursprungliga argumentet, och stegen har en botten. Till slut är varje rad på en gren en atom eller negationen av en, och det finns inget mer att göra.

Det är en verklig garanti, inte ett hopp. Det betyder att metoden är en beslutsprocedur för satslogiken: kör den på vilket argument som helst och den stannar, antingen med ett stängt träd eller med en öppen gren, och aldrig med en axelryckning. Bevisaren på den här webbplatsen håller därtill en nodbudget, men bara som skydd mot att en patologisk formel tömmer en webbläsarflik - matematiken behöver ingen sådan gräns.

9. Andra bevissystem

Tablåer är ett bevissystem bland flera, och de är det vederläggningsformade: de arbetar genom att utesluta misslyckande. Naturlig deduktion går åt andra hållet och bygger slutsatsen framåt ur premisserna, med regler som modus ponens och villkorligt bevis, och läses långt mer som det sätt en matematiker resonerar i prosa. Ett bevis i naturlig deduktion är oftast kortare; att hitta det kräver oftast mer uppfinningsrikedom.

Sekventkalkylen formaliserar följdtecknet självt och behandlar följdpåståenden som föremål, vilket gör den till det självklara verktyget när man vill bevisa saker om bevis. Resolution reducerar allt till klausuler och en enda regel, vilket är föga upplyftande att läsa och utomordentligt snabbt att köra - det är vad de flesta automatiska bevisare och SAT-lösare är byggda på.

Alla är eniga om vilka satslogiska argument som är giltiga; de skiljer sig i hur ett bevis ser ut och i vad som är lätt att hitta. Tablåer är de vänligaste att lära sig av, eftersom ett misslyckat bevis inte är en återvändsgränd - det räcker dig motexemplet.

10. Öva

Snabbaste sättet att lära sig metoden är att köra den. Skriv ett argument i kalkylatorn med ⊨, ⊢ eller |= så ritas tablån bredvid sanningstabellen, så att du kan hålla trädet mot raderna. Arbeta sedan igenom ett par bevis på papper innan du tittar.