pathterminuspages/brkmnd.dk/aboutcontactabout me

Bevisteori

26-07-2017|Udsagnslogik

Naturlig deduktion er en kalkyle til at konstruere beviser baseret på de fire konnektiver beskrevet i syntaksen. Deduktionen sker ved at anvende følgende bevisregler deduktivt på et udsagn.

Først og fremmest skrives et bevis formelt som:

%phi_1, %phi_2, ... , %phi_n .assert %psi

Der står at med φ'erne som præmisser skal vi nå ψ som konklusion. Dette kan skrives som et udsagn ved brug af konnektiver:

%phi_1 .and %phi_2 .and ... .and %phi_n .drarrow %psi

Hver af de fire konnektiver har en introduktions- og en eliminationsregel. For negation er der en ekstra, derudover er der nogle sammensatte regler der i sig selv kan bevises. De sammensatte regler er så normale at de har fået deres eget navn.

Beviserne er lavet i en Fitchstyle-beviskasse. Denne synes jeg virker mest overskuelig. Ud for hvert udsagn er listet dettes egenskab eller hvilken regel der er brugt til at udlede udsagnet. Derudover er der sorte kasser rundt om nogle dele af beviserne, disse kasser udgør et scope.

Sidenote: Beviserne kan laves online ved at bruge ProofWeb - på siden er en guide i at bruge ProofWeb.

Konjunktion

Introduktion

{%phi %psi}over{%phi .and %psi}

Reglen siger, at har vi φ og ψ til rådighed, kan vi slutte φ ∧ ψ.

Elimination, e1 og e1

{%phi .and %psi}over{%phi} hhv. {%phi .and %psi}over{%psi}

Reglerne siger, at har vi φ ∧ ψ til rådighed, kan vi slutte dem begge en ad gangen.

Eksempel(1)

Vi vil bevise p .and q, r .assert q .and r:

p .and q __(præmis) r __(præmis) q __(.and e2) q .and r __(.and i)

Dobbelnegation

Introduktion

{%phi}over{.not\not %phi}

Elimination

{.not\not %phi}over{%phi}

Reglerne minder ret meget om minus gange minus som jo bekendt giver plus. De siger: har vi en dobbeltnegeret udsagn, kan vi slutte udsagnet som ikke negeret.

Implikation

Elimination

{%phi, %phi .drarrow %psi}over{%psi}

Reglen siger, at har vi φ samt φ ⇒ ψ, kan vi slutte ψ. Denne regel kan virke lidt mere indviklet end de tidligere. Under semantik for udsagnslogik er der sandhedstabeller, disse viser at sand medfører falsk er den eneste mulighed for en falsk implikation. Men indtil videre er dette sådan denne regel er.

Introduktion

{%phi ... %psi}over{%psi .drarrow %psi}

Reglen siger, antag φ, og hvis vi kan vise ψ, kan vi slutte φ ⇒ ψ.

Denne regel er den første af de regler der involverer en antagelse. De kan godt være lidt svære at sluge til at starte med da antagelser kan virke som noget taget ud af den blå luft.

Med antagelser i naturlig deduktion følger et scope. Antagelsen kan kun bruges inden for dette scope.

Eksempel(2a)

Vi vil gerne vise at p, p .drarrow q .and r .assert r

p __(præmis) p .imp q .and r __(præmis) q .and r __(.imp e) r __(.and e2)

Eksempel(2b)

Vi vil gerne vise at p .drarrow q, \not q .assert \not p

p .imp q __(præmis) \not q __(præmis) .scopeStart p __(antagelse) q __(.imp e) .contra .scopeSlut \not p __(.not i)

Eksempel(2c)

Vi vil gerne vise at p .drarrow q .assert \not q .drarrow \not p

p .imp q __(præmis) .scopeStart \not q __(antagelse) .scopeStart p __(antagelse) q __(.imp e) .contra __(.not e) .scopeSlut \not p __(.not i) .scopeSlut \not q .imp \not p __(.imp i)

I 2b og 2c er brugt hvad der lige straks kommer, nemlig introduktions- og eliminationsreglen for negation. Det interessante lige nu er at vi antager ¬q og viser at dette medfører ¬p.

2b kaldes Modus Tollens og er et ret anvendt resultat. Faktisk er de to sider logisk ækvivalente, mere om det senere.

2c kaldes kontraposition. De to sider er også ækvivalente, mere om det senere.

Modus Tollens (MT)

{%phi .drarrow %psi, .not%psi}over{.not%phi}

Kontraposition

{%phi .drarrow %psi}over{.not%psi .drarrow .not%phi}

Disjunktion

Introduktion, i1 og i2

{%phi}over{%phi .or %psi} hhv. {%psi}over{%phi .or %psi}

Reglerne siger, at har vi φ, kan vi slutte φ ∨ ψ da vi en med en disjunktion kun er interesseret i at en af de to udsagn er sandt.

Elimination

{%phi .or %psi, %phi ... %chi, %psi ... %chi}over{%chi}

Denne regel er en af de mere mærkelige. Den siger, at har vi en disjunktion, φ ∨ ψ, og kan vi bevise at begge disjunkter hver især fører til en eller anden formel, χ, kan vi slutte χ.

Eliminationsreglen er sådan fordi vi med antagelsen φ ∨ ψ ikke kan være sikre på hvilken af de to der sand. Derfor bliver vi nødt til at vise at begge fører til den rigtige konklusion. Denne fremgangsmåde siges at være udtømmende: der er to situationer, og vi tester begge.

Med reglen for elimination af disjunktion kan vi feks. ikke bevise %phi .or %psi .assert %psi da vi ikke kan vise at %phi .assert %psi.

