Logik Rapport

Holger Bock Axelsen Michael Kirkedal Thomsen

GRD-2005-07-04.UTC:21:57:57.981341

Contents

2

1 Introduktion til Logiweb

Denne rapport er skrevet med henblik på publikation i Logiweb-systemet, og er hvad der kaldes en Logiweb-side. Logiweb er ikke kun lavet for at kunne fremvise rapporter og matematiske formler på en pæn måde^{1}; Logiweb skal også kunne forstå (dele af) den matematik, der bliver skrevet på siden. Med denne forståelse gives der mulighed for at definere en bevischecker og køre programmer, som defineret på Logiweb sider, og formelt verificere korrekthed. Logiweb-sider kan også publiceres på en Logiweb-server, så andre nemt kan henvise til siden og benytte beviser og lignende fra publicerede sider på en nem, men formel og korrekt måde.

1.1 Logiweb-siden

Til at generere Logiweb sider er der designet et sprog kaldet pyk, der på mange måder minder om andre mark-up sprog: Først defineres sidens navn, derefter de sider der refereres til, og bagefter de pyk-konstruktioner, der benyttes på siden (også dem som er defineret på referencesider). En konstruktion kan være alt fra formler og relationer til variabler og programmer. Alle konstruktioner introduceres med en pyk-(reference) og en tex-definition af deres udseende på papiret. Dette er et eksempel på forskellige aspekter af den samme konstruktion, et begreb der er meget vigtigt for pyk-compileren: F.eks. vil pyk-aspektet af en definition blive brugt i den formelle verifikation af en side, og tex-aspektet blive brugt i generering af den læsbare tekst.

Vi bruger altså en pyk-compiler i samarbejde med en Logiweb-server til at få en reel Logiweb-side. En pyk-kildetekst består således groft sagt af nogle sætninger og beviser skrevet i pyk sammensat med brødtekst, der skal være formateret i L^{A}TEX kode. Udseendet af den formelle matematik og Logiwebs forståelse af dem afhænger af de konstruktioner der er defineret på siden og i bibliografien. For den formelle verifikation af matematikken skal pyk-konstruktion-er altså benyttes.

Som uddata giver Logiweb-serveren et system af html-sider, tilgængeligt via internettet, med følgende indhold:

• Reference - Unik reference til siden så andre kan benytte indholdet.

• Vector - Den del af en Logiweb side der bliver indlæst af andre sider.

• Body - Selve siden i “papir”. Denne rapport er body til denne Logiweb side.

• Bibliography - Liste med de Logiweb-sider som siden refererer til, inkl. siden selv.

• Dictionary - Liste med alle Logiweb-konstruktioner der er introduceret på siden.

1Der er mange systemer der er god til at fremvise rapporter og især matematiske formler.

TEX (og herunder L^{A}TEX) er et meget godt eksempel herpå.

• Codex - Liste med alt som er defineret på denne side, samt deres definitioner.

• Expansion - Version af body som er makro ekspanderet fuldt ud.

• Diagnose - Hvis matematikken ikke kunne verificeres gives her en fejlmeddelelse.

• Source - Sidens kildekode (i pyk).

Indholdet i hvert af afsnittene (undtagen Source, som er den rå pyk kodetekst) kan ses i en række formater, bl.a. PDF^{2}.

For den interesserede læser er der (meget) mere om Logiweb i (base reference)

– det vigtigste at få ud af den meget korte introduktion til Logiweb ovenfor er at sider publiceret i Logiweb-systemet er checket af en automatisk bevischecker (der i sig selv er defineret i pyk).

1.2 Denne Logiweb side.

Til eksempel kan vi gennemgå denne side i Logiweb-forstand:

Denne Logiweb side hedder [HMpeano →^{pyk} “hmpeano”][HMpeano →^{tex} “HMpeano”]. I fodnoten ses den først introduktion på denne side, som er en pyk-definition af selve siden.

Denne sides bibliografi er bestemt af referencen til to andre sider:

• base^{3} - indeholder bevischecker, makroudfoldelse, aritmetik og meget mere.

• peano^{4} - definerer Peano aritmetik som benyttes på denne side.

Dens Logiweb homepage er

http://www.diku.dk/~grue/logiweb/20050502/home/funkstar/hmpeano

