Bevis og semantiske tablåer

1. Hva et bevis er

Et argument er påstanden om at en konklusjon følger av noen premisser. Et bevis er det som avgjør den påstanden: et endelig, etterprøvbart objekt som hvem som helst kan lese linje for linje og gi sin tilslutning til, uten å måtte ta deg på ordet. Poenget med et bevis er ikke at det overbeviser - det kan en god tale også - men at hvert eneste steg i det ikke kunne ha falt ut annerledes.

Det er et strengere krav enn det høres ut som. «Det regner, så bakken er våt» er rimelig å si, men det hviler på det du vet om regn og bakke. Formell logikk skjærer det bort og stiller et snevrere spørsmål: finnes det, ut fra formen på setningene alene, i det hele tatt en måte premissene kan være sanne og konklusjonen usann på? Finnes det ingen, er argumentet gyldig, og beviset er nedtegnelsen av hvorfor det ikke gjør det.

Denne veiledningen handler om én måte å lage den nedtegnelsen på - metoden med semantiske tablåer, også kalt sannhetstrær. Det er metoden dette nettstedet bruker hver gang du skriver et argument i kalkulatoren, og har du fulgt den én gang, kan du kontrollere et argument på papir med ingenting annet enn en penn.

2. Gyldig - og hvordan du vet det

Skriv et argument med et følgetegn: premissene til venstre, konklusjonen til høyre. Påstanden p → q, ¬q ⊨ ¬p sier at av en implikasjon og negasjonen av dens konsekvens følger negasjonen av dens antecedens. Følgetegnet er ikke enda en konnektiv. Det er en påstand om formlene på hver side av det, og den er enten riktig eller gal.

Definisjonen av gyldighet peker rett på en måte å prøve den på: gå gjennom hver tildeling av sant og usant til variablene, og se om noen av dem gjør alle premissene sanne og konklusjonen usann. Det er det en sannhetstabell gjør, og med to eller tre variabler går det helt fint. Problemet er at tabellen vokser som 2ⁿ. Ti variabler krever tusen rader, tjue krever en million, og tabellen sier ingenting om hvilke rader som betydde noe.

Et tablå angriper det samme spørsmålet fra den andre enden. I stedet for å liste opp hver mulighet og lete etter en dårlig, antar det at det finnes en dårlig, og prøver å bygge den. Bryter forsøket sammen i motsigelse langs hver vei det kunne ta, finnes ingen slik tildeling, og argumentet er gyldig. Lykkes forsøket, er det som ble bygd et moteksempel du kan lese av direkte.

3. Tablåmetoden

Et tablå er et tre av fortegnede formler. Hver linje er en formel med en T eller en F foran, og fortegnet sier hva grenen antar om den formelen - ikke hva sannhetsverdien er, men hva den måtte være for at argumentet skulle svikte. Hele metoden er fire steg:

1. Skriv hvert premiss med en T. Du forutsetter at alle premissene i argumentet holder.
2. Skriv konklusjonen med en F. Du forutsetter at den svikter likevel - det er antakelsen du vil gjendrive.
3. Ta en linje som ikke alt er et atom, og bruk regelen for hovedkonnektiven og fortegnet; det regelen gir, føyes til enden av hver gren som går gjennom den.
4. Steng en gren så snart den bærer både T A og F A for den samme formelen A. Stopp når hver gren er stengt, eller når ingen linje er igjen å bryte ned.

Ingenting i den sløyfen krever list eller et valg av strategi. Hver linje har nøyaktig én regel, og å bruke dem i hvilken som helst rekkefølge gir samme dom - derfor kan en maskin gjøre det, og derfor kan du stole på resultatet når den gjør det.

4. Reglene

Det finnes én regel for hver konnektiv under hvert fortegn - ti i alt. De faller i to slag, og forskjellen mellom slagene er hele grunnen til at et tablå er et tre og ikke en liste. En α-regel sier at flere ting må holde sammen, så den stabler resultatene sine nedover grenen. En β-regel sier at én av to ting må holde, så den deler grenen i to og lar hvert tilfelle gå sin egen vei.

Hver regel er bare sannhetsbetingelsen til konnektiven sin, lest baklengs. En konjunksjon er bare sann når begge sider er det, så T (A ∧ B) stabler T A og T B. En konjunksjon er usann når minst én side er det, men formelen sier ikke hvilken, så F (A ∧ B) må prøve begge: den forgrener. Den samme asymmetrien løper motsatt vei for disjunksjonen, og en usann implikasjon betyr at antecedensen holdt og konsekvensen sviktet - det ene tilfellet der en implikasjon brister.

Merk deg hva reglene aldri gjør: de finner aldri opp en formel. Alt en regel gir, er en bit av linjen den kom fra. Den egenskapen - delformelegenskapen - er det som gjør metoden endelig, og vi kommer tilbake til den nedenfor.

5. Å stenge en gren

En gren er én sammenhengende tankerekke: les fra roten ned til et blad, og du har ett fullstendig sett antakelser. En gren stenges når de antakelsene motsier hverandre rett ut, altså når den bærer både T A og F A for én og samme formel. Det spiller ingen rolle hvor innfløkt A er, eller hvor langt fra hverandre de to linjene står - krever en gren at en formel er både sann og usann, er det ingenting som oppfyller den.