Eksempel(3a)

Vi vil gerne vise at p .and q .assert p .or r

p .and q __(præmis) p __(.and e1) p .or r __(.or i1)

Eksempel(3b)

Vi vil gerne vise at p .or q, p .drarrow r, q .drarrow r .assert r

p .or q __(præmis) p .imp r __(præmis) q .imp r __(præmis) .scopeStart p __(antagelse) r __(.imp e) .scopeSlut .scopeStart q __(antagelse) r __(.imp e) .scopeSlut r __(.or e)

Eksempel(3c)

Vi vil gerne vise at disjunktioner distribuerer over konjunktioner, altså p .and (q .or r) .assert (p .and q) .or (p .and r)

p .and (q .or r) __(præmis) .scopeStart q __(antagelse) p __(.and e1) p .and q __(.and i) p .and q .or p .and r __(.or i1) .scopeSlut .scopeStart r __(antagelse) p __(.and e1) p .and r __(.and i) p .and q .or p .and r __(.or i2) .scopeSlut p .and q .or p .and r __(.or e)

Negation

Reglerne for negation er lidt mere specielle end de andre. For at behandle dem introducerer vi først en modstrid.

Modstrid

En modstrid er et udtryk af formen %phi .and .not%phi eller .not%phi .and %phi. Et andet ord for at noget er en modstrid, er at det er absurd. Til modstrid bruges tegnet ?.

Vi kan jo skrive et bevis som %phi_1 .and %phi_2 .and ... .and %phi_n .drarrow %psi. Som vi senere skal se ud fra sandhedstabeller og semantik for konnektiverne: hvis højresiden af en implikation er falsk, er udtrykket altid sandt. Dette fører til den første eliminationsregel for negation.

Bundelimination

{.contra}over{%phi}

Hvilket egentligt siger at en modstrid kan bevise hvad som helst.

Elimination

{%phi, .not%phi}over{.contra}

Reglen siger, at har vi φ og ¬φ, da har vi en modstrid.

Eksempel(4a)

Vi vil gerne vise at \not p .or q .assert p .drarrow q.

\not p .or q __(præmis) .scopeStart \not p __(antagelse) p __(antagelse) .contra __(.not e) q __(.contra e) .scopeSlut p .imp q __(.imp i) .scopeStart q __(antagelse) p __(antagelse) q __(fra antagelse) .scopeSlut p .imp q __(.imp i) p .imp q __(.or e)

Introduktion

{%phi ... .contra}over{.not%phi}

Reglen siger, at har vi en antagelse der bringer os til en modstrid, da har vi bevist at antagelsen ikke kan være sand.

Eksempel(4b)

Vi vil gerne vise at p .drarrow q, p .drarrow \not q .assert \not p.

p .imp q __(præmis) p .imp \not q __(præmis) .scopeStart p __(antagelse) q __(.imp e) \not q __(.imp e) .contra __(.not e) .scopeSlut \not q __(.not i)

Yderligere eksempler fås i 2b og 2c.

Udledte

Udover MT er der to andre tit anvendte regler. Disse er udledte, de er skabt på baggrund af ovenstående regler. Derfor kan de bevises hvilket er selvfølgelig er gjort her.

Bevis ved modstrid - Reductio ad absurdum

{.not%phi ... .contra}over{%phi}

Reglen siger: antag at det vi vil bevise, er falsk og vis at denne antagelse medfører en modstrid. Reglen minder en del om ¬i bare med omvendt fortegn. På engelsk hedder den Prove By Contradiction eller PBC.

PBC kan bevises sådan her:

Vi vil gerne vise \not p .drarrow .contra .assert p

\not p .imp .contra __(præmis) .scopeStart \not p __(antagelse) .contra __(.imp e) .scopeSlut .not\not p __(.not i) p __(.not.not e)

Lad os sige at vi vil vise et eller andet, feks. at alle ænder ikke er lavet af smør. Vi antager at der er en and der er lavet af smør, finder en and og ser at denne antagelse medfører en modstrid. Altså er alle ænder ikke lavet af smør.

Lov om den udelukkede midte - LEM

{}over{%phi .or .not%phi}

Reglen siger at enten har vi φ eller også har vi ikke φ. Reglen er selvindlysende sand, dette kaldes en tautologi, en sådan skrives med tegnet ?.

Men vi vil gerne vise at p .or \not p

.scopeStart .not(p .or \not p) __(antagelse) .scopeStart \not p __(antagelse) p .or \not p __(.or i2) .contra __(.not e) .scopeSlut p __(PBC) p .or \not p __(.or i1) .contra __(.not e) .scopeSlut p .or \not p __(PBC)

Eksempel(5)

Med LEM kan vi hurtigt bevise p .drarrow q .assert \not p .or q :

p .imp q __(præmis) p .or \not p __(LEM) .scopeStart p __(antagelse) q __(.imp e) \not p .or q __(.or i2) .scopeSlut .scopeStart \not p __(antagelse) \not p .or q __(.or i1) .scopeSlut \not p .or q __(.or e)

For ikke at tale om eliminationsreglen til dobbelt negation:

.not\not p __(præmis) p .or \not p __(LEM) .scopeStart p __(antagelse) .scopeSlut .scopeStart \not p __(antagelse) p __(.not e) .scopeSlut p __(.or e)

Læg mærke til det cirkulære i vores fremgangsmåde her. Til at bevise PBC har vi brugt elimininationsreglen for dobbelt negation. Til at bevise denne har vi brugt LEM som vi til at vise har brugt PBC. Af den grund er reglerne for dobbeltnegation ikke udledte i denne gennemgang.