Dens kana reference er

     nani
     suki tana kenu tatu nanu  sena keka nasa kani suti
     nane kutu tuna keka tasi  keka tusi kise nina sesu
     siki kasi kusu sita sine  saku sika nasa natu

1.2.1 Opsætning af beviser.

Opsætningen af beviser og definitioner bliver fastlagt på Logiweb-siderne selv – i vores tilfælde benytter vi bevis-konstruktet fra [1]. Men alle lemmaer på siden skal introduceres, defineres og bevises. Læg mærke til at papiropsætningen, texaspektet, er uafhængigt af bevis-checkeren. Således kan et bevis være forkert, men sat op på samme måde som andre beviser. Kun ved at konsultere Logiwebsystemet kan man reelt verificere at beviset er korrekt^{5}.

2Portable Document Format

3Se [1].

4Se [2].

Et bevis vil på denne side fremstå som en række linier, der definerer argumentationen for beviset. Et eksempel på et bevis is systemet System for propositionen Lemma ser således ud:

System proof of Lemma:

L01: Argument ≫  Konklusion  ;
L02: Keyword ≫  Formel/Term  □

Et Argument kan være et axiom eller et lemma, og inludere linienumre, variable eller andre konstruktioner i argumentationen, og en formel understøttet af denne argumentation kan skrives som Konklusion (en sand formel, givet forudsætningerne for beviset). Mao. er opsætningen ikke tænkt som i en bevisassistent, der generer en formel udfra en given argumentation, men som linier med tilhørende argumentation. Dette svarer også til pyk-koden, og formatet brugt i (Mendelson reference). Argumenter har udforming som følgende eksempel, MP⊳L_{a} ⊳L_{b}, der skal forstås på den måde at Lemma/Axiom MP benyttet med linierne L_{a} og L_{b} som preæmisser, understøtter den givne konklusion. Den eneste anden form for argumentation vil vi se i denne rapport, er A4′ @ ẋ der siger at A4′’s substitutions variabel (meta-kvantiseret som \underline{x}) er ẋ i konklusionen.

Et Keyword er et de følgende fire:

• Arbitrary, hvor konklusionen er en meta-variabel (skrevet med kalligrafisk skrifttype). Hvad meta-variablen rangerer over (formler, termer, Peano variable) vil være klart af konteksten. Hvis vi har introduceret en variabel som Arbitrary, vil en konklusion automatisk være generaliseret (med alkvantoren ∀).

• Premise, hvor konklusion er en af de givne præmisser.

• Side-condition, hvor konklusionen er en given sidebetingelse.

• Local, hvor konklusion er bindingen af en frisk meta-variabel til en given formel/term.

Vi vil ikke direkte benytte Side-condition, men bemærker at der er forskel på at kræve noget som side-betingelse i forhold til at kræve det som præmis: I Peano aritmetik, som defineret nedenfor, har flere af axiomerne side-betingelser.

Endelig vil den sidste linie i beviset være afsluttet med □ (klassisk forkortelse for quod erat demontrandum), og konklusionen vil være identisk med Lemmaets proposition.

5Med det caveat at beviset skal være genereret udfra et pyk-bevis. Med L^{A}TEX kan man naturligvis emulere de generede beviser, hvorfor skeptikeren bør inspicere kildekoden.

1.3 Hvorfor benytte Logiweb?

Denne rapport er som betingelse skrevet i Logiweb, men det er ikke svært at se Logiwebs styrker:

• Globalt. Sider publiceret på Logiweb er tilgængelige for alle, hvilket motiverer kode-deling, og fælles udvikling.

• Modulært. Sider (som) denne kan opbygges af eksisterende bestandele.

• Selvindeholdt. Selvom vi har benyttet grunddefinitioner fra en bestemt side, er dette ikke mandatorisk, og andre formuleringer kan tænkes.

• Pænt. For læseren genereres et læsbart stykke tekst der svarer til de formelle definitioner.

• Frit. Næsten alt kan tilpasses, og specielle konstruktioner kan introduceres efter behov.

2 Peano-aritmetik

