Forside/Blogaden
Tekster
UfNet
Musik
Nørderier
Linktree
FB
Om
I stedet for at fumle rundt med de der sandhedstabeller kan vi lave en kalkule som vi kan bruge til at bevise. Ideen er at vi har et sæt regler vi bruger til at deducere os frem til om konklusion \( \psi \) følger af en mængde præmisser \( \Phi \). Navnet Naturlig Deduktion kommer selvfølgeligt af den deduktive fremgangsmåde. Deduktion er at bruge generelt accepterede regler til at vise et eller andet. Her bruger vi symbolet \( \vdash \), vi vil altså vise at: $$ \phi_1,\phi_2, \dots \vdash \psi $$
Som skrevet på forrige side: alle formler der kan vises at være en tautologi med en sandhedstabel, kan vises sandt ved brug af naturlig deduktion. Dette gælder også omvendt. Så vi kan frit vælge hvilken metode vi bruger.
Lad os først og fremmest se på reglerne. Normalt har vi en eliminations-regel og en introduktions-regel. Som navnene måske antyder: for elimination og introduktion dekonstruerer vi hhv. konstruerer formlen for et givet konnektiv. Denne proces minder lidt om at programmere. Der er tilmed udviklet det der kaldes proof assitants til at assistere med at lave de her beviser. Her bruger vi BoxProver. Jeg har selv designet kasserne beviserne vises i. Du kan trykke på knappen i menuen over hver kasse for at få info om dem osv. Du kan endda eksportere koden til latex. Gear!
For at få et bevis til at køre i BoxProver, skal følgende boiler plate-kode bruges:
%abbrev proof_name : {p1}{p2} ... {pn} proof ( ... sequent ... ) = [p1][p2] ... [pn] ... proof body ... .Lad os så komme videre i programmet.
Der er om nævnt to regler her. Føst har vi introduktion.
Denne er givet ved: $$ \frac{\phi\ \ \ \ \psi}{\phi \land \psi} \land i $$ Bemærk det lille i uden for reglen. Selvfølgeligt for at markere at reglen er en introduktion. Reglerne her læses som at har vi det over brøkstregen, kan vi slutte det under. Det lyder vist rimeligt at ved vi \( \phi,\psi \) er sande, kan vi slutte \( \phi \land \psi \).
Her har vi to regler. De er stort set lige så intuitive som ovenstående. Den første: $$ \frac{\phi \land \psi}{\phi} \land e_1 $$ Og den anden: $$ \frac{\phi \land \psi}{\psi} \land e_2 $$ Ved vi at \( \phi \land \psi \) er sandt, kan vi klart slutte at hver af de to operander er sand. Nu har vi regler nok til at bevise at \( p \land q, r \vdash q \land r \), vi får:
p /\ q assumption; [l1] r assumption; [l2] q by con_e2 l1 ; [l3] q /\ r by con_i l3 l2 .Splendid. Vi kan lave flere beviser. Vi kan feks. bevise at konjunktion kommuterer:
p /\ q assumption; [l1] p by con_e1 l1 ; [l2] q by con_e2 l1 ; [l3] q /\ p by con_i l3 l2 .Vi har at \( \neg \neg \phi \vdash \phi \). Det minder ret meget om at "minus gange minus giver plus". Det er også rimeligt intuitivt: at sætningen "det er ikke tilfældet at jeg ikke har en kat" er det samme som at sige "jeg har en kat" - selvom første er en noget mere uelegant og forvirrende måde at sige det på.
Lad os bare få den skrevet ned: $$ \frac{\neg \neg \phi}{\phi} \neg \neg e $$
Her er den: $$ \frac{\phi}{\neg \neg \phi} \neg \neg i $$
Med det vi har været igennem indtil videre, kan vi bevise noget a la \( \neg \neg (p \land q) \vdash \neg \neg p \land q \), vi får:
~ ~ (p /\ q) assumption; [l1] p /\ q by nne l1 ; [l2] p by con_e1 l2 ; [l3] ~ ~ p by nni l3 ; [l4] q by con_e2 l2 ; [l5] ~ ~ p /\ q by con_i l4 l5 .Denne er ret meget lige ud ad landevejen. Den er magen til modus ponens vi snakkede om under semantik. Vi har $$ \frac{\phi \ \ \ \phi \rightarrow \psi}{\psi} \rightarrow e $$ Vi kan udvide reglen til hvad der kaldes modus tollens (dette er en udledt regel, mere om dem senere): $$ \frac{\neg \psi \ \ \ \phi \rightarrow \psi}{\neg \phi} MT $$ Og vi kan nu vise at \( p, p \rightarrow q, q \rightarrow r \vdash r \), get it on:
p assumption; [l1] p => q assumption; [l2] q => r assumption; [l3] q by imp_e l1 l2 ; [l4] r by imp_e l4 l3 .Vi kan bruge MT til at vise at \( \neg r, p \rightarrow q, q \rightarrow r \vdash \neg p \):
~ r assumption; [l1] p => q assumption; [l2] q => r assumption; [l3] ~ q by mt l3 l1 ; [l4] ~ p by mt l2 l4 .For at håndtere introduktionsreglen her bliver vi nødt til at forholde os til en antagelse. Vi vil gerne vise at hvis \( \phi \) er sand, er \( \psi \) også sand. Måden at gøre det på er at antage at \( phi \) er sand. Og så bruge den antagelse til at vise at \( \psi \) er sand. Det åbner op for et scope i de her beviskasser. Vi skal være sikre på at antagelsen ikke forlader kassen og bruges til at bevise alt mulig andet. Nu til reglen: $$ \frac{[ \phi \cdots \psi ]}{\phi \rightarrow \psi} \rightarrow i $$ hvor [] indikerer scoped. Vi kan bruge reglen til at vise at implikationer er transitive, dvs. at \( p \rightarrow q, q \rightarrow r \vdash p \rightarrow r \). Vi får:
p => q assumption; [l1] q => r assumption; [l2] ( p assumption; [l3] q by imp_e l3 l1 ; [l4] r by imp_e l4 l2 ) ; [imp1] p => r by imp_i imp1 .Jeg har lagt skygger på kassen så den er lidt mere tydelig.
Med det vi har indtil videre kan vi vise at \( p \land q \rightarrow r \vdash p \rightarrow (q \rightarrow r) \), vi får:
p /\ q => r assumption; [l1] ( p assumption; [l2] ( q assumption; [l3] p /\ q by con_i l2 l3 ; [l4] r by imp_e l4 l1 ) ; [imp1] q => r by imp_i imp1 ) ; [imp2] p => (q => r) by imp_i imp2 .Vi kan også vise at \( p \rightarrow (q \rightarrow r) \vdash p \land q \rightarrow r \), vi får:
p => (q => r) assumption; [l1] ( p /\ q assumption; [l2] p by con_e1 l2 ; [l3] q => r by imp_e l3 l1 ; [l4] q by con_e2 l2 ; [l5] r by imp_e l5 l4 ) ; [imp1] p /\ q => r by imp_i imp1 .Læg mærke til de to foregående beviser. De er omvendte af hinanden. Vi har altså bevist begge veje. Dvs. vi har $$ p \rightarrow (q \rightarrow r) \dashv \vdash p \land q \rightarrow r $$ Hvilket betyder at de to udtryk på hver side er logisk ækvivalente.
Disse to er lige ud ad landevejen, vi har: $$ \frac{\phi}{\phi \lor \psi} \lor i_1 $$ og $$ \frac{\psi}{\phi \lor \psi} \lor i_2 $$ Det giver vel rimelig mening intuitivt at hvis "jeg har en kat" er sand, så er "jeg har en kat eller en hund" det også. Disse er lidt de omvendte af elimination for konjunktion.
Denne er noget mere omstændig. Vi kan starte med at skrive den op: $$ \frac{\phi \lor \psi \ \ [\phi \cdots \chi]\ \ [\psi \cdots \chi]}{\chi} \lor e $$ Som med implikation introduktion involvere denne antagelse(r). Der er to i dette tilfælde. Nu når introduktion for disjunktion var så let at forholde sig til, hvorfor er denne så så bøvlet? Godt spørgsmål. Problemet med at \( \phi \lor \psi \) er sand, er at vi ikke ved hvilken af de to der er sand. Så for at dekonstruere en disjunktion, bliver vi nødt til at antage at begge er sande hver for sig og vise at det medfører det resultat vi prøver at nå. Så vi åbner to separate scopes og viser at begge fører til \( \chi \). Lad os bare gå i gang med at vise at disjunktion kommuterer, altså \( p \lor q \vdash q \lor p \):
p \/ q assumption; [l1] ( p assumption; [l2] q \/ p by dis_i2 l2 ) ; [dis1] ( q assumption; [l3] q \/ p by dis_i1 l3 ) ; [dis2] q \/ p by dis_e l1 dis1 dis2 .Husk det med at antagelser ikke må forlade deres scope. Vi kan let vise den anden vej, vi kan bare bytte om på navnene af variable. Så vi har at \( \phi \lor \psi \equiv \psi \lor \phi \). Flere beviser. Vi har disjunktion distribuerer over konjunktion, dvs. \( p \land (q \lor r) \vdash (p \land q) \lor (p \land r) \), vi får:
p /\ (q \/ r) assumption; [l1] p by con_e1 l1 ; [l2] q \/ r by con_e2 l1 ; [l3] ( q assumption; [l4] p /\ q by con_i l2 l4 ; [l5] (p /\ q) \/ (p /\ r) by dis_i1 l5 ) ; [dis1] ( r assumption; [l6] p /\ r by con_i l2 l6 ; [l7] (p /\ q) \/ (p /\ r) by dis_i2 l7 ) ; [dis2] (p /\ q) \/ (p /\ r) by dis_e l3 dis1 dis2 .Vi har også den anden vej. Altså har vi at \( p \land (q \lor r) \equiv (p \land q) \lor (p \land r) \)
For at forholde os til de her regler skal vi lige vende tilbage til det at noget er en modsigelse. Hele det her bevissystem er bygget op omkring ideen om en implikation. Det over og det under brøkstregen kan ses som venstreside hhv. højreside af en implikation. Vi kan bare skrive en eller anden regel ud for at indse det, feks. disjunktion introduktion: "hvis jeg ved at φ er sand, ved jeg at φ ∨ ψ er sand". Vi ved fra sandhedstabellen at hvis \( \bot \rightarrow \phi \) altid er sand. Uanset \( \phi \). Så vi ved at har jeg ⊥, kan jeg bevise alting. Typisk skriver vi en kontradiktion som \( p \land \neg p \). Altså "jeg har en kat og jeg har ikke en kat" hvilket helt åbenlyst er absurd. Så hvis jeg antager \( \phi \land \neg \phi \), kan jeg bevise hvad som helst. Det er lidt noget rod. Feks. kan jeg antage at jorden er flad og bruge det til at bevise hvad som helst. På en anden side forlader vi ligesom det her bevissystem med den slags antagelser.
Denne har vi lige diskuteret, vi har: $$ \frac{\bot}{\phi} \bot e $$ Har vi noget absurd, slutter vi bare løs.
Nu har vi at: $$ \frac{\phi \ \ \ \ \neg \phi}{\bot} \neg e $$ Lad os bruge det til at vise at \( \neg p \lor q \vdash p \rightarrow q \):
~ p \/ q assumption; [l1] ( ~ p assumption; [l2] ( p assumption; [l3] bot by neg_e l3 l2 ; [l4] q by bot_e l4 ) ; [imp1] p => q by imp_i imp1 ) ; [dis1] ( q assumption; [l3] ( p assumption; [l4] q by copy l3 ) ; [imp1] p => q by imp_i imp1 ) ; [dis2] p => q by dis_e l1 dis1 dis2 .Dette går begge veje, altså har at \( \neg p \lor q \equiv p \rightarrow q \)
Denne er lidt mere intuitiv. Lad os sige vi har en antagelse der ender i en modsigelse. Så må denne antagelse være falsk, right? Altså har vi: $$ \frac{[\phi \cdots \bot]}{\neg \phi} \neg i $$
Vi kan nu vise at \( \neg p \rightarrow \bot \vdash p \). Denne slags formel kaldes bevis ved modsigelse. Eller prove by contradiction på engelsk. Eller forkortet PBC. Eller sågar reductio ad absurdum. Læg mærke til forskellen på negation introduktion og PBC. Ved PBC er antagelsen negeret. Vi får:
~ p => bot assumption; [l1] ( ~ p assumption; [l2] bot by imp_e l2 l1 ) ; [neg1] ~ ~ p by neg_i neg1 ; [l3] p by nne l3 .Vi har PBC som: $$ \frac{[\neg \phi \cdots \bot]}{\phi} PBC $$ Både PBC og MT er det vi kalder afledte regler. De andre regler vi har været igennem kan ses som basale regler, og afledte regler altså regler der kan afledes på baggrund af basale regler.
Der er i hvert fald endnu en nævneværdig afledt regel, nemlig LEM eller Law of the Excluded Middle. Den er ret handy. Vi har: $$ \frac{}{\phi \lor \neg \phi} LEM $$ Den er også ret intuitiv. Enten har jeg en kat, eller også har jeg ikke en. Læg mærke til at der ikke er noget over brøkstregen på denne regel. Den holder vand uanset. Regler der bare er sande, kalder vi aksiomer. Vi kan bruge LEM til følgende bevis:
( ~ (p \/ ~ p) assumption; [l1] ( ~ p assumption; [l2] p \/ ~ p by dis_i2 l2 ; [l3] bot by neg_e l3 l1 ) ; [case1] p by pbc case1 ; [l4] p \/ ~ p by dis_i1 l4 ; [l5] bot by neg_e l5 l1 ) ; [case2] p \/ ~ p by pbc case2 .
Index
Del
Terminus