Beviser og semantiske tableauer

1. Hvad et bevis er

Et argument er påstanden om, at en konklusion følger af nogle præmisser. Et bevis er det, der afgør den påstand: et endeligt, efterprøveligt objekt, som enhver kan læse linje for linje og give ret, uden at skulle tage dit ord for noget. Pointen med et bevis er ikke, at det overbeviser - det kan en god tale også - men at hvert eneste skridt i det ikke kunne være faldet ud anderledes.

Det er et strengere krav, end det lyder. »Det regner, så jorden er våd« er rimeligt at sige, men det læner sig op ad, hvad du ved om regn og jord. Den formelle logik skærer det væk og stiller et snævrere spørgsmål: er der, alene ud fra sætningernes form, overhovedet en måde, hvorpå præmisserne kan være sande og konklusionen falsk? Er der ingen, er argumentet gyldigt, og beviset er optegnelsen over, hvorfor der ingen er.

Denne guide handler om én måde at fremstille den optegnelse på - metoden med semantiske tableauer, også kaldet sandhedstræer. Det er den metode, dette site bruger, hver gang du skriver et argument i beregneren, og har du fulgt den én gang, kan du kontrollere et argument på papir med intet andet end en kuglepen.

2. Gyldigt - og hvordan man ved det

Skriv et argument med et følgetegn: præmisserne til venstre, konklusionen til højre. Påstanden p → q, ¬q ⊨ ¬p siger, at af en implikation og negationen af dens konsekvens følger negationen af dens antecedens. Følgetegnet er ikke endnu en konnektiv. Det er en påstand om formlerne på hver sin side af det, og den er enten rigtig eller forkert.

Definitionen af gyldighed peger direkte på en måde at afprøve den på: gennemgå hver tildeling af sand og falsk til variablerne, og se, om nogen af dem gør alle præmisser sande og konklusionen falsk. Det er, hvad en sandhedstabel gør, og ved to eller tre variable er det aldeles fint. Problemet er, at tabellen vokser som 2ⁿ. Ti variable kræver tusind rækker, tyve kræver en million, og tabellen siger intet om, hvilke rækker der betød noget.

Et tableau angriber det samme spørgsmål fra den anden ende. I stedet for at opregne enhver mulighed og lede efter en dårlig antager det, at der findes en dårlig, og forsøger at bygge den. Bryder forsøget sammen i modsigelse ad hver eneste vej, det kunne tage, findes en sådan tildeling ikke, og argumentet er gyldigt. Lykkes forsøget, er det, det byggede, et modeksempel, du kan aflæse direkte.

3. Tableaumetoden

Et tableau er et træ af fortegnede formler. Hver linje er en formel med et T eller et F foran, og fortegnet siger, hvad grenen antager om den formel - ikke hvad dens sandhedsværdi er, men hvad den skulle være, for at argumentet fejlede. Hele metoden består af fire trin:

1. Skriv hver præmis med et T. Du forudsætter, at argumentets præmisser alle holder.
2. Skriv konklusionen med et F. Du forudsætter, at den alligevel fejler - det er den antagelse, du vil gendrive.
3. Tag en linje, der ikke allerede er et atom, og anvend reglen for dens hovedkonnektiv og fortegn; hvad reglen giver, føjes til enden af hver gren, der løber gennem den.
4. Luk en gren, så snart den rummer både T A og F A for den samme formel A. Stop, når hver gren er lukket, eller når ingen linje er tilbage at nedbryde.

Intet i den løkke kræver snilde eller et valg af strategi. Hver linje har præcis én regel, og at anvende dem i vilkårlig rækkefølge giver samme dom - det er derfor, en maskine kan gøre det, og derfor du kan stole på resultatet, når den gør.

4. Reglerne

Der er én regel for hver konnektiv under hvert fortegn - ti i alt. De falder i to slags, og forskellen mellem dem er hele grunden til, at et tableau er et træ og ikke en liste. En α-regel siger, at flere ting må holde sammen, så den stabler sine resultater ned ad grenen. En β-regel siger, at én af to ting må holde, så den deler grenen i to og lader hvert tilfælde gå sin egen vej.

Hver regel er blot sandhedsbetingelsen for sin konnektiv, læst baglæns. En konjunktion er kun sand, når begge sider er det, så T (A ∧ B) stabler T A og T B. En konjunktion er falsk, når mindst én side er det, men formlen siger ikke hvilken, så F (A ∧ B) må prøve begge: den forgrener. Den samme asymmetri løber den anden vej for disjunktionen, og en falsk implikation betyder, at antecedensen holdt, og konsekvensen svigtede - det ene tilfælde, hvor en implikation brister.

Læg mærke til, hvad reglerne aldrig gør: de opfinder aldrig en formel. Alt, hvad en regel giver, er et stykke af den linje, den kom fra. Den egenskab - delformelegenskaben - er det, der gør metoden endelig, og vi vender tilbage til den nedenfor.

5. At lukke en gren

En gren er én sammenhængende tankegang: læs fra roden ned til et blad, og du har ét fuldstændigt sæt antagelser. En gren lukker, når de antagelser modsiger hinanden direkte, altså når den bærer både T A og F A for én og samme formel. Det er ligegyldigt, hvor indviklet A er, eller hvor langt de to linjer står fra hinanden - kræver en gren, at en formel er både sand og falsk, opfylder intet den.