Det logiske system system vi benytter er Peano aritmetik (PA), som defineret i systemet S’ defineret på siden [2], svarende til Mendelson Lemma 3.1. Vi giver her en kort gennemgang af dette system, og henviser læseren til [2] for yderligere detaljer.

PA termer og formler er opbygget af en række konstruktorer, beskrevet ved følgende BNF:

\underline{t} ::= ˙0 | \underline{t}′ | \underline{t} ˙+ \underline{t} | \underline{t} ˙· \underline{t} | \underline{x}
\underline{f} ::= \underline{t} =^{p} \underline{t} | ˙¬ \underline{f} | \underline{f} ˙⇒ \underline{f} | ˙∀\underline{x}: \underline{f}
\underline{x} ::= ẋ

hvor ẋ er navnet på en konkret Peano variabel. Tilgængelige navne er ȧ til ż. De resterende logiske konnektiver kan defineret udfra de her givne, hvilket er gjort i [2], men i denne rapport er de originale kontruktioner nok. Når vi skriver formler i PA bruges præcedens regler til at udflade syntakstræet, og eliminere parenteser. De brugte operatorer i denne rapport har præcedensorden ˙⇒, ˙∀, ˙+, ′, hvor ′ binder stærkest. Til forskel fra Mendelson er ˙⇒ højreassociativ.

Til formel ræssonering om PA termer og formler har vi brug for axiomer og inferensregler.

[S′ →^{stmt} x]

[A1′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a}][A1′ →^{proof} Rule tactic] [A2′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c}][A2′ →^{proof} Rule tactic]

[A3′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ \underline{b} ˙⇒ ˙¬ \underline{a} ˙⇒ ˙¬ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b}][A3′ →^{proof} Rule tactic]

[A4′ →^{stmt} S′ ⊢ ∀\underline{c}: ∀\underline{a}: ∀\underline{x}: ∀\underline{b}: ⌈\underline{a}⌉≡⟨⌈\underline{b}⌉|⌈\underline{x}⌉ := ⌈\underline{c}⌉⟩ ⊢⊢ ˙∀\underline{x}: \underline{b} ˙⇒ \underline{a}][A4′ →^{proof} Rule tactic]

[A5′ →^{stmt} S′ ⊢ ∀\underline{x}: ∀\underline{a}: ∀\underline{b}: ṅonfree(⌈\underline{x}⌉, ⌈\underline{a}⌉) ⊢⊢ ˙∀\underline{x}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ ˙∀\underline{x}: \underline{b}][A5′ →^{proof} Rule tactic]

A1′ til A5′ er de velkendte axiomer for første ordens prædikat-kalkyle (Mendelson, s.69). Bemærk formalisering af Mendelsons “free for” begreb i sidebetingelserne for A4′ og A5′: ⌈\underline{a}⌉≡⟨⌈\underline{b}⌉|⌈\underline{x}⌉ := ⌈\underline{c}⌉⟩ betyder at \underline{a} er syntaktisk ækvivalent med \underline{b} hvor alle frie forekomster af \underline{x} er substitueret med \underline{c}. ṅonfree(⌈\underline{x}⌉, ⌈\underline{a}⌉) betyder det oplagte: \underline{a} indeholder ingen frie forekomster af \underline{x}. Den præcise formalisering som disse konstrukter dækker over kan ses på siden (peano reference).

Det er desuden vigtigt at bemærke forskellen på kvantisering over formler (well-forms) hvor notationen benytter den almindelige al-kvantor, og kvantisering over Peano variable, hvor notationen benytter en al-kvantor med en prik, ˙∀. I PA er disse to distinkte konstruktioner. Dette vil være relevant senere i rapporten, men det allerede nu burde konventionen være klar: Variable med prik er Peano variable, konstruktioner (funktioner, relationer) med en prik er Peano konstruktioner. Logiweb-systemet har ingen intrinsisk viden om semantikken for disse konstruktioner, dvs. vil man argumentere med f.eks. DeMorgans love, skal disse formuleres med de tilsvarende Peano konstruktioner og bevises vha. ovenstående axiomer. Mao. er Logiweb-systemet syntaktisk.

[MP′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙⇒ \underline{b} ⊢ \underline{a} ⊢ \underline{b}][MP′ →^{proof} Rule tactic]
[Gen′ →^{stmt} S′ ⊢ ∀\underline{x}: ∀\underline{a}: \underline{a} ⊢ ˙∀\underline{x}: \underline{a}][Gen′ →^{proof} Rule tactic]

Disse er de velkendte inferensregler, modus ponens og generalisering.

[S1′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} =^{p} \underline{b} ˙⇒ \underline{a} =^{p} \underline{c} ˙⇒ \underline{b} =^{p} \underline{c}][S1′ →^{proof} Rule tactic]

[S2′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} =^{p} \underline{b} ˙⇒ \underline{a}′ =^{p} \underline{b}′][S2′ →^{proof} Rule tactic]
[S3′ →^{stmt} S′ ⊢ ∀\underline{a}: ¬˙0 =^{p} \underline{a}′][S3′ →^{proof} Rule tactic]
[S4′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ =^{p} \underline{b}′ ˙⇒ \underline{a} =^{p} \underline{b}][S4′ →^{proof} Rule tactic]
[S5′ →^{stmt} S′ ⊢ ∀\underline{a}: \underline{a} ˙+ ˙0 =^{p} \underline{a}][S5′ →^{proof} Rule tactic]
[S6′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙+ \underline{b}′ =^{p} \underline{a} ˙+ \underline{b}′][S6′ →^{proof} Rule tactic]

[S7′ →^{stmt} S′ ⊢ ∀\underline{a}: \underline{a} ˙· ˙0 =^{p} ˙0][S7′ →^{proof} Rule tactic]
[S8′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙· \underline{b}′ =^{p} \underline{a} ˙· \underline{b} ˙+ \underline{a}][S8′ →^{proof} Rule tactic]

[S9′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{x}: \underline{b}≡⟨\underline{a}|\underline{x} := ˙0⟩ ⊢⊢ \underline{c}≡⟨\underline{a}|\underline{x} := \underline{x}′⟩ ⊢⊢ \underline{b} ˙⇒ ˙∀\underline{x}: \underline{a} ˙⇒

\underline{c} ˙⇒ ˙∀\underline{x}: \underline{a}][S9′ →^{proof} Rule tactic]

S1′ til S9′ er de egentlige axiomer i PA, og giver logikken lighed, rekursive definitioner af to funktioner (addition og multiplikation), samt induktion. Igen, for at skelne lighed i PA med lighed defineret andetsteds i Logiweb bibliografien for denne side (specifikt, lighed som defineret på siden [1]), har lighedstegnet fået et “p” (for Peano.) Bemærk også brugen af side-betingelser i induktionsprincippet. Brugen af Peano al-kvantoren betyder også at induktion kun kan foregå over Peano variable.

3 Hypotetisk deduktion

Beviser der gør brug af induktionsprincippet giver os et glimrende eksempel på en klassisk problemstilling i logik: forholdet mellem praktisk anvendelighed og parsimoni. Ofte vil det være muligt at komprimere en teori til meget få og præcise grundelementer, men på bekostning af brugervenlighed. Et eksempel med høj relevans for dataloger er NAND-gates: De velkendte logiske konnektiver kan repræsenteres ved blot et enkelt, binært symbol. Tilgændgæld bliver alt udover de allersimpleste udtryk uoverskuelige at læse for mennesker. En tilsvarende situation gør sig gældende for axiomatiske systemer: Mængden af axiomer kan gøres lille, men samtidig bliver systemet sværere at bruge.

Specifikt skal vi i denne rapport benytte induktion, og i induktionsskridtet bevise en implikation. Havde vi arbejdet i et andet system end PA, f.eks. naturlig deduktion (se [4]) ville fremgangsmåden havde været oplagt: naturlig deduktion inkluderer en regel der direkte laver et bevis for \underline{a} ⊢ \underline{b} om til et bevis for \underline{a} ˙⇒ \underline{b}. Det “tynde” (men ækvivalente) axiomatiske system, har ikke en sådan regel, da det kan indses ved et meta-argument at ethvert bevis for \underline{a} ⊢ \underline{b} kan transformeres til et bevis \underline{a} ˙⇒ \underline{b} rent mekanisk. Mendelson gennemgår argumentet i [3] s.37, og benytter derfra argumentet som “Deduction theorem” i teksten. Dette er en luksus vi ikke kan tillade os i et strengt formelt system som Logiweb. Alligevel er det oplagt at et bevis for \underline{a} ˙⇒ \underline{b} bør basere sig på beviset for \underline{a} ⊢ \underline{b}, og derfor står vi overfor følgende valg:

1. Udfold beviset for \underline{a} ⊢ \underline{b} i hånden.

2. Implementer deduktionsalgoritmen i pyk.

1. er den oplagte mulighed. Det er nemt og velkendt, men det giver lange, ofte uoverskuelige, beviser i praksis. 2. blev frarådet os i forelæsningerne, og selvom det absolut ville være den mest elegante løsning er det formodentlig også urealistisk givet vores erfaring med pyk og Logiweb-systemet. Men der er faktisk en løsning der kombiner begge løsningers styrker:

3. Svæk de benyttede lemmaer og arbejd bag implikationspilen.

Hvad menes der så med det? Jo, det er velkendt at vi kan svække en vilkårlig sand proposition med en vilkårlig betingelse. Dette gælder således også for lemmaer uden præmisser. Vi kan generalisere dette på følgende måde: Givet et beviseligt lemma \underline{d} ⊢ \underline{e} findes et tilsvarende hypotetisk lemma \underline{h} ˙⇒ \underline{d} ⊢ \underline{h} ˙⇒ \underline{e}. Den hypotetiske udgave af et lemma tillader os at springe implikationspilen over, så at sige. Dette medfører at givet hypotetiske versioner af de lemmaer og axiomer der indgår i beviset for \underline{a} ⊢ \underline{b}, så kan vi trivielt oversætte beviset til et bevis for \underline{a} ˙⇒ \underline{b}. Den opmærksomme læser vil indvende at dette reelt set er ækvivalent til at udfolde beviset, men med udfoldningen lagt ud i lemmaer. Dette er korrekt, men overser de motiverende faktorer:

• Hypotetiske lemmaer kan genbruges i andre beviser.

• Det nye bevis har samme længde og struktur som det originale bevis.

Disse faktorer er lovende nok til at vi har benyttet denne bevis strategi. Hypotetiske lemmaer vil fremover blive angivet med et sænket “h”, f.eks. er MP′_{h} den hypotetiske udgave af modus ponens, dvs. et lemma der siger

[MP′_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: \underline{h} ˙⇒ \underline{a} ˙⇒ \underline{b} ⊢ \underline{h} ˙⇒ \underline{a} ⊢ \underline{h} ˙⇒ \underline{b}]

Denne definition er direkte taget fra siden [2], hvor lemmaet også er bevist. Fra denne side tager vi også lemmaet Hypothesize der siger

[Hypothesize →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{a}: \underline{a} ⊢ \underline{h} ˙⇒ \underline{a}]

Normalt ville vi have kaldt et sådant lemma for “Weaken” eller noget lignende, men med den ovenstående diskussion giver Hypothesize bedre mening.

3.1 Forkortende notation

Ovenstående har vi gennemgået hvorledes vi kan benytte argumentationen i et bevis for \underline{a} ⊢ \underline{b} til at lave et bevis for \underline{a} ˙⇒ \underline{b}. Det modsatte kan naturligvis også lade sig gøre, ved en simpel anvendelse af modus ponens. Et sådant lemma vil vi kalde et regel–lemma, og være indikere med et hævet “R”, f.eks. er Mendelson 3 .2 (b)^{R} regel-udgaven af Mendelson 3 .2 (b). Vi vil benytter lemmaer der både er regel- og hypotetiske lemmaer. Dette skal forstås som “den hypotetiske udgave af regel-lemmaet”.

Derudover vil vi tillade os at lægge instantiering af lemmaer med udtryk kvantiseret over Peano variable ud i seperate lemmaer. Dette vil blive noteret som lemmaet’s navn efter fulgt at den konkrete variabel (i parentes) der instantieres med. Dette er nødvendigt da al-kvantoren for peano-variable, ˙∀, ikke er identisk med al-kvantoren for meta-variable, ∀, og bevischeckeren fra [1] ved ikke at al-kvantiserede PA udtryk kan instantieres. For at få en konkret instantiering ud af et peano-kvatiseret udtryk skal vi derfor igennem lidt teknisk fifleri med axiom A4′, men dette er uinteressant for de beviser hvori instantiering bruges.

Endelig benytter vi lokale makro-definitioner i induktions-skridtet, for at komprimere det visuelle plads-forbrug: (Næsten) alt interessant forgår bag implikations-pilen, så en metavariabel reserveres til den fælles præmis. Vi følger eksemplet fra [2] og makrodefinerer desuden anvendelser MP′ og MP′_{h} med følgende:

[x ⊵_{h} y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ⊵_{h} y ¨= MP′_{h} ⊳ x ⊳ y]⌉)]

[x ⊵ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ⊵ y ¨= MP′ ⊳ x ⊳ y]⌉)]

Dette gøres både af æstetiske hensyn, samt for at lette pyk-kodningen.

Værdien af den fremlagte strategi er åbenlys når vi betragter de resulterende beviser (nedenfor): Intet bevis er længere end 10 linier, og argumentationen er klart ækvivalent til Mendelsons.

4 Beviser

Formålet med denne rapport er at bevise kommutativitet for addition ([Mendelson 3 .2 (h) →^{pyk} “prop three two h”][Mendelson 3 .2 (h) →^{tex} “\mathit{Mendelson \; 3.2(h)}”]), som vist i [3], s.156-159.

[Mendelson 3 .2 (h) →^{stmt} S′ ⊢ ˙∀ṫ: ˙∀ṙ: ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ]

Betragtes beviset i [3], ses det at vi også har brug for følgende lemmaer fra samme afsnit:

[Mendelson 3 .2 (a) →^{pyk} “prop  three  two  a”][Mendelson 3 .2 (a) →^{tex}

“\mathit{Mendelson \; 3.2(a)}”], [Mendelson 3 .2 (b) →^{pyk} “prop three

two  b”][Mendelson 3 .2 (b) →^{tex} “\mathit{Mendelson  \;  3.2(b)}”],
[Mendelson 3 .2 (c) →^{pyk} “prop  three  two  c”][Mendelson 3 .2 (c) →^{tex}

“\mathit{Mendelson \; 3.2(c)}”], [Mendelson 3 .2 (d) →^{pyk} “prop three two d”][Mendelson 3 .2 (d) →^{tex} “\mathit{Mendelson \; 3.2(d)}”], [Mendelson 3 .2 (f ) →^{pyk} “prop three

two  f”][Mendelson 3 .2 (f ) →^{tex} “\mathit{Mendelson  \;  3.2(f)}”] og
[Mendelson 3 .2 (g) →^{pyk} “prop  three  two  g”][Mendelson 3 .2 (g) →^{tex}

“\mathit{Mendelson \; 3.2(g)}”].

For at gøre beviserne overskuelige ændres nogle af lemmaerne (og et enkelt axiom) til regellemmaer og/eller hypotetiske lemmaer samt specialisering til en konkret Peano varial. Notationen forklaret i afsnit 3 benyttes i alle tilfælde. Se bilag A & B for sætninger og beviser for disse.

4.1 Tautologier

Der ses desuden at der er brug for to unavngivne tautologier, [Lemma 1 →^{pyk} “permute premises”][Lemma 1 →^{tex} “\mathit{Lemma \; 1}”] og [Lemma 2 →^{pyk} “no middle man”][Lemma 2 →^{tex} “\mathit{Lemma \; 2}”]

Bevis for Lemma 1

[Lemma 1 →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊢ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c}]

[Lemma 1 →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊢ A2′ ≫ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c}; MP′ ⊳ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c} ⊳ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ≫ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c}; Hypothesize ⊳ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c} ≫ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c}; A1′ ≫ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b}; MP′_{h} ⊳ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c} ⊳ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b} ≫ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c}⌉, p_{0}, c)] Bevis for Lemma 2

[Lemma 2 →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ⊢ \underline{b} ˙⇒ \underline{c} ⊢ \underline{a} ˙⇒ \underline{c}]

[Lemma 2 →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ⊢ \underline{b} ˙⇒ \underline{c} ⊢ Hypothesize ⊳ \underline{b} ˙⇒ \underline{c} ≫ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c}; MP′_{h} ⊳ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊳ \underline{a} ˙⇒ \underline{b} ≫ \underline{a} ˙⇒ \underline{c}⌉, p_{0}, c)]