Merk en stengt gren med ×, nevn de to linjene som stengte den, og slutt å arbeide med den. Det er ikke mer å lære av en antakelse som allerede var umulig.

Når hver gren stenges, er tablået stengt, og det er beviset. Det viser at forutsetningen du begynte med - alle premisser sanne, konklusjonen usann - fører til motsigelse langs hver vei den kunne ta. Siden ingen vei var igjen, finnes ingen slik tildeling, og argumentet er gyldig. Dette er et motsigelsesbevis, lagt fram slik at tilfellene ikke kan overses.

6. Et bevis, linje for linje

Ta modus tollens: p → q, ¬q ⊨ ¬p. Linje 1 og 2 er premissene, antatt sanne. Linje 3 er konklusjonen, antatt usann - og siden konklusjonen er ¬p, er det å anta den usann det samme som å anta p sann, noe linje 5 fører opp. Linje 4 kommer av negasjonsregelen brukt på linje 2: er ¬q sann, er q usann. Implikasjonen på linje 1 er den eneste linjen igjen med en konnektiv, og den er en β-regel, så treet deler seg:

Den venstre grenen antar at implikasjonen holdt fordi antecedensen sviktet - men linje 5 har allerede p sann, så grenen motsier seg selv og stenges. Den høyre grenen antar at den holdt fordi konsekvensen var sann - men linje 4 har allerede q usann, så også den stenges.

Begge grenene stengte, så det finnes ingen måte å ha p → q og ¬q sanne med ¬p usann. Argumentet er gyldig, og treet er grunnen. Merk at beviset aldri nevner regn, bakke eller hva p og q står for. Det trengte det ikke.

7. Når en gren blir stående åpen

Ikke hvert argument er gyldig, og det er her metoden gjør nytte for seg. Arbeider du en gren gjennom til ingenting på den kan brytes videre ned - bare atomer og negerte atomer står igjen - og den fremdeles ikke er stengt, da er den grenen mettet og åpen. Den ble ikke stående ustengt fordi du stoppet for tidlig. Det er ikke mer å prøve.

En åpen gren er mer enn dommen «ugyldig». Les av fortegnene på atomene, og du har en tildeling: hvert atom merket T er sant, hvert atom merket F er usant. Den tildelingen gjør hvert premiss sant og konklusjonen usann, som er nøyaktig det et moteksempel er. Logikere kaller det en motmodell, og det er et konkret svar på «hvorfor ikke?» heller enn et avslag.

Å bekrefte konsekvensen, p → q, q ⊨ p, er standardtilfellet. Tablået lar en gren stå åpen med p usann og q sann - en situasjon der implikasjonen holder og konsekvensen holder, og antecedensen likevel ikke gjør det. Den ene tildelingen gjendriver argumentet på egen hånd.

8. Hvorfor den alltid tar slutt

Hver regel bytter ut en formel med dens egne delformler, og hver delformel er strengt kortere enn formelen den kom fra. Ingen gren kan derfor vokse i det uendelige: hvert steg går ned en endelig stige av biter av det opprinnelige argumentet, og stigen har en bunn. Til slutt er hver linje på en gren et atom eller negasjonen av et, og det er ingenting mer å gjøre.

Det er en virkelig garanti, ikke et håp. Det betyr at metoden er en avgjørelsesprosedyre for utsagnslogikken: kjør den på hvilket som helst argument, og den stopper, enten med et stengt tre eller med en åpen gren, og aldri med et skuldertrekk. Beviseren på dette nettstedet håndhever i tillegg et nodebudsjett, men bare som vern mot at en patologisk formel tømmer en nettleserfane - matematikken trenger ingen slik grense.

9. Andre bevissystemer

Tablåer er ett bevissystem blant flere, og de er det gjendrivelsesformede: de virker ved å utelukke svikt. Naturlig deduksjon går motsatt vei og bygger konklusjonen forover fra premissene, med regler som modus ponens og betinget bevis, og leses langt mer som måten en matematiker argumenterer i prosa. Et bevis i naturlig deduksjon er som regel kortere; å finne det krever som regel mer oppfinnsomhet.

Sekventkalkylen formaliserer selve følgetegnet og behandler følgepåstander som objekter, noe som gjør den til det foretrukne verktøyet når man vil bevise noe om bevis. Resolusjon reduserer alt til klausuler og én eneste regel, noe som er lite oppløftende å lese og overmåte raskt å kjøre - det er det de fleste automatiske bevisere og SAT-løsere er bygd på.

Alle er enige om hvilke utsagnslogiske argumenter som er gyldige; de skiller seg i hvordan et bevis ser ut og i hva som er lett å finne. Tablåer er de vennligste å lære av, for et mislykket bevis er ingen blindvei - det rekker deg moteksempelet.

10. Øv

Den raskeste måten å lære metoden på er å kjøre den. Skriv et argument i kalkulatoren med ⊨, ⊢ eller |=, og tablået tegnes ved siden av sannhetstabellen, så du kan holde treet opp mot radene. Arbeid deretter gjennom et par bevis på papir før du ser etter.