Markér en lukket gren med ×, nævn de to linjer, der lukkede den, og hold op med at arbejde på den. Der er ikke mere at lære af en antagelse, der allerede var umulig.

Når hver gren lukker, er tableauet lukket, og det er beviset. Det viser, at den forudsætning, du begyndte med - alle præmisser sande, konklusionen falsk - fører til modsigelse ad hver vej, den kunne tage. Da ingen vej var tilbage, findes en sådan tildeling ikke, og argumentet er gyldigt. Dette er et modstridsbevis, lagt frem så tilfældene ikke kan overses.

6. Et bevis, linje for linje

Tag modus tollens: p → q, ¬q ⊨ ¬p. Linje 1 og 2 er præmisserne, antaget sande. Linje 3 er konklusionen, antaget falsk - og da konklusionen er ¬p, er det at antage den falsk det samme som at antage p sand, hvilket linje 5 noterer. Linje 4 kommer af negationsreglen anvendt på linje 2: er ¬q sand, er q falsk. Implikationen på linje 1 er den eneste linje tilbage med en konnektiv, og den er en β-regel, så træet deler sig:

Den venstre gren antager, at implikationen holdt, fordi dens antecedens svigtede - men linje 5 har allerede p sand, så grenen modsiger sig selv og lukker. Den højre gren antager, at den holdt, fordi dens konsekvens var sand - men linje 4 har allerede q falsk, så også den lukker.

Begge grene lukkede, så der er ingen måde at have p → q og ¬q sande med ¬p falsk. Argumentet er gyldigt, og træet er grunden. Læg mærke til, at beviset aldrig nævner regn, jord eller hvad p og q står for. Det havde ikke brug for det.

7. Når en gren forbliver åben

Ikke ethvert argument er gyldigt, og her tjener metoden sit brød. Arbejder du en gren igennem, til intet på den kan nedbrydes yderligere - kun atomer og negerede atomer er tilbage - og den stadig ikke er lukket, så er den gren mættet og åben. Den er ikke forblevet ulukket, fordi du stoppede for tidligt. Der er ikke mere at prøve.

En åben gren er mere end dommen »ugyldigt«. Aflæs fortegnene på dens atomer, og du har en tildeling: hvert atom mærket T er sandt, hvert atom mærket F er falskt. Den tildeling gør hver præmis sand og konklusionen falsk, hvilket er præcis, hvad et modeksempel er. Logikere kalder det en modmodel, og det er et konkret svar på »hvorfor ikke?« frem for et afslag.

At bekræfte konsekvensen, p → q, q ⊨ p, er standardtilfældet. Dets tableau efterlader en gren åben med p falsk og q sand - en situation, hvor implikationen holder, og dens konsekvens holder, og hvor antecedensen alligevel ikke gør. Den ene tildeling gendriver argumentet helt alene.

8. Hvorfor den altid slutter

Hver regel erstatter en formel med dens egne delformler, og hver delformel er strengt kortere end den formel, den kom fra. Ingen gren kan derfor vokse i det uendelige: hvert skridt går ned ad en endelig stige af stykker af det oprindelige argument, og stigen har en bund. Til sidst er hver linje på en gren et atom eller negationen af et, og der er intet videre at gøre.

Det er en reel garanti, ikke et håb. Det betyder, at metoden er en afgørelsesprocedure for udsagnslogikken: kør den på et hvilket som helst argument, og den standser, enten med et lukket træ eller med en åben gren, og aldrig med et skuldertræk. Beviseren på dette site håndhæver oven i købet et knudebudget, men kun som værn mod, at en patologisk formel udtømmer en browserfane - matematikken har ingen sådan grænse brug for.

9. Andre bevissystemer

Tableauer er ét bevissystem blandt flere, og de er det gendrivelsesformede: de virker ved at udelukke fejl. Naturlig deduktion går den modsatte vej og bygger konklusionen fremad ud fra præmisserne med regler som modus ponens og betinget bevis, og den læses langt mere som den måde, en matematiker argumenterer i prosa. Et bevis i naturlig deduktion er som regel kortere; at finde det kræver som regel mere opfindsomhed.

Sekventkalkylen formaliserer selve følgetegnet og behandler følgepåstande som objekter, hvilket gør den til det foretrukne redskab, når man vil bevise noget om beviser. Resolution reducerer alt til klausuler og én enkelt regel, hvilket er ikke særlig opløftende at læse og overordentlig hurtigt at køre - det er, hvad de fleste automatiske bevisere og SAT-løsere er bygget på.

De er alle enige om, hvilke udsagnslogiske argumenter der er gyldige; de er forskellige i, hvordan et bevis ser ud, og i hvad der er let at finde. Tableauer er de venligste at lære af, for et mislykket bevis er ikke en blindgyde - det rækker dig modeksemplet.

10. Øv dig

Den hurtigste måde at lære metoden er at køre den. Skriv et argument i beregneren med ⊨, ⊢ eller |=, og tableauet tegnes ved siden af sandhedstabellen, så du kan holde træet op mod rækkerne. Arbejd derefter et par beviser igennem på papir, før du kigger.