4.2 Beviser for hovedlemmaer

De tre første lemmaer udsiger at =^{p} er en ækvivalensrelation. Bemærk at hvor Mendelson rask væk springer flere skridt over, og benytter uidentificerede tautologier, må vi i Logiweb holde os strengt til reglerne for at vise korrekthed.

4.2.1 Bevis for Mendelson 3 .2 (a)

[Mendelson 3 .2 (a) →^{stmt} S′ ⊢ ∀\underline{t}: \underline{t} =^{p} \underline{t}]

[Mendelson 3 .2 (a) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: S5′ ≫ \underline{t} ˙+ ˙0 =^{p} \underline{t}; S1′ ≫ \underline{t} ˙+ ˙0 =^{p} \underline{t} ˙⇒ \underline{t} ˙+ ˙0 =^{p} \underline{t} ˙⇒ \underline{t} =^{p} \underline{t}; MP′ ⊳ \underline{t} ˙+ ˙0 =^{p} \underline{t} ˙⇒ \underline{t} ˙+ ˙0 =^{p} \underline{t} ˙⇒ \underline{t} =^{p} \underline{t} ⊳ \underline{t} ˙+ ˙0 =^{p} \underline{t} ≫ \underline{t} ˙+ ˙0 =^{p} \underline{t} ˙⇒ \underline{t} =^{p} \underline{t}; MP′ ⊳ \underline{t} ˙+ ˙0 =^{p} \underline{t} ˙⇒ \underline{t} =^{p} \underline{t} ⊳ \underline{t} ˙+ ˙0 =^{p} \underline{t} ≫ \underline{t} =^{p} \underline{t}⌉, p_{0}, c)]

4.2.2 Bevis for Mendelson 3 .2 (b)

[Mendelson 3 .2 (b) →^{stmt} S′ ⊢ ∀\underline{t}: ∀\underline{r}: \underline{t} =^{p} \underline{r} ˙⇒ \underline{r} =^{p} \underline{t}]

[Mendelson 3 .2 (b) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: ∀\underline{r}: S1′ ≫ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t}; Lemma 1 ⊳ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ≫ \underline{t} =^{p} \underline{t} ˙⇒ \underline{t} =^{p} \underline{r} ˙⇒ \underline{r} =^{p} \underline{t}; Mendelson 3 .2 (a) ≫ \underline{t} =^{p} \underline{t}; MP′ ⊳ \underline{t} =^{p} \underline{t} ˙⇒ \underline{t} =^{p} \underline{r} ˙⇒ \underline{r} =^{p} \underline{t} ⊳ \underline{t} =^{p} \underline{t} ≫ \underline{t} =^{p}

\underline{r} ˙⇒ \underline{r} =^{p} \underline{t}⌉, p_{0}, c)]

4.2.3 Bevis for Mendelson 3 .2 (c)

[Mendelson 3 .2 (c) →^{stmt} S′ ⊢ ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: \underline{t} =^{p} \underline{r} ˙⇒ \underline{r} =^{p} \underline{s} ˙⇒ \underline{t} =^{p} \underline{s}]

[Mendelson 3 .2 (c) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: S1′ ≫ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s} ˙⇒ \underline{t} =^{p} \underline{s}; Mendelson 3 .2 (b) ≫ \underline{t} =^{p} \underline{r} ˙⇒ \underline{r} =^{p} \underline{t}; Lemma 2 ⊳ \underline{t} =^{p} \underline{r} ˙⇒ \underline{r} =^{p} \underline{t} ⊳ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s} ˙⇒ \underline{t} =^{p} \underline{s} ≫ \underline{t} =^{p} \underline{r} ˙⇒ \underline{r} =^{p} \underline{s} ˙⇒ \underline{t} =^{p} \underline{s}⌉, p_{0}, c)]

4.2.4 Bevis for Mendelson 3 .2 (d)

[Mendelson 3 .2 (d) →^{stmt} S′ ⊢ ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: \underline{r} =^{p} \underline{t} ˙⇒ \underline{s} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s}]

[Mendelson 3 .2 (d) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: Mendelson 3 .2 (c) ≫ \underline{r} =^{p} \underline{t} ˙⇒ \underline{t} =^{p} \underline{s} ˙⇒ \underline{r} =^{p} \underline{s}; Lemma 1 ⊳ \underline{r} =^{p} \underline{t} ˙⇒ \underline{t} =^{p} \underline{s} ˙⇒ \underline{r} =^{p} \underline{s} ≫ \underline{t} =^{p} \underline{s} ˙⇒ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s}; Mendelson 3 .2 (b) ≫ \underline{s} =^{p} \underline{t} ˙⇒ \underline{t} =^{p} \underline{s}; Lemma 2 ⊳ \underline{s} =^{p} \underline{t} ˙⇒ \underline{t} =^{p} \underline{s} ⊳ \underline{t} =^{p} \underline{s} ˙⇒ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s} ≫ \underline{s} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s}; Lemma 1 ⊳ \underline{s} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s} ≫ \underline{r} =^{p} \underline{t} ˙⇒ \underline{s} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s}⌉, p_{0}, c)]

Hvis det ovenstående bevis samlignes med det givet i [3], ses det at Mendelson mangler den sidste linie, og har således ikke bevist det ønskede! Selv en stærk formel beskrivelse kan således falde igennem hvis den bliver checket af en bevis checker. Disse små, trivielle lemmaer viser med al ønskelig tænkelighed at automatiske bevis checkere er relevante, også selvom de identificerede fejl er nemme at rette. Dette gælder specielt i logik, der priser formalisme meget højt.

4.3 Induktive beviser for resterende hovedlemmaer

De sidste tre lemmaer bevises ved induktion. Hvis vi ser på axiom S9’ ser vi at vi skal vise en implikation, for at vise induktionskridtet.

Bemærk desuden at f,g,h bruger forskellige kvantorer!!!

4.3.1 Bevis for Mendelson 3 .2 (f )

[Mendelson 3 .2 (f ) →^{stmt} S′ ⊢ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ]

Vi splitter Mendelson 3 .2 (f ) i et basistilælde [Mendelson 3 .2 (f )_{0} →^{pyk} “prop three two f base”][Mendelson 3 .2 (f )_{0} →^{tex} “\mathit{Mendelson\; 3.2(f) 0}”], og et induktionsskridt [Mendelson 3 .2 (f )_{n} →^{pyk} “prop three two f ind”][Mendelson 3 .2 (f )_{n} →^{tex} “\mathit{Mendelson\; 3.2(f) n}”].

[Mendelson 3 .2 (f )_{0} →^{stmt} S′ ⊢ ˙0 =^{p} ˙0 ˙+ ˙0]

[Mendelson 3 .2 (f )_{0} →^{proof} λc.λx.P(⌈S′ ⊢ S5′ ≫ ˙0 ˙+ ˙0 =^{p} ˙0; Mendelson 3 .2 (b)^{R} ⊳

˙0 ˙+ ˙0 =^{p} ˙0 ≫ ˙0 =^{p} ˙0 ˙+ ˙0⌉, p_{0}, c)]

[Mendelson 3 .2 (f )_{n} →^{stmt} S′ ⊢ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′]

[Mendelson 3 .2 (f )_{n} →^{proof} λc.λx.P(⌈S′ ⊢ S6′_{h} ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p} ˙0 ˙+ ṫ′; S2′ ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′; Mendelson 3 .2 (d)_{h}^{R}⊳ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′⊳ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p} ˙0 ˙+ ṫ′ ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′; Gen′ ⊳ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ≫ ˙∀ṫ: ṫ =^{p}

˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′⌉, p_{0}, c)]

Induktionsbeviset for Mendelson 3 .2 (f )

[Mendelson 3 .2 (f ) →^{proof} λc.λx.P(⌈S′ ⊢ Mendelson 3 .2 (f )_{0} ≫ ˙0 =^{p} ˙0 ˙+ ˙0; Mendelson 3 .2 (f )_{n} ≫ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′; S9′ ≫ ˙0 =^{p} ˙0 ˙+ ˙0 ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ; MP′⊳ ˙0 =^{p} ˙0 ˙+ ˙0 ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ⊳ ˙0 =^{p} ˙0 ˙+ ˙0 ≫ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ; MP′ ⊳ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ⊳ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ≫ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ⌉, p_{0}, c)]