Formelt bevis for kummutativitet af addition under Peanos axiomer

Anders Vaaben Andersen

GRD-2005-07-04.UTC:09:35:58.146674

Contents

1 Indledning 2

2 Logiweb 2

3 Peano aritmetik 3

3.1 Symboler i Peano aritmetik . . . . . . . . . . . . . . . . . . . . . 4 3.1.1 Termer . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.1.2 Formularer . . . . . . . . . . . . . . . . . . . . . . . . . . 4 3.1.3 Andre symboler . . . . . . . . . . . . . . . . . . . . . . . . 4

3.2 Axiomer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2.1 De logiske axiomer . . . . . . . . . . . . . . . . . . . . . . 6 3.2.2 Slutningsregler . . . . . . . . . . . . . . . . . . . . . . . . 6 3.2.3 De ægte axiomer . . . . . . . . . . . . . . . . . . . . . . . 7

4 Sætninger 8 4.1 Mendelson Lemma 3.2 (a) . . . . . . . . . . . . . . . . . . . . . . 8 4.2 Mendelson Lemma 3.2 (b) . . . . . . . . . . . . . . . . . . . . . . 9

4.2.1 Deduktions algoritmen . . . . . . . . . . . . . . . . . . . . 10 4.2.2 Hypothetitisk modus ponens . . . . . . . . . . . . . . . . 10 4.2.3 Tilføj hypotese . . . . . . . . . . . . . . . . . . . . . . . . 11 4.2.4 Hypotetisk generalisering . . . . . . . . . . . . . . . . . . 11 4.2.5 Korollar M1.10b . . . . . . . . . . . . . . . . . . . . . . . 11

4.3 M3.2(c) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 4.4 M3.2(d) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4.5 Flere hypotetiske lemmaer . . . . . . . . . . . . . . . . . . . . . . 15 4.6 Lemma M3.2(h)(I) . . . . . . . . . . . . . . . . . . . . . . . . . . 17 4.7 Lemma M3.2(g) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 4.8 Lemma M3.2(h)(II) . . . . . . . . . . . . . . . . . . . . . . . . . . 19 4.9 Lemma M3.2(h) . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

5 Konklusion 20 A Pyk definitioner 21

A.1 Sidens navn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 A.2 Modus ponens . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 A.3 Variable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 A.4 free og nonefree . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 A.5 Variables of Peano arithmetic . . . . . . . . . . . . . . . . . . . . 22 A.6 TEX definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 A.7 Test . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 A.8 Priority table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

B Index 27

C Bibliografi 27

D Pyk kildetekst 27

1 Indledning

Følgende er en besvarelse af rapport opgaven på logik kurset ved DIKU foråret 2005 udarbejdet af Anders Vaaben Andersen. Sigtet med opgaven er at føre læseren gennem et bevis for [ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ] med udgangspunkt i Peanos axiomer. Det er tilstræbt at rapporten kan læses uden større forhåndskendskab til formel bevisførelse, dog forventes et kendskab til de logiske symboler, samt kendskab til begreberne frie og bundne variable. Beviset er produceret i pyk sproget hvilket har muliggjort en maskinel kontrol af bevisets korrekthed og er publiceret på DIKUS lokale logiweb system. Fra webadressen http://www.diku.dk/ grue/logiweb/20050502/home/vaaben/proofreport/latest/ kan man hente denne rapport både som pyk kildetekst, som LaTeX fil, som dvi eller som pdf. Yderligere kan man på den ovenstående URL se at Logiweb siden er godkendt. Siden er baseret påden oprindelige ’Peano’ side af Klaus Grue og alle dens konstruktioner er inkluderet direkte påsiden. Denne side kan findes på http://www.diku.dk/ grue/logiweb/20050502/home/grue/peano/GRD-2005-06-22-UTC-07-23-31-271829/ Fokus vil primært være på hvorledes et formelt bevis forløber samt metoder til at undgå at beviserne bliver for store og uoverskuelige. Der vil undervejs blive refereret til sætninger fra [2] desuden vil beviserne i hovedtræk være ført på samme måde.

2 Logiweb

Kort fortalt er Logiweb [1] et system til at publicere sider med matematisk indhold, hvor korrektheden af det matematiske indhold bliver kontrolleret af Logiweb serveren. En Logiweb side starter som en pyk kildetekst, der indeholder følgende elementer:

• PAGE, som definerer sidens navn.

• BIBLIOGRAPHY, referencer til andre Logiweb sider, hvorfra pyk konstruktioner importeres.

• PREASSOCIATIVE/POSTASSOCIATIVE der bestemmer associativitets regler samt hvilke konstruktioner, der skal importeres fra siderne i bibliografien.

• BODY indeholder kroppen af en TeX fil med pyk konstruktioner indlejret.

Pyk konstruktionerne bliver dels oversat til et binært format der kan læses af logiweb serveren og dels oversat til TeX. Den binære version bruges til at checke sidens korrekthed, mens TeX versionen automatisk bliver oversat til dvi og pdf når pyk compileren er færdig. Noget egentligt kendskab til Logiweb forudsættes ikke i det følgende da pyk compileren i samarbejde med TeX producerer læselig matematisk notation. Såfremt læseren har et ønske om at tilegne sig yderligere kendskab til logiweb systemet kan hevises til base page som denne rapports Logiweb side inkluderer (http://www.diku.dk/ grue/logiweb/20050502/home/grue/base/latest/). Alternativt kan man hente kildeteksten fra den URL, der blev nævnt i indledningen. Hvis man allerede er fortrolig med TeXs syntaks burde det være nemt at identificere de dele der bliver fortolket af pyk kompileren. De forskellige centrale pyk konstruktioner kan desuden ses i fodnoterne efterhånden som de bliver introduceret mens appendix A indeholder alle de knap så centrale.

3 Peano aritmetik

Som nævnt indledningsvis vil rapporten gennemgå et formelt bevis for sætningen [ ˙∀ẋ: ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ]. Peanos axiomer der vil blive benyttet som udgangspunkt for beviset er en axiomatisering af de naturlige tal samt symbolerne plus, gange og lighed. På et intuitivt plan er axiomerne oplagt sande udsagn om de naturlige tal, men hvad der er knap så oplagt er at de medfører grundlæggende egenskaber som associativitet, distributivitet og den egenskab som vil blive vist i det følgende: kommutativitet. Hvor man i de fleste matematiske tekster vil undlade detaljer der må betragtes som indlysende vil beviset i det efterfølgende være udpenslet således at enhvert argument kan spores tilbage til axiomerne. Hovedmotivationen for axiomatisering og formel logik har netop været at give matematik et så solidt grundlag at intet var overladt til intuition, samt undgåde paradokser der opstod af et for løst matematisk fundament.

3.1 Symboler i Peano aritmetik

3.1.1 Termer

Termer er opbygget af følgende symboler:

• Variable, der repræsenteres af de små bogstaver fra det engelske alfabet: [ȧ] - [ż]. [˙0 →^{pyk} “peano zero”][˙0 →^{tex} “ \dot{0}”] svarer til symbolet nul. Alle andre tal defineres induktivt som efterfølgere [x′ →^{pyk} “∗ peano succ”][x′ →^{tex} “#1.’”], af hinanden.

• Derudover kan termer indeholde plus [x ˙+ y →^{pyk} “∗ peano plus

∗”][x ˙+ y →^{tex} “#1.

\mathop{\dot{+}} #2.”]

• Gange [x ˙· y →^{pyk} “∗ peano times ∗”][x ˙· y →^{tex} “#1.

\mathop{\dot{\cdot}} #2.”].

3.1.2 Formularer

Formularer er opbygget af:

• Lighed [x =^{p} y →^{pyk} “∗ peano is ∗”][x =^{p} y →^{tex} “#1.

\stackrel{p}{=} #2.”] mellem termer.

• Negation [ ˙¬ x →^{pyk} “peano not ∗”][ ˙¬ x →^{tex} “ \dot{\neg}\, #1.”] af en formular

• Implikation [x ˙⇒ y →^{pyk} “∗ peano imply ∗”][x ˙⇒ y →^{tex} “#1.

\mathrel{\dot{\Rightarrow}} #2.”] mellem formularer.

• universel kvantifisering [ ˙∀x: y →^{pyk} “peano all ∗ indeed ∗”][ ˙∀x: y →^{tex} “ \dot{\forall} #1. \colon #2.”] af en formular.

Bemærk at implikation i det følgende er højre associativ modsat konventionen i Mendelson.

3.1.3 Andre symboler

Derudover kan følgende almindeligt kendte symboler umiddelbart defineres udfra de ovenstående:

• Een: [˙1 →^{pyk} “peano one”][˙1 →^{tex} “ \dot{1}”] som

[˙1 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[˙1 ¨= ˙0′]⌉)]

• To: [˙2 →^{pyk} “peano two”][˙2 →^{tex} “ \dot{2}”] som

[˙2 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[˙2 ¨= ˙1′]⌉)]

• Logisk og: [x ˙∧ y →^{pyk} “∗ peano and ∗”][x ˙∧ y →^{tex} “#1. \mathrel{\dot{\wedge}} #2.”] som

[x ˙∧ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ˙∧ y ¨= ˙¬ (x ˙⇒ ˙¬ y)]⌉)]

• Logisk eller: [x ˙∨ y →^{pyk} “∗ peano or ∗”][x ˙∨ y →^{tex} “#1. \mathrel{\dot{\vee}} #2.”] som

[x ˙∨ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ˙∨ y ¨= ˙¬ x ˙⇒ y]⌉)]

• Biimplikation: [x ˙⇔ y →^{pyk} “∗ peano iff ∗”][x ˙⇔ y →^{tex} “#1. \mathrel{\dot{\Leftrightarrow}} #2.”] som

[x ˙⇔ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ˙⇔ y ¨= (x ˙⇒ y) ˙∧ (y ˙⇒ x)]⌉)]

• Eksistens: [ ˙∃x: y →^{pyk} “peano exist ∗ indeed ∗”][ ˙∃x: y →^{tex} “ \dot{\exists} #1. \colon #2.”] som

[ ˙∃x: y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ ˙∃x: y ¨= ˙¬ ˙∀x: ˙¬ y]⌉)]

Symbolerne er defineret som makroer, dvs pyk compileren erstatter dem med definition før siden bliver kontrolleret. Jeg har dog valgt udelukkende at holde mig til de oprindelige symboler da jeg synes det gør det væsentligt nemmere at overskue korrektheden af et bevis end når forskellige symboler dækker over helt ækvivalente udsagn. Det skal bemærkes at hvor Mendelson skelner i sin notation mellem termer og formularer, så er der i den underliggendende pyk implementation for denne rapport benyttet såkaldte metavariable til både termer og formularer. Dog kan man altid udlede af konteksten hvad et symbol repræsenterer så det burde ikke skabe forvirring.

3.2 Axiomer

Axiomerne er det fundament hvoraf sætningerne i en teori kan opbygges. Løst sagt kan man beskrive dem som de ’grundantagelser’ der er nødvendige før man kan drage konklusioner om noget som helst. Peano aritmetikken består af 14 axiomer samt 2 slutningsregler, hvoraf de 5 første axiomer er de logiske axiomer, der er fælles for alle første ordens teorier, mens de 9 ’ægte’ axiomer er specifikke for Peano aritmetik. System [S′ →^{pyk} “system prime s”][S′ →^{tex} “ S’”] [S′ →^{stmt} ∀\underline{a}: ∀\underline{b}: \underline{a} ˙+ \underline{b}′ =^{p} \underline{a} ˙+ \underline{b}′ ⊕ ∀\underline{a}: ∀\underline{b}: ˙¬ \underline{b} ˙⇒ ˙¬ \underline{a} ˙⇒ ˙¬ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b} ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} =^{p} \underline{b} ˙⇒ \underline{a}′ =^{p} \underline{b}′ ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙⇒ \underline{b} ⊢ \underline{a} ⊢ \underline{b} ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a}′ =^{p} \underline{b}′ ˙⇒ \underline{a} =^{p} \underline{b} ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ⊕ ∀\underline{x}: ∀\underline{a}: ∀\underline{b}: ṅonfree(⌈\underline{x}⌉, ⌈\underline{a}⌉) ⊢⊢ ˙∀\underline{x}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ ˙∀\underline{x}: \underline{b} ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙· \underline{b}′ =^{p} \underline{a} ˙· \underline{b} ˙+ \underline{a} ⊕ ∀\underline{a}: \underline{a} ˙+ ˙0 =^{p} \underline{a} ⊕ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c} ⊕ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} =^{p} \underline{b} ˙⇒ \underline{a} =^{p} \underline{c} ˙⇒ \underline{b} =^{p} \underline{c} ⊕ ∀\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} ⊕

∀\underline{a}: ¬˙0 =^{p} \underline{a}′ ⊕ ∀\underline{x}: ∀\underline{a}: \underline{a} ⊢ ˙∀\underline{x}: \underline{a} ⊕ ∀\underline{c}: ∀\underline{a}: ∀\underline{x}: ∀\underline{b}: ⌈\underline{a}⌉≡⟨⌈\underline{b}⌉|⌈\underline{x}⌉ := ⌈\underline{c}⌉⟩ ⊢⊢

˙∀\underline{x}: \underline{b} ˙⇒ \underline{a} ⊕ ∀\underline{a}: \underline{a} ˙· ˙0 =^{p} ˙0]

3.2.1 De logiske axiomer

De logiske axiomer beskæftiger sig ikke med termer men udelukkende med sammenhænge mellem formularer. A1 - A3 er de grundlæggende for formelle teorier, mens A4-A5 yderligere fastlægger en første ordens teori. [A1′ →^{pyk} “axiom prime a one”][A1′ →^{tex} “ A1’”], [A2′ →^{pyk} “axiom prime a two”][A2′ →^{tex} “ A2’”], [A3′ →^{pyk} “axiom prime a three”][A3′ →^{tex} “ A3’”], [A4′ →^{pyk} “axiom prime a four”][A4′ →^{tex} “ A4’”], og [A5′ →^{pyk} “axiom prime a five”][A5′ →^{tex} “ A5’”]

[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]

Både axiom A4 og A5 har sidebetingelser for deres anvendelse. A4s sidebetingelse kræver at [\underline{c}] er fri for [\underline{x}] i [\underline{b}]. [\underline{x}] kan eventuelt være lig [\underline{c}] A5s sidebetingelser er at der ikke findes nogen frie forekomster af [\underline{x}] i [\underline{a}].

3.2.2 Slutningsregler

De to slutningsregler Peano aritmetik er: [MP′ →^{pyk} “rule prime mp”][MP′ →^{tex} “ MP’”] og [Gen′ →^{pyk} “rule prime gen”][Gen′ →^{tex} “ Gen’”]

[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]

Bemærk at begge regler benytter symbolet ⊢ . Symbolet betyder at det der står efter det sidste ⊢ symbol kan konkluderes hvis man allerede har vist de formularer, der står foran ⊢ symbolerne. Intuitivt svarer det til symbolet ˙⇒ men med den afgørende forskel at ˙⇒ er et symbol i Peano sproget mens ⊢ betyder at det er en forudsætning der skal være opfyldt før man kan bruge en sætningen eller reglen. Modus ponens der er den primære logiske slutningsregel gør os i stand til at slutte [\underline{b}] når man allerede har vist [\underline{a} ˙⇒ \underline{b}] hvis man allerede har vist [\underline{a}]. Jeg vil senere komme ind på hvorledes man kan konstruere et bevis for at [\underline{a} ˙⇒ \underline{b}] når man har et bevis for [\underline{a} ⊢ \underline{b}]. I det følgende vil jeg betegne det der står foran ⊢ som en ’forudsætning’, mens jeg vil betegne det der står foran ˙⇒ som en ’hypotese’. Desuden vil jeg for sætninger med flere hypoteser ( f.eks [\underline{i} ˙⇒ \underline{h} ˙⇒ \underline{a}] ) betegne hypotesen længst til venstre som den første eller forreste mens jeg for forudsætninger vil betegne forudsætningen længst til højre som den første eller forreste.

3.2.3 De ægte axiomer

De sidste 9 axiomer er regneregler, der fastlægger egenskaberne for plus, gange og lighed. Axiomerne der er valgt afviger en smule fra dem, der er beskrevet i Mendelson idet Mendelsons axiomer udtaler sig om forhold mellem variable mens disse axiomer udtaler sig om forhold mellem termer. De to axiomssæt er dog fuldstændigt ækvivalente og kan hver især nemt udledes fra det andet. Bemærk det sidste og meget centrale axiom. Det er dette axiom, der tillader induktionsbeviser, hvilket bliver essentielt i de tre store afsluttende sætninger fra Mendelson. [S1′ →^{pyk} “axiom prime s one”][S1′ →^{tex} “ S1’”], [S2′ →^{pyk} “axiom prime s two”][S2′ →^{tex} “ S2’”], [S3′ →^{pyk} “axiom prime s three”][S3′ →^{tex} “ S3’”], [S4′ →^{pyk} “axiom prime s four”][S4′ →^{tex} “ S4’”], [S5′ →^{pyk} “axiom prime s five”][S5′ →^{tex} “ S5’”], [S6′ →^{pyk} “axiom prime s six”][S6′ →^{tex} “ S6’”], [S7′ →^{pyk} “axiom prime s seven”][S7′ →^{tex} “ S7’”], [S8′ →^{pyk} “axiom prime s eight”][S8′ →^{tex} “ S8’”], [S9′ →^{pyk} “axiom prime s nine”][S9′ →^{tex} “ S9’”].

[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]

4 Sætninger

Som nævnt indledningsvis vil beviset blive ført fra bar bund. Dvs de eneste linjer der kan bruges i beviset er axiomer, slutningsregler eller sætninger, der er bevist på denne logiweb side. Jeg vil i nogle tilfælde præsentere beviserne i omvendt rækkefølge således at man på forhånd kan se at de enkelte lemmaer tjener et formål. I hovedtræk vil beviserne følge de beviser, der er beskrevet i Mendelson, men specielt i forbindelse med brug af sætning 2.5 (Deduktions sætningen) vil der blive foretaget nogle afvigelser. Indledningsvis vil jeg dog bevise nogle helt grundlæggende egenskaber ved Peano aritmetik. Det allerførste resultat der skal vises er følgende:

4.1 Mendelson Lemma 3.2 (a)

[L3.2(a)′ →^{pyk} “lemma prime l three two a”][L3.2(a)′ →^{tex} “L3.2(a)’”] Det første bevis stammer fra den oprindelige Peano side og da beviset er rimeligt simpelt er det en god introduktion til hvordan et formelt bevis ser ud: [M3.2(a) →^{pyk} “mendelson three two a”][M3.2(a) →^{tex} “ M3.2(a)”]

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

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

Den allerførste linje siger at beviset gælder for vilkårlige [\underline{a}]. Linje 2 og 3 instantierer axiomerne S5 og S1. Bemærk at for linje S1 i linje 3 er [\underline{c}] og [\underline{b}] valgt lig [\underline{a}] således at de to hypoteser er lig hinanden og konklusionen er det ønskede resultat. Samtidig er S5 i linje to valgt så den matcher de to hypoteser i linje tre. Derfor kan beviset nemt afsluttes ved at bruge modus ponens med linje to på linje tre og derefter en gang til med linje to på linje fire. Bemærk brugen af trekant symbolet. For hver forudsætning til en regel eller sætning beskriver udtrykket efter et af trekantsymbolerne hvordan forudsætningen er overholdt. Fremover vil modus ponens dog istedet være repræsenteret ved symbolet ⊵ mellem de to forudsætninger.

4.2 Mendelson Lemma 3.2 (b)

I sit bevis for næste bevis benytter Mendelson følgende tautologi [\underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c}], men som det kan ses af beviset er der benyttet en lidt anden sætning. [M3.2(b) →^{pyk} “ lemma prime l three two b”][M3.2(b) →^{tex} “M3.2(b)”]

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

[M3.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}; L3.2(a)′ ≫ \underline{t} =^{p} \underline{t}; M1.10(b) ⊳ \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}⌉, p_{0}, c)]

Den afgørende observation her er at tautologien ovenfor essentielt svarer til M1.10(b), der udsiger [\underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊢ \underline{b} ⊢ \underline{a} ˙⇒ \underline{b}]. Som det kan ses af beviset er det netop denne regel der er benyttet den afsluttende linje. M1.10(b) opnås ved en enkelt anvendelse af deduktions sætningen (M1.9) på følgende trivielle sætning: [M1.10(b_{−}) →^{pyk} “mendelson corollary one ten pre b”][M1.10(b_{−}) →^{tex} “ M1.10(b -)”]

[M1.10(b_{−}) →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊢ \underline{b} ⊢ \underline{a} ⊢ \underline{c}]

[M1.10(b_{−}) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊢ \underline{b} ⊢ \underline{a} ⊢ MP′ ⊳ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊳ \underline{a} ≫ \underline{b} ˙⇒ \underline{c}; MP′ ⊳ \underline{b} ˙⇒ \underline{c} ⊳ \underline{b} ≫ \underline{c}⌉, p_{0}, c)]

Bemærk at jeg kalder sætningen M1.10(b_{−}) selv om den ikke er nævnt i Mendelson. Navnet skyldes at den svarer til M1.10(b) hvor M1.10(b) i stedet for den første forudsætning har en hypotese. Problemet er nu at M1.9 ikke bliver bevist formelt således at man uden videre kan introducere det på siden og rent faktisk gælder M1.9 ikke ubetinget for første ordens teorier. Til gengæeld præsenteres en betinget version for første ordens teorier, hvor der tages forbehold ved brugen af Gen i beviser: M2.5: Antag at der i et bevis for [\underline{b} ⊢ \underline{c}] ikke benyttes Gen på en linje som afhænger af [\underline{b}] således at den kvantifiserede variabel er en af [\underline{b}]s frie variable. Da eksisterer et bevis for [\underline{b} ˙⇒ \underline{c}] Hertil bemærkes at ovenstående bevis ikke benytter Gen og korollar 1.10 gælder derfor også i første ordens teorier.

Beviset er dog langt fra færdigt idet M2.5 ikke er et formelt bevis og derfor ikke uden videre kan inkluderes på siden. Beviset er derimod konstruktivt, dvs den skitserer en algoritme til at konvertere et bevis for en sætning med en forudsætning til et bevis, for en sætning med en tilsvarende hypotese.

4.2.1 Deduktions algoritmen

I første omgang beskrives den ’rå’ ufortolkede version af deduktionsalgoritmen. Indledningsvis ekspanderes alle beviser således at beviset udelukkende består af hypoteser, axiomer og de to regler. Deduktions algoritmen for at ændre en forudsætning til en hypotese [\underline{h}] forløber således, hvor de sætninger der refereres til følger umiddelbart efter:

• Hypotesen erstattes af 5 linjer der, viser at [\underline{h} ˙⇒ \underline{h}], hvor de 5 linjer svarer til beviset for [M1.7]

• En linje bestående af et axiom på formen [\underline{a}] erstattes af tre linjer, der viser at [\underline{h} ˙⇒ \underline{a}] med to linjer der svarer til [Tilføjhypotese] samt det oprindelige axiom.

• Tilsvarende erstattes en linje med modus ponens der virker ved [\underline{a} ˙⇒ \underline{b} ⊢ \underline{a} ⊢ \underline{b}] med 3 linjer, der udfører [\underline{h} ˙⇒ \underline{a} ˙⇒ \underline{b} ⊢ \underline{h} ˙⇒ \underline{a} ⊢ \underline{h} ˙⇒ \underline{b}] svarende til [MP′_{h}]..

• En linje med Gen erstattes af 3 linjer, der erstatter [ ˙∀\underline{x}: \underline{a}] med [\underline{h} ˙⇒ ˙∀\underline{x}: \underline{a}] svarende til [Gen′_{h}].

• For hver linje over hypotesen tilføjes 2 linjer svarende til [Tilføjhypotese].

Følgende fire sætninger stammer fra den oprindelige Peano side og er yderst anvendelige når man vil konvertere et bevis med forudsætninger til et bevis for en sætning med en forudsætning mindre. Lemma [M1.7 →^{pyk} “mendelson one seven”][M1.7 →^{tex} “ M1.7”], svarer til M1.7 og udsiger:

[M1.7 →^{stmt} S′ ⊢ ∀\underline{b}: \underline{b} ˙⇒ \underline{b}]

[M1.7 →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{b}: A1′ ≫ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b}; A2′ ≫ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b}; MP′ ⊳ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ⊳ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ≫ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b}; A1′ ≫ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b}; MP′ ⊳ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ⊳ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{b} ≫ \underline{b} ˙⇒ \underline{b}⌉, p_{0}, c)]

4.2.2 Hypothetitisk modus ponens

Hypotetisk modus ponens [MP′_{h} →^{pyk} “hypothetical rule prime mp”][MP′_{h} →^{tex} “ MP’ h”] tillader brugen af modus ponens ’bag’ en hypotese. Dvs. begge forudsætninger samt konklusionen har den samme hypotese.

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

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

Hvor de tre sidste linjer er dem, der blev nævnt i algoritmen.

4.2.3 Tilføj hypotese

Lemma [Tilføjhypotese →^{pyk} “hypothesize”][Tilføjhypotese →^{tex} “ Tilf\o j hypotese”] tillader som tilføje en vilkårlig hypotese til forudsætningen:

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

[Tilføjhypotese →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{a}: \underline{a} ⊢ A1′ ≫ \underline{a} ˙⇒ \underline{h} ˙⇒ \underline{a}; MP′ ⊳ \underline{a} ˙⇒ \underline{h} ˙⇒ \underline{a} ⊳ \underline{a} ≫ \underline{h} ˙⇒ \underline{a}⌉, p_{0}, c)]

De to nederste linjer samt forudgående instantiering af selve axiomet udgør de nævnte tre linjer

4.2.4 Hypotetisk generalisering

Hhypotetisk generalisering [Gen′_{h} →^{pyk} “hypothetical rule prime gen”][Gen′_{h} →^{tex} “ Gen’ h”] tillader som ved hypotetisk modus ponens at man kan benytte Gen′ ’bag’ en foranstående hypotese \underline{h}:

[Gen′_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{x}: ∀\underline{a}: ṅonfree(⌈\underline{x}⌉, ⌈\underline{h}⌉) ⊢⊢ \underline{h} ˙⇒ \underline{a} ⊢ \underline{h} ˙⇒ ˙∀\underline{x}: \underline{a}]

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

De tre sidste linjer er dem, der fremkommer af deduktions algoritmen.

4.2.5 Korollar M1.10b

Med disse redskaber kan vi nu returnere til beviset for [M1.10(b) →^{pyk} “mendelson corollary one ten b”][M1.10(b) →^{tex} “ M1.10(b)”]. Husk at beviset for M1.10(b_{−}) netop svarer til M1.10b bortset fra at konklusionens hypotese indgår som en forudsætning.

[M1.10(b) →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊢ \underline{b} ⊢ \underline{a} ˙⇒ \underline{c}]

Det resulterende bevis er oversat linje for linje fra M1.10(pre-b)med de ovenstående regler:

[M1.10(b) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊢ \underline{b} ⊢ Tilføjhypotese ⊳ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ≫ \underline{a} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c}; Tilføjhypotese⊳\underline{b} ≫ \underline{a} ˙⇒ \underline{b}; M1.7 ≫ \underline{a} ˙⇒ \underline{a}; MP′_{h}⊳\underline{a} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊳ \underline{a} ˙⇒ \underline{a} ≫ \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)]

Hvis man ikke tæller den enkelte define med er beviset nu blevet en linje længere for hver af de to resterende forudsætninger, men svarer ellers fuldstændig til det oprindelige. Det er dog værd at bemærke at eftersom [\underline{a}] er identisk med [\underline{h}] konkluderer den første modus ponens at [\underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c}] hvilket stadig haves som forudsætninger, hvilket gør linjen overflødig. Med beviset for M1.10(b) er beviset for M3.2(b) samtidig blevet afsluttet. Det kan sikkert virke på læseren som en unødvendigt detaljeret gennemgang af et ikke særligt kompliceret bevis, men metoden med brug af sætninger, der kun modificerer konklusionen og ikke hypotesen af et udsagn, viser sig helt uundværlig i de senere induktionsbeviser. Hvor Mendelson i sine beviser hver gang starter med en forudsætning som han til sidst ændrer til en hypotese ved brug af deduktions sætningen (M2.5), bliver man her nødt til at slæbe hypotesen med fra start til slut. Netop derfor er det afgørende at have de sætninger, der tillader at hypotesen kan ignoreres.

4.3 M3.2(c)

Den næste sætning, der bliver brug for minder i udpræget grad om axiom S1, men med termerne permuteret således at den ikke kan opnås ved en direkte anvendelse af axiomet: [M3.2(c) →^{pyk} “ lemma prime l three two c”][M3.2(c) →^{tex} “M3.2(c)”]

[M3.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}]

[M3.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}; M3.2(b) ≫ \underline{t} =^{p} \underline{r} ˙⇒ \underline{r} =^{p} \underline{t}; M1.10(a) ⊳ \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)]

Som det kan ses kan termerne i axiom S1 vælges således at den resulterende tautologi kun afviger fra det ønskede i den forreste hypotese. Desuden fortæller foregående sætning at den forreste hypotese er lig den forreste version. For at nå resultatet benyttes endnu et korollar M1.10(a). [M1.10(a) →^{pyk} “ mendelson corollary one ten a ”][M1.10(a) →^{tex} “M1.10(a)”]

[M1.10(a) →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ⊢ \underline{b} ˙⇒ \underline{c} ⊢ \underline{a} ˙⇒ \underline{c}]

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

Beviset konstrueres helt analogt til M1.10(b)

4.4 M3.2(d)

Ligesom foregående sætning minder M3.2(d) om axiom S1, men i dette tilfælde kan sætningen ikke instantieres fra de forudgående således at det kun er forreste hypotese der afviger fra det ønskede. Udgangspunktet for sætningen bliver M3.2(c) der instantieres således at konklusionen svarer til konklusionen for den ønskede sætning. Der har indsneget sig en mindre fejl i Mendelson idet beviset for M3.2(d) resulterer i [\underline{s} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s}], mens det han oprindelig kalder M3.2(d) er [\underline{r} =^{p} \underline{t} ˙⇒ \underline{s} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s}]. Sætningerne er essentielt forskellige dvs, man kan ikke bare instantiere den anden version ved at bytte om på termernes navne. Da de følgende resultater kræver begge versioner har jeg kaldt den sætning Mendelson får vist for M3.2(d)(I), mens sætningen som den bliver beskrevet indledningsvis er kaldt M3.2(d)(II).

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

[M3.2(d)(I) →^{pyk} “ lemma prime l three two d one”][M3.2(d)(I) →^{tex} “M3.2(d) (I)”]

[M3.2(d)(I) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: M3.2(c) ≫ \underline{r} =^{p} \underline{t} ˙⇒ \underline{t} =^{p} \underline{s} ˙⇒ \underline{r} =^{p} \underline{s}; M1.10(b_{+}) ⊳ \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}; M3.2(b) ≫ \underline{s} =^{p} \underline{t} ˙⇒ \underline{t} =^{p} \underline{s}; M1.10(a) ⊳ \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}⌉, p_{0}, c)]

Den helt afgørende linje i ovenstående bevis er nummer fem, hvor en ny version af korollar 1.10(b) benyttes (jeg har kaldt den korollar M1.10(b_{+}), selv om denne formulering af sætningen heller ikke findes i Mendelson). I den nye version a M1.10(b_{+}) er endnu en forudsætning fjernet og tilføjet som hypotese. At foregående version ikke er tilstrækkelig kan ses af at den bagerste hypotese ikke længere er en tautologi som i beviset for M3.2(b) (hvor man benyttede det allerede viste [\underline{t} =^{p} \underline{t}]) Beviset for korollar M1.10(b) indeholder ligesom beviset for M1.10(b_{−}) ikke nogen linjer der bruger Gen. Derfor kan vi uden bekymring bruge deduktions algoritmen endnu en gang, men spørgsmålet er nu hvorledes dette gøres nemmest. Problemet med deduktionsalgoritmen er at den ekspanderer et bevis ganske voldsomt. Et bevis med n linjer og en enkelt forudsætning, der skal fjernes vokser til et bevis med 3n+2 linjer og tilsvarende vil yderligere fjernelse af forudsætninger fåbeviset til at vokse med ca. en faktor tre. Men inspireret af beviset for M1.10(b), hvor der fandtes en metode til at oversætte beviset linje for linje til et bevis af essentielt samme størrelse, vil jeg nu forøge at generalisere metoden så jeg kan fjerne to forudsætninger uden at beviset vokser eller bliver ulæseligt Jeg har dog undladt Gen, da den ikke er nødvendig til beviset. Lemma [Tilføjhypotese_{+} →^{pyk} “hypothesize plus plus”][Tilføjhypotese_{+} →^{tex} “ Tilf\o j hypotese +”] tillader som tilføje en vilkårlig hypotese til forudsætningen [Tilføjhypotese_{+} →^{stmt} S′ ⊢ ∀\underline{i}: ∀\underline{h}: ∀\underline{a}: \underline{a} ⊢ \underline{i} ˙⇒ \underline{h} ˙⇒ \underline{a}]

[Tilføjhypotese_{+} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{i}: ∀\underline{h}: ∀\underline{a}: \underline{a} ⊢ Tilføjhypotese ⊳ \underline{a} ≫ \underline{h} ˙⇒ \underline{a}; Tilføjhypotese ⊳ \underline{h} ˙⇒ \underline{a} ≫ \underline{i} ˙⇒ \underline{h} ˙⇒ \underline{a}⌉, p_{0}, c)]

Ved ovenstående er der snydt lidt i den forstand at beviset ikke bygger på deduktions algoritmen. Beviset kan dog stadig uden videre generaliseres til flere hypoteser. Hypotetisk modus ponens [MP′_{h}+ →^{pyk} “hypothetical rule prime mp plus plus”][MP′_{h}+ →^{tex} “ MP’ h+”]

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

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

Modus ponens generaliserers umiddelbart til to hypoteser ved at konvertere beviset for modus ponens med en hypotese. Bemærk at beviset stadig ekspanderer med en enkelt linie, hvilket skyldes at axiom to ikke på forhånd er bevist i en hypotetisk udgave. Der er dog stadig ingen problemer med at beviset ekspanderer ukontrollabelt ved yderligere generalisering idet man ved endnu et gennemløb af algoritmen erstatter ’Tilføj hypotese’ med ’Tilføj hypotese+’. Det er knap så åbenlyst hvordan man introducerer forudsætning nummer to [\underline{b}] som en hypotese. Husk at hvis der i det oprindelige bevis er blevet benyttet [\underline{b}] vil der efter første gennemløb af algoritmen være en ’Tilføj hypotese’ der fortæller at [\underline{a} ˙⇒ \underline{b}]. Men når forudsætningen [\underline{b}] fjernes er ovenstående ikke længere sandt og hvor man i de øvrige tilfælde kan erstatte ’Tilføj hypotese’ med ’Tilføj hypotese+’ så er forudsætningen for brug af lemmaet ikke længere til stede. Algoritmen fungerer ikke desto mindre stadigvæk så det man skal huske er at fåhypoteserne introduceret korrekt. Hertil bruges: [M1.7_{+} →^{pyk} “mendelson one seven plus plus”][M1.7_{+} →^{tex} “ M1.7 +”].

[M1.7_{+} →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b}]

[M1.7_{+} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: M1.7 ≫ \underline{b} ˙⇒ \underline{b}; A1′ ≫ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b}; Tilføjhypotese ⊳ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b} ≫ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b}; MP′_{h} ⊳ \underline{b} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b} ⊳ \underline{b} ˙⇒ \underline{b} ≫ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b}⌉, p_{0}, c)] Hvor M1.7 bliver brugt til at introducere første hypotese bliver M1.7_{+} bliver brugt til at introducere hypotese nummer to. M1.7_{+} kan ligeledes generaliseres til flere hypoteser. Man skal dog være opmærksom på at mens de tre nederste linjer skal igennem algoritmen igen, så den tilsvarende regel med en hypotese mere, så skal linjen der instantierer M1.7 forblive uberørt. Ovenstående er et bevis for axiom A1 og kunne derfor nemt være undværet. Men hvor man ved to hypoteser får sætningen forærende vil man ved f.eks tre hypoteser skulle vise [\underline{c} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c}] som kan vises med udgangspunkt i M1.7++ . For nu at vende tilbage til udgangspunktet: Lemma [M1.10(b_{+}) →^{pyk} “mendelson corollary one ten b plus plus”][M1.10(b_{+}) →^{tex} “ M1.10(b +)”]

[M1.10(b_{+}) →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊢ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c}]

[M1.10(b_{+}) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊢ M1.7_{+} ≫ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b}; M1.7 ≫ \underline{a} ˙⇒ \underline{a}; Tilføjhypotese ⊳ \underline{a} ˙⇒ \underline{a} ≫ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{a}; Tilføjhypotese_{+} ⊳ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ≫ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c}; MP′_{h} + ⊳\underline{b} ˙⇒ \underline{a} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊳ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{a} ≫ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c}; MP′_{h} + ⊳\underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ⊳ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b} ≫ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c}⌉, p_{0}, c)]

Hermed er beviset for sætning M3.2(d)(I). Sætning M3.2(d)(II) følger umiddelbart:

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

[M3.2(d)(II) →^{pyk} “ lemma prime l three two d two”][M3.2(d)(II) →^{tex} “M3.2(d) (II)”]

[M3.2(d)(II) →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: M3.2(d)(I) ≫ \underline{s} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s}; M1.10(b_{+}) ⊳ \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)]

De beviste sætninger giver os nu følgende fundamentale egenskaber ved lighed:

• M3.2(a): refleksivitet

• M3.2(b): symmetri

• M3.2(c+d): transitivitet (delvis, men tilstrækkeligt til vores formål)

4.5 Flere hypotetiske lemmaer

Jeg kan allerede nu afsløre at der ikke kommer flere sætninger, hvor håndtering af to hypoteser er nødvendigt. Til gengæld vil der være flittig brug af sæningerne, der håndterer en enkelt hypotese. Dertil vil følgende simple sætninger hjælpe med at holde beviserne korte og overskuelige idet man slipper for at instantiere ’Tilføj hypotese’ hver gang man instantierer et lemma eller axiom. [M3.2(a)_{h} →^{pyk} “hypothetical three two a”][M3.2(a)_{h} →^{tex} “ M3.2(a) h”] [M3.2(a)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{t}] [M3.2(a)_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{t}: L3.2(a)′ ≫ \underline{t} =^{p} \underline{t}; Tilføjhypotese ⊳ \underline{t} =^{p} \underline{t} ≫

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

[M3.2(b)_{h} →^{pyk} “hypothetical three two b”][M3.2(b)_{h} →^{tex} “ M3.2(b) h”] [M3.2(b)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{r} =^{p} \underline{t}][M3.2(b)_{h} →^{proof} Rule tactic] [M3.2(b)_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ S1′ ≫ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t}; Tilføjhypotese ⊳ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ≫ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t}; MP′_{h} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ≫ \underline{h} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t}; M3.2(a)_{h} ≫ \underline{h} ˙⇒ \underline{t} =^{p} \underline{t}; MP′_{h} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{t} ≫ \underline{h} ˙⇒ \underline{r} =^{p} \underline{t}⌉, p_{0}, c)] [M3.1(S2′)_{h} →^{pyk} “hypothetical three one s two”][M3.1(S2′)_{h} →^{tex} “ M3.1(S2’) h”] [M3.1(S2′)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{t}′ =^{p} \underline{r}′] [M3.1(S2′)_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ S2′ ≫ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t}′ =^{p} \underline{r}′; Tilføjhypotese ⊳ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t}′ =^{p} \underline{r}′ ≫ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t}′ =^{p} \underline{r}′; MP′_{h} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t}′ =^{p} \underline{r}′ ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ≫ \underline{h} ˙⇒ \underline{t}′ =^{p} \underline{r}′⌉, p_{0}, c)] [M3.1(S1′)_{h} →^{pyk} “hypothetical three one s one”][M3.1(S1′)_{h} →^{tex} “ M3.1(S1’) h”] [M3.1(S1′)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{t} =^{p} \underline{s} ⊢ \underline{h} ˙⇒ \underline{r} =^{p} \underline{s}] [M3.1(S1′)_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{t} =^{p} \underline{s} ⊢ S1′ ≫ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{s} ˙⇒ \underline{r} =^{p} \underline{s}; Tilføjhypotese ⊳ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{s} ˙⇒ \underline{r} =^{p} \underline{s} ≫ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{s} ˙⇒ \underline{r} =^{p} \underline{s}; MP′_{h} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{s} ˙⇒ \underline{r} =^{p} \underline{s} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ≫ \underline{h} ˙⇒ \underline{t} =^{p} \underline{s} ˙⇒ \underline{r} =^{p} \underline{s}; MP′_{h} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{s} ˙⇒ \underline{r} =^{p} \underline{s} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{s} ≫ \underline{h} ˙⇒ \underline{r} =^{p} \underline{s}⌉, p_{0}, c)] [M3.2(c)_{h} →^{pyk} “hypothetical three two c”][M3.2(c)_{h} →^{tex} “ M3.2(c) h”] [M3.2(c)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{r} =^{p} \underline{s} ⊢ \underline{h} ˙⇒ \underline{t} =^{p} \underline{s}] [M3.2(c)_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{r} =^{p} \underline{s} ⊢ M3.2(c) ≫ \underline{t} =^{p} \underline{r} ˙⇒ \underline{r} =^{p} \underline{s} ˙⇒ \underline{t} =^{p} \underline{s}; Tilføjhypotese ⊳ \underline{t} =^{p} \underline{r} ˙⇒ \underline{r} =^{p} \underline{s} ˙⇒ \underline{t} =^{p} \underline{s} ≫ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ˙⇒ \underline{r} =^{p} \underline{s} ˙⇒ \underline{t} =^{p} \underline{s}; MP′_{h} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ˙⇒ \underline{r} =^{p} \underline{s} ˙⇒ \underline{t} =^{p} \underline{s} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ≫ \underline{h} ˙⇒ \underline{r} =^{p} \underline{s} ˙⇒ \underline{t} =^{p} \underline{s}; MP′_{h} ⊳ \underline{h} ˙⇒ \underline{r} =^{p} \underline{s} ˙⇒ \underline{t} =^{p} \underline{s} ⊳ \underline{h} ˙⇒ \underline{r} =^{p} \underline{s} ≫ \underline{h} ˙⇒ \underline{t} =^{p} \underline{s}⌉, p_{0}, c)]

[M3.1(S5′)_{h} →^{pyk} “hypothetical three one s five”][M3.1(S5′)_{h} →^{tex} “ M3.1(S5’) h”]

[M3.1(S5′)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: \underline{h} ˙⇒ \underline{t} ˙+ ˙0 =^{p} \underline{t}]

[M3.1(S5′)_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{t}: S5′ ≫ \underline{t} ˙+ ˙0 =^{p} \underline{t}; Tilføjhypotese ⊳ \underline{t} ˙+ ˙0 =^{p}

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

[M3.1(S6′)_{h} →^{pyk} “hypothetical three one s six”][M3.1(S6′)_{h} →^{tex} “ M3.1(S6’) h”]

[M3.1(S6′)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: \underline{h} ˙⇒ \underline{t} ˙+ \underline{r}′ =^{p} \underline{t} ˙+ \underline{r}′]

[M3.1(S6′)_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: S6′ ≫ \underline{t} ˙+ \underline{r}′ =^{p} \underline{t} ˙+ \underline{r}′; Tilføjhypotese ⊳ \underline{t} ˙+ \underline{r}′ =^{p} \underline{t} ˙+ \underline{r}′ ≫ \underline{h} ˙⇒ \underline{t} ˙+ \underline{r}′ =^{p} \underline{t} ˙+ \underline{r}′⌉, p_{0}, c)]

[M3.2(d)_{h} →^{pyk} “ hypothetical three two d”][M3.2(d)_{h} →^{tex} “M3.2(d) h”]

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

[M3.2(d)_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: \underline{h} ˙⇒ \underline{r} =^{p} \underline{t} ⊢ \underline{h} ˙⇒ \underline{s} =^{p} \underline{t} ⊢ M3.2(d)(I) ≫ \underline{s} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s}; Tilføjhypotese ⊳ \underline{s} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s} ≫ \underline{h} ˙⇒ \underline{s} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s}; MP′_{h} ⊳ \underline{h} ˙⇒ \underline{s} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s} ⊳ \underline{h} ˙⇒ \underline{s} =^{p} \underline{t} ≫ \underline{h} ˙⇒ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s}; MP′_{h} ⊳ \underline{h} ˙⇒ \underline{r} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{s} ⊳ \underline{h} ˙⇒ \underline{r} =^{p} \underline{t} ≫ \underline{h} ˙⇒ \underline{r} =^{p} \underline{s}⌉, p_{0}, c)]

Flere af de ovenstående sætninger afviger fra den oprindelige version ved at de har erstattet hypoteser med forudsætninger. Dette giver mening i de kommende lange beviser idet man for hver forudsætning sparer den modus ponens der skal til for at fjerne en hypotese. Det kræver til gengæld at forudsætningerne er bevist.

4.6 Lemma M3.2(h)(I)

Nu er fundamentet lagt til at induktions beviset kan på begyndes. Som sagt ønskes sætningen [ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ] bevist for alle x og y. For at følge Mendelson vil beviset derfor blive ført i tre trin ved induktion over ẏ. [M3.2(h)(I) →^{pyk} “ lemma prime l three two h one”][M3.2(h)(I) →^{tex} “M3.2(h) (I)”]

[M3.2(h)(I) →^{stmt} S′ ⊢ ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ] [M3.2(h)(I) →^{proof} λc.λx.P(⌈S′ ⊢ S5′ ≫ ẋ ˙+ ˙0 =^{p} ẋ; M3.2(f) ≫ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ; A4′ @ ẋ ≫ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ẋ =^{p} ˙0 ˙+ ẋ; MP′ ⊳ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ẋ =^{p} ˙0 ˙+ ẋ ⊳ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ≫ ẋ =^{p} ˙0 ˙+ ẋ; M3.2(c) ≫ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ =^{p} ˙0 ˙+ ẋ ˙⇒ ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ; MP′ ⊳ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ =^{p} ˙0 ˙+ ẋ ˙⇒ ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ ⊳ ẋ ˙+ ˙0 =^{p} ẋ ≫ ẋ =^{p} ˙0 ˙+ ẋ ˙⇒ ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ; MP′ ⊳ ẋ =^{p} ˙0 ˙+ ẋ ˙⇒ ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ ⊳ ẋ =^{p} ˙0 ˙+ ẋ ≫ ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ⌉, p_{0}, c)]

Bemærk at der ikke længere benyttes termer (repræsenteret ved metavariable), men konkrete variable hvilket skyldes at axiom S9 ikke er gyldigt for vilkårlige termer. Som det kan ses giver det nogle ekstra linjer i beviset når et resultat for en konkret variabel skal konverteres til det tilsvarende resultat for en anden variabel. Der mangler stadig resultatet for M3.2(f): [M3.2(f) →^{pyk} “mendelson three two f”][M3.2(f) →^{tex} “ M3.2(f)”]

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

[M3.2(f) →^{proof} λc.λx.P(⌈S′ ⊢ A1′ ≫ x ˙⇒ x ˙⇒ x; M3.1(S5′)_{h} ≫ x ˙⇒ x ˙⇒ x ˙⇒ ˙0 ˙+ ˙0 =^{p} ˙0; M3.2(b)_{h} ⊳ x ˙⇒ x ˙⇒ x ˙⇒ ˙0 ˙+ ˙0 =^{p} ˙0 ≫ x ˙⇒ x ˙⇒ x ˙⇒ ˙0 =^{p} ˙0 ˙+ ˙0; MP′ ⊳ x ˙⇒ x ˙⇒ x ˙⇒ ˙0 =^{p} ˙0 ˙+ ˙0 ⊳ x ˙⇒ x ˙⇒ x ≫ ˙0 =^{p} ˙0 ˙+ ˙0; M1.7 ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ; M3.1(S2′)_{h} ⊳ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′; M3.1(S6′)_{h} ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p} ˙0 ˙+ ṫ′; M3.2(b)_{h} ⊳ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p} ˙0 ˙+ ṫ′ ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p} ˙0 ˙+ ṫ′; M3.2(c)_{h} ⊳ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ⊳ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p} ˙0 ˙+ ṫ′ ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′; Gen′⊳ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ≫ ˙∀ṫ: ṫ =^{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)]

M3.2(f) er et fuldt induktionsbevis, hvor der i første del udnyttes refleksivitet af lighed og i anden del transitivitet af lighed. Induktions axiomet bliver først instantieret mod slutningen efter at begge dets hypoteser er bevist som tautologier. Linje 7-11 illustrerer brugen af den teknik, der tillader at føre formelle beviser uden referencer til deduktions sætningen og uden at ødelægge bevisets overskuelighed. Den lidt spøjse brug af [\underline{z}] i starten af beviset skyldes at beviset stammer fra den oprindelige Peano side hvor M3.2(b) kun var vist i en hypotetisk udgave. Der tilføjes derfor en vilkårlig tautologi før sætningen bruges for derefter at blive smidt væk. Med M3.2(f) fuldstændiggør første del af beviset for kommutativet, nemlig det simple tilfælde hvor [ẏ] er [˙0].

4.7 Lemma M3.2(g)

Inden M3.2(h) kan afsluttes er der brug for et sidste, men ganske omfattende induktionsbevis: [M3.2(g) →^{pyk} “ lemma prime l three two g”][M3.2(g) →^{tex} “M3.2(g)”]

[M3.2(g) →^{stmt} S′ ⊢ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′]

[M3.2(g) →^{proof} λc.λx.P(⌈S′ ⊢ S5′ ≫ ẏ′ ˙+ ˙0 =^{p} ẏ′; S5′ ≫ ẏ ˙+ ˙0 =^{p} ẏ; S2′ ≫ ẏ ˙+ ˙0 =^{p} ẏ ˙⇒ ẏ ˙+ ˙0′ =^{p} ẏ′; MP′ ⊳ ẏ ˙+ ˙0 =^{p} ẏ ˙⇒ ẏ ˙+ ˙0′ =^{p} ẏ′ ⊳ ẏ ˙+ ˙0 =^{p} ẏ ≫ ẏ ˙+ ˙0′ =^{p} ẏ′; M3.2(d)(II) ≫ ẏ′ ˙+ ˙0 =^{p} ẏ′ ˙⇒ ẏ ˙+ ˙0′ =^{p} ẏ′ ˙⇒ ẏ′ ˙+ ˙0 =^{p} ẏ ˙+ ˙0′; MP′ ⊳ ẏ′ ˙+ ˙0 =^{p}

ẏ′ ˙⇒ ẏ ˙+ ˙0′ =^{p} ẏ′ ˙⇒ ẏ′ ˙+ ˙0 =^{p} ẏ ˙+ ˙0′ ⊳ ẏ′ ˙+ ˙0 =^{p} ẏ′ ≫ ẏ ˙+ ˙0′ =^{p} ẏ′ ˙⇒ ẏ′ ˙+ ˙0 =^{p}

ẏ ˙+ ˙0′; MP′ ⊳ ẏ ˙+ ˙0′ =^{p} ẏ′ ˙⇒ ẏ′ ˙+ ˙0 =^{p} ẏ ˙+ ˙0′ ⊳ ẏ ˙+ ˙0′ =^{p} ẏ′ ≫ ẏ′ ˙+ ˙0 =^{p}

ẏ ˙+ ˙0′; M1.7 ≫ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′; M3.1(S6′)_{h} ≫ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ′ ˙+ ẋ′; M3.1(S2′)_{h} ⊳ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ≫ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′′; M3.2(c)_{h} ⊳ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ′ ˙+ ẋ′ ⊳ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′′ ≫ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′′; M3.1(S6′)_{h} ≫ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′; M3.1(S2′)_{h} ⊳ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′ ≫ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ ˙+ ẋ′′ =^{p} ẏ ˙+ ẋ′′; M3.2(d)_{h} ⊳ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′′ ⊳ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ ˙+ ẋ′′ =^{p} ẏ ˙+ ẋ′′ ≫ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′′; S9′ ≫ ẏ′ ˙+ ˙0 =^{p} ẏ ˙+ ˙0′ ˙⇒ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′′ ˙⇒ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′; MP′ ⊳ ẏ′ ˙+ ˙0 =^{p} ẏ ˙+ ˙0′ ˙⇒ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′′ ˙⇒ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ⊳ ẏ′ ˙+ ˙0 =^{p} ẏ ˙+ ˙0′ ≫ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′′ ˙⇒ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′; Gen′ ⊳ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′′ ≫ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′′; MP′ ⊳ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′′ ˙⇒ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ⊳ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ′ =^{p} ẏ ˙+ ẋ′′ ≫ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′; A4′ @ ẋ ≫ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′; MP′ ⊳ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ˙⇒ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ⊳ ˙∀ẋ: ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ≫ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′⌉, p_{0}, c)]

Ligesom i M3.2 (f) er det transitivitets sætningerne, der binder de forskellige linjer sammen i beviset mens udsagnene der kombineres i dette bevis stammer fra axiomerne S2, S5 og S6. Jeg har med vilje byttet om på variablene x og y i forhold til Mendelsons formulering idet M3.2(h)(II) bruger sætningen i den formulering. Jeg slipper derfor for at bruge Gen og A4 til at skifte variable.

4.8 Lemma M3.2(h)(II)

Nu kan den sidste hypotese i induktionen bevises. Med udgangspunkt i axiom S6 og forrige resultat kan beviset strikkes sammen ved symmetri og transitivitets sætningerne: [M3.2(h)(II) →^{pyk} “ lemma prime l three two h two”][M3.2(h)(II) →^{tex} “M3.2(h) (II)”]

[M3.2(h)(II) →^{stmt} S′ ⊢ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ′ ˙+ ẋ] [M3.2(h)(II) →^{proof} λc.λx.P(⌈S′ ⊢ M1.7 ≫ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ; M3.1(S6′)_{h} ≫ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẋ ˙+ ẏ′; M3.2(g) ≫ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′; Tilføjhypotese ⊳ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ≫ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′; M3.1(S2′)_{h} ⊳ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ≫ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ ˙+ ẋ′; M3.2(c)_{h} ⊳ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẋ ˙+ ẏ′ ⊳ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ ˙+ ẋ′ ≫ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ ˙+ ẋ′; M3.2(d)_{h} ⊳ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ ˙+ ẋ′ ⊳ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẏ′ ˙+ ẋ =^{p} ẏ ˙+ ẋ′ ≫ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ′ ˙+ ẋ⌉, p_{0}, c)]

4.9 Lemma M3.2(h)

[M3.2(h) →^{pyk} “ lemma prime l three two h”][M3.2(h) →^{tex} “M3.2(h)”]

[M3.2(h) →^{stmt} S′ ⊢ ˙∀ẋ: ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ]

[M3.2(f) →^{pyk} “ lemma prime l three two f”][M3.2(f) →^{tex} “M3.2(f)”] Nu kan brikkerne samles ved en sidste gang at instantiere S9:

[M3.2(h) →^{proof} λc.λx.P(⌈S′ ⊢ S9′ ≫ ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ ˙⇒ ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ′ ˙+ ẋ ˙⇒ ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ; M3.2(h)(I) ≫ ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ; M3.2(h)(II) ≫ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ′ ˙+ ẋ; Gen′ ⊳ ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ′ ˙+ ẋ ≫ ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ′ ˙+ ẋ; MP′ ⊳ ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ ˙⇒ ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ′ ˙+ ẋ ˙⇒ ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ⊳ ẋ ˙+ ˙0 =^{p} ˙0 ˙+ ẋ ≫ ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ′ ˙+ ẋ ˙⇒ ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ; MP′ ⊳ ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ′ ˙+ ẋ ˙⇒ ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ⊳ ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ˙⇒ ẋ ˙+ ẏ′ =^{p} ẏ′ ˙+ ẋ ≫ ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ; Gen′ ⊳ ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ ≫ ˙∀ẋ: ˙∀ẏ: ẋ ˙+ ẏ =^{p} ẏ ˙+ ẋ⌉, p_{0}, c)]

Beviset er afsluttet og siden godkendt af Logiweb serveren.

5 Konklusion

Beviset er i hovedtræk gennemført som beskrevet i Mendelson, men hvor Mendelson bruger deduktions sætningen (M2.5) som garanti for eksistensen af et bevis, har kravet til denne opgave været konstruktionen af et sådant bevis. Derfor er der to grundlæggende strategier, man kan følge: Implementer et program, der konstruerer et bevis med hypoteser udfra et bevis med forudsætninger. Jeg er overbevist om at dette kan lade sig gøre inden for Logiweb systemet, men vil kræve at man benytter væsentlig mere kompliceret og grundlæggende funktionalitet i systemet end det er der er benyttet til denne side. Alternativt kan man som illustreret i rapporten hvorledes man udleder sætningerne, med udgangspunkt i den konstruktive algoritme bag M2.5. Ved omhyggeligt at konstruere hjælpesætninger baseret på deduktions algoritmen kan man manuelt modificere sine beviser uden at de bliver uoverskuelige eller eksploderer i størrelse.

A Pyk definitioner

A.1 Sidens navn

[proofreport →^{pyk} “proofreport”]

A.2 Modus ponens

[x ⊵_{h} y →^{pyk} “∗ hypothetical modus ponens ∗”][x ⊵_{h} y →^{tex} “#1. \unrhd h #2.”]

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

[x ⊵ y →^{pyk} “∗ macro modus ponens ∗”][x ⊵ y →^{tex} “#1. \unrhd #2.”]

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

A.3 Variable

[ẋ →^{pyk} “∗ peano var”][ẋ →^{tex} “ \dot{#1. }”] [x^{P} →^{pyk} “∗ is peano var”][x^{P} →^{tex} “#1. {} ˆ {\cal P}”]

[x^{P} →^{val} x =^{r} ⌈ẋ⌉]

[ȧ →^{pyk} “peano a”][ȧ →^{tex} “ \dot{\mathit{a}}”]

[ȧ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ȧ ¨= ȧ]⌉)]

A.4 free og nonefree

[ṅonfree(x, y) →^{pyk} “peano nonfree ∗ in ∗ end nonfree”][ṅonfree(x, y) →^{tex} “ \dot{nonfree}(#1. , #2. )”] [ṅonfree^{∗}(x, y) →^{pyk} “peano nonfree star ∗ in ∗ end nonfree”][ṅonfree^{∗}(x, y) →^{tex} “ \dot{nonfree}ˆ ∗(#1. , #2. )”]

[ṅonfree(x, y) →^{val}

If(y^{P}, ¬x =^{t} y,

If(¬y =^{r} ⌈ ˙∀x: y⌉, ṅonfree^{∗}(x, y^{t}), If(x =^{t} y^{1}, T, ṅonfree(x, y^{2}))))]

[ṅonfree^{∗}(x, y) →^{val} x!If(y, T, If(ṅonfree(x, y^{h}), ṅonfree^{∗}(x, y^{t}), F))]

[ḟree⟨a|x := b⟩ →^{pyk} “peano free ∗ set ∗ to ∗ end free”][ḟree⟨a|x := b⟩ →^{tex} “ \dot{free}\langle #1. | #2. := #3. \rangle”] [ḟree^{∗}⟨a|x := b⟩ →^{pyk} “peano free star ∗ set ∗ to ∗ end free”][ḟree^{∗}⟨a|x := b⟩ →^{tex} “ \dot{free}{}ˆ ∗\langle #1. | #2. := #3. \rangle”] [a]

[ḟree⟨a|x := b⟩ →^{val} x!b!

If(a^{P}, T,

If(¬a =^{r} ⌈ ˙∀u: v⌉, ḟree^{∗}⟨a^{t}|x := b⟩,

If(a^{1} =^{t} x, T,

If(ṅonfree(x, a^{2}), T, If(¬ṅonfree(a^{1}, b), F, ḟree⟨a^{2}|x := b⟩)))))]

[ḟree^{∗}⟨a|x := b⟩ →^{val} x!b!If(a, T, If(ḟree⟨a^{h}|x := b⟩, ḟree^{∗}⟨a^{t}|x := b⟩, F))]

[a≡⟨b|x := c⟩ →^{pyk} “peano sub ∗ is ∗ where ∗ is ∗ end sub”][a≡⟨b|x := c⟩ →^{tex} “#1. {\equiv}\langle #2. |#3. :=#4. \rangle”] [a≡⟨^{∗}b|x := c⟩ →^{pyk} “peano sub star ∗ is ∗ where ∗ is ∗ end sub”][a≡⟨^{∗}b|x := c⟩ →^{tex} “#1. {\equiv}\langleˆ ∗ #2. |#3. :=#4. \rangle”]

[a≡⟨b|x := c⟩ →^{val} a!x!c!
If(If(b =^{r} ⌈ ˙∀u: v⌉, b^{1} =^{t} x, F), a =^{t} b,
If(b^{P} ∧ b =^{t} x, a =^{t} c, If(
a =^{r} b, a^{t}≡⟨^{∗}b^{t}|x := c⟩, F)))]
[a≡⟨^{∗}b|x := c⟩ →^{val} b!x!c!If(a, T, If(a^{h}≡⟨b^{h}|x := c⟩, a^{t}≡⟨^{∗}b^{t}|x := c⟩, F))]

A.5 Variables of Peano arithmetic

[ḃ →^{pyk} “peano b”][ḃ →^{tex} “ \dot{\mathit{b}}”], [ċ →^{pyk} “peano c”][ċ →^{tex} “ \dot{\mathit{c}}”], [ḋ →^{pyk} “peano d”][ḋ →^{tex} “ \dot{\mathit{d}}”], [ė →^{pyk} “peano e”][ė →^{tex} “ \dot{\mathit{e}}”], [ḟ →^{pyk} “peano f”][ḟ →^{tex} “ \dot{\mathit{f}}”], [ġ →^{pyk} “peano g”][ġ →^{tex} “ \dot{\mathit{g}}”], [ḣ →^{pyk} “peano h”][ḣ →^{tex} “ \dot{\mathit{h}}”], [i̇ →^{pyk} “peano i”][i̇ →^{tex} “ \dot{\mathit{i}}”], [j̇ →^{pyk} “peano j”][j̇ →^{tex} “ \dot{\mathit{j}}”], [k̇ →^{pyk} “peano k”][k̇ →^{tex} “ \dot{\mathit{k}}”], [l̇ →^{pyk} “peano l”][l̇ →^{tex} “ \dot{\mathit{l}}”], [ṁ →^{pyk} “peano m”][ṁ →^{tex} “ \dot{\mathit{m}}”], [ṅ →^{pyk} “peano n”][ṅ →^{tex} “ \dot{\mathit{n}}”], [ȯ →^{pyk} “peano o”][ȯ →^{tex} “ \dot{\mathit{o}}”], [ṗ →^{pyk} “peano p”][ṗ →^{tex} “ \dot{\mathit{p}}”], [q̇ →^{pyk} “peano q”][q̇ →^{tex} “ \dot{\mathit{q}}”], [ṙ →^{pyk} “peano r”][ṙ →^{tex} “ \dot{\mathit{r}}”], [ṡ →^{pyk} “peano s”][ṡ →^{tex} “ \dot{\mathit{s}}”], [ṫ →^{pyk} “peano t”][ṫ →^{tex} “ \dot{\mathit{t}}”], [u̇ →^{pyk} “peano u”][u̇ →^{tex} “ \dot{\mathit{u}}”], [v̇ →^{pyk} “peano v”][v̇ →^{tex} “ \dot{\mathit{v}}”], [ẇ →^{pyk} “peano w”][ẇ →^{tex} “ \dot{\mathit{w}}”], [ẋ →^{pyk} “peano x”][ẋ →^{tex} “ \dot{\mathit{x}}”], [ẏ →^{pyk} “peano y”][ẏ →^{tex} “ \dot{\mathit{y}}”] [ż →^{pyk} “peano z”][ż →^{tex} “ \dot{\mathit{z}}”] [ḃ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ḃ ¨= ḃ]⌉)], [ċ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ċ ¨= ċ]⌉)], [ḋ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ḋ ¨= ḋ]⌉)], [ė →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ė ¨= ė]⌉)], [ḟ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ḟ ¨= ḟ]⌉)], [ġ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ġ ¨= ġ]⌉)], [ḣ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ḣ ¨= ḣ]⌉)], [i̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[i̇ ¨= i̇]⌉)], [j̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[j̇ ¨= j̇]⌉)], [k̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[k̇ ¨= k̇]⌉)], [l̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[l̇ ¨= l̇]⌉)], [ṁ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṁ ¨= ṁ]⌉)], [ṅ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṅ ¨= ṅ]⌉)], [ȯ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ȯ ¨= ȯ]⌉)], [ṗ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṗ ¨= ṗ]⌉)], [q̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[q̇ ¨= q̇]⌉)], [ṙ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṙ ¨= ṙ]⌉)], [ṡ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṡ ¨= ṡ]⌉)], [ṫ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṫ ¨= ṫ]⌉)], [u̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[u̇ ¨= u̇]⌉)], [v̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[v̇ ¨= v̇]⌉)], [ẇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ẇ ¨= ẇ]⌉)], [ẋ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ẋ ¨= ẋ]⌉)], [ẏ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ẏ ¨= ẏ]⌉)], [ż →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ż ¨= ż]⌉)].

A.6 TEX definitions

A.7 Test

A.8 Priority table

[proofreport →^{prio} Preassociative [proofreport], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [math ∗ end math], [flush left [∗]], [x], [y], [z], [[∗ ▷◁ ∗]], [[∗ →^{∗} ∗]], [pyk], [tex], [name], [prio], [∗], [T], [if(∗, ∗, ∗)], [[∗ ⇒^{∗} ∗]], [val], [claim], [⊥], [f(∗)], [(∗)^{I}], [F], [\underline{0}], [\underline{1}], [\underline{2}], [\underline{3}], [\underline{4}], [\underline{5}], [\underline{6}], [\underline{7}], [\underline{8}], [\underline{9}], [0], [1], [2], [3], [4], [5], [6], [7], [8], [9], [a], [b], [c], [d], [e], [f], [g], [h], [i], [j], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [(∗)^{M}], [If(∗, ∗, ∗)], [array{∗} ∗ end array], [l], [c], [r], [empty], [⟨∗ | ∗:= ∗⟩], [M(∗)], [Ũ(∗)], [U(∗)], [U^{M}(∗)], [apply(∗, ∗)], [apply_{1}(∗, ∗)], [identifier(∗)], [identifier_{1}(∗, ∗)], [arrayplus(∗, ∗)], [array-remove(∗, ∗, ∗)], [array-put(∗, ∗, ∗, ∗)], [array-add(∗, ∗, ∗, ∗, ∗)], [bit(∗, ∗)], [bit_{1}(∗, ∗)], [rack], ["vector"], ["bibliography"], ["dictionary"], ["body"], ["codex"], ["expansion"], ["code"], ["cache"], ["diagnose"], ["pyk"], ["tex"], ["texname"], ["value"], ["message"], ["macro"], ["definition"], ["unpack"], ["claim"], ["priority"], ["lambda"], ["apply"], ["true"], ["if"], ["quote"], ["proclaim"], ["define"], ["introduce"], ["hide"], ["pre"], ["post"], [E(∗, ∗, ∗)], [E_{2}(∗, ∗, ∗, ∗, ∗)], [E_{3}(∗, ∗, ∗, ∗)], [E_{4}(∗, ∗, ∗, ∗)], [lookup(∗, ∗, ∗)], [abstract(∗, ∗, ∗, ∗)], [⌈∗⌉], [M(∗, ∗, ∗)], [M_{2}(∗, ∗, ∗, ∗)], [M^{∗}(∗, ∗, ∗)], [macro], [s_{0}], [zip(∗, ∗)], [assoc_{1}(∗, ∗, ∗)], [(∗)^{p}], [self], [[∗ ¨= ∗]], [[∗ ˙= ∗]], [[∗ ´= ∗]], [[∗ =^{pyk} ∗]], [[∗ =^{tex} ∗]], [[∗ =^{name} ∗]], [Priority table[∗]], [M̃_{1}], [M̃_{2}(∗)], [M̃_{3}(∗)], [M̃_{4}(∗, ∗, ∗, ∗)], [M̃(∗, ∗, ∗)], [Q̃(∗, ∗, ∗)], [Q̃_{2}(∗, ∗, ∗)], [Q̃_{3}(∗, ∗, ∗, ∗)], [Q̃^{∗}(∗, ∗, ∗)], [(∗)], [aspect(∗, ∗)], [aspect(∗, ∗, ∗)], [⟨∗⟩], [tuple_{1}(∗)], [tuple_{2}(∗)], [let_{2}(∗, ∗)], [let_{1}(∗, ∗)], [[∗ =^{claim} ∗]], [checker], [check(∗, ∗)], [check_{2}(∗, ∗, ∗)], [check_{3}(∗, ∗, ∗)], [check^{∗}(∗, ∗)], [check_{2}^{∗}(∗, ∗, ∗)], [[∗]^{·}], [[∗]^{−}], [[∗]^{∘}], [msg], [[∗ =^{msg} ∗]], [<stmt>], [stmt], [[∗ =^{stmt} ∗]], [HeadNil′], [HeadPair′], [Transitivity′], [⊥ ⊥], [Contra′], [T′_{E}], [L_{1}], [\underline{∗}], [A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N], [O], [P], [Q], [R], [S], [T ], [U], [V], [W], [X], [Y], [Z], [⟨∗ | ∗:= ∗⟩], [⟨^{∗}∗ | ∗:= ∗⟩], [∅], [Remainder], [(∗)^{v}], [intro(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗)], [error(∗, ∗)], [error_{2}(∗, ∗)], [proof(∗, ∗, ∗)], [proof_{2}(∗, ∗)], [S(∗, ∗)], [S^{I}(∗, ∗)], [S^{⊳} (∗, ∗)], [S_{1}^{⊳} (∗, ∗, ∗)], [S^{E}(∗, ∗)], [S_{1}^{E}(∗, ∗, ∗)], [S^{+}(∗, ∗)], [S_{1}^{+}(∗, ∗, ∗)], [S^{−}(∗, ∗)], [S_{1}^{−}(∗, ∗, ∗)], [S^{∗}(∗, ∗)], [S_{1}^{∗}(∗, ∗, ∗)], [S_{2}^{∗}(∗, ∗, ∗, ∗)], [S^{@}(∗, ∗)], [S_{1}^{@}(∗, ∗, ∗)], [S^{⊢}(∗, ∗)], [S_{1}^{⊢}(∗, ∗, ∗, ∗)], [S⊢ ⊢(∗, ∗)],

[S⊢ ⊢ ; 1(∗, ∗, ∗, ∗)], [S^{i.e.}(∗, ∗)], [S_{1}^{i.e.}(∗, ∗, ∗, ∗)], [S_{2}^{i.e.}(∗, ∗, ∗, ∗, ∗)], [S^{∀}(∗, ∗)],

[S_{1}^{∀}(∗, ∗, ∗, ∗)], [S^{;}(∗, ∗)], [S_{1}^{;}(∗, ∗, ∗)], [S_{2}^{;}(∗, ∗, ∗, ∗)], [T (∗)], [claims(∗, ∗, ∗)], [claims_{2}(∗, ∗, ∗)], [<proof>], [proof], [[Lemma ∗: ∗]], [[Proof of ∗: ∗]], [[∗ lemma ∗: ∗]], [[∗ antilemma ∗: ∗]], [[∗ rule ∗: ∗]], [[∗ antirule ∗: ∗]], [verifier], [V_{1}(∗)], [V_{2}(∗, ∗)], [V_{3}(∗, ∗, ∗, ∗)], [V_{4}(∗, ∗)], [V_{5}(∗, ∗, ∗, ∗)], [V_{6}(∗, ∗, ∗, ∗)], [V_{7}(∗, ∗, ∗, ∗)], [Cut(∗, ∗)], [Head_{⊕}(∗)], [Tail_{⊕}(∗)], [rule_{1}(∗, ∗)], [rule(∗, ∗)], [Rule tactic], [Plus(∗, ∗)], [[Theory ∗]], [theory_{2}(∗, ∗)], [theory_{3}(∗, ∗)], [theory_{4}(∗, ∗, ∗)], [HeadNil′′], [HeadPair′′], [Transitivity′′], [Contra′′], [HeadNil], [HeadPair], [Transitivity], [Contra], [T_{E}], [ragged right], [ragged right expansion ], [parm(∗, ∗, ∗)], [parm^{∗}(∗, ∗, ∗)], [inst(∗, ∗)], [inst^{∗}(∗, ∗)], [occur(∗, ∗, ∗)], [occur^{∗}(∗, ∗, ∗)], [unify(∗ = ∗, ∗)], [unify^{∗}(∗ = ∗, ∗)], [unify_{2}(∗ = ∗, ∗)], [L_{a}], [L_{b}], [L_{c}], [L_{d}], [L_{e}], [L_{f}], [L_{g}], [L_{h}], [L_{i}], [L_{j}], [L_{k}], [L_{l}], [L_{m}], [L_{n}], [L_{o}], [L_{p}], [L_{q}], [L_{r}], [L_{s}], [L_{t}], [L_{u}], [L_{v}], [L_{w}], [L_{x}], [L_{y}], [L_{z}], [L_{A}], [L_{B}], [L_{C}], [L_{D}], [L_{E}], [L_{F}], [L_{G}], [L_{H}], [L_{I}], [L_{J}], [L_{K}], [L_{L}], [L_{M}], [L_{N}], [L_{O}], [L_{P}], [L_{Q}], [L_{R}], [L_{S}], [L_{T}], [L_{U}], [L_{V}], [L_{W}], [L_{X}], [L_{Y}], [L_{Z}], [L_{?}], [Reflexivity], [Reflexivity_{1}], [Commutativity], [Commutativity_{1}], [<tactic>], [tactic], [[∗ =^{tactic} ∗]], [P(∗, ∗, ∗)], [P^{∗}(∗, ∗, ∗)], [p_{0}], [conclude_{1}(∗, ∗)], [conclude_{2}(∗, ∗, ∗)], [conclude_{3}(∗, ∗, ∗, ∗)], [conclude_{4}(∗, ∗)], [˙0], [˙1], [˙2], [ȧ], [ḃ], [ċ], [ḋ], [ė], [ḟ], [ġ], [ḣ], [i̇], [j̇], [k̇], [l̇], [ṁ], [ṅ], [ȯ], [ṗ], [q̇], [ṙ], [ṡ], [ṫ], [u̇], [v̇], [ẇ], [ẋ], [ẏ], [ż], [ṅonfree(∗, ∗)], [ṅonfree^{∗}(∗, ∗)], [ḟree⟨∗|∗ := ∗⟩], [ḟree^{∗}⟨∗|∗ := ∗⟩], [∗≡⟨∗|∗ := ∗⟩], [∗≡⟨^{∗}∗|∗ := ∗⟩], [S′], [A1′], [A2′], [A3′], [A4′], [A5′], [S1′], [S2′], [S3′], [S4′], [S5′], [S6′], [S7′], [S8′], [S9′], [MP′], [Gen′], [L3.2(a)′], [nani teki nina...:54], [nani teki nina...:55], [nani teki nina...:56], [M3.2(b)], [M3.2(c)], [M3.2(d)(I)], [M3.2(d)(II)], [M3.2(f)], [M3.2(g)], [M3.2(h)(I)], [M3.2(h)(II)], [M3.2(h)], [nani teki nina...:66], [M3.2(d)_{h}], [M1.10(a)], [M1.10(b)], [M1.10(b_{−})], [M1.10(b_{+})], [MP′_{h}+], [Tilføjhypotese_{+}], [M1.7_{+}], [M1.7], [MP′_{h}], [Tilføjhypotese], [Gen′_{h}], [M3.2(a)], [M3.2(a)_{h}], [M3.2(b)_{h}], [M3.1(S1′)_{h}], [M3.2(c)_{h}], [M3.1(S2′)_{h}], [M3.1(S5′)_{h}], [M3.1(S6′)_{h}], [M3.2(f)]; Preassociative [∗ {∗}], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [˙∗]; Preassociative [“ ∗ ”], [], [(∗)^{t}], [string(∗) + ∗], [string(∗) ++ ∗], [ ∗], [ ∗], [!∗], [”∗], [#∗], [$∗], [%∗], [&∗], [’∗], [(∗], [)∗], [∗∗], [+∗], [, ∗], [-∗], [.∗], [/∗], [0∗], [1∗], [2∗], [3∗], [4∗], [5∗], [6∗], [7∗], [8∗], [9∗], [:∗], [; ∗], [<∗], [=∗], [>∗], [?∗], [@∗], [A∗], [B∗], [C∗], [D∗], [E∗], [F∗], [G∗], [H∗], [I∗], [J∗], [K∗], [L∗], [M∗], [N∗], [O∗], [P∗], [Q∗], [R∗], [S∗], [T∗], [U∗], [V∗], [W∗], [X∗], [Y∗], [Z∗], [[∗], [\∗], []∗], [ˆ ∗], [ ∗], [‘∗], [a∗], [b∗], [c∗], [d∗], [e∗], [f∗], [g∗], [h∗], [i∗], [j∗], [k∗], [l∗], [m∗], [n∗], [o∗], [p∗], [q∗], [r∗], [s∗], [t∗], [u∗], [v∗], [w∗], [x∗], [y∗], [z∗], [{∗], [|∗], [}∗], [˜ ∗], [Preassociative ∗; ∗], [Postassociative ∗; ∗], [[∗], ∗], [priority ∗ end], [newline ∗], [macro newline ∗]; Preassociative [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗^{H}], [∗^{T}], [∗^{U}], [∗^{h}], [∗^{t}], [∗^{s}], [∗^{c}], [∗^{d}], [∗^{a}], [∗^{C}], [∗^{M}], [∗^{B}], [∗^{r}], [∗^{i}], [∗^{d}], [∗^{R}], [∗^{0}], [∗^{1}], [∗^{2}], [∗^{3}], [∗^{4}], [∗^{5}], [∗^{6}], [∗^{7}], [∗^{8}], [∗^{9}], [∗^{E}], [∗^{V}], [∗^{C}], [∗^{C^{∗}}], [∗′]; Preassociative [∗ · ∗], [∗ ·_{0} ∗], [∗ ˙· ∗]; Preassociative [∗ + ∗], [∗ +_{0} ∗], [∗ +_{1} ∗], [∗ − ∗], [∗ −_{0} ∗], [∗ −_{1} ∗], [∗ ˙+ ∗]; Preassociative [∗ ∪ {∗}], [∗ ∪ ∗], [∗\{∗}]; Postassociative [∗ ˙. . ∗], [∗ \underline{˙. .} ∗], [∗ \underline{: :} ∗], [∗ \underline{+2∗} ∗], [∗ : : ∗], [∗ +2∗ ∗]; Postassociative [∗, ∗]; Preassociative

[∗ ≈^{B} ∗], [∗ ≈^{D} ∗], [∗ ≈^{C} ∗], [∗ ≈^{P} ∗], [∗ ≈ ∗], [∗ = ∗], [∗ →^{+} ∗], [∗ =^{t} ∗], [∗ =^{t^{∗}} ∗], [∗ =^{r} ∗],

[∗ ∈_{t} ∗], [∗ ⊆_{T} ∗], [∗ =^{T} ∗], [∗ =^{s} ∗], [∗ free in ∗], [∗ free in^{∗} ∗], [∗ free for ∗ in ∗],

[∗ free for^{∗} ∗ in ∗], [∗ ∈_{c} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗], [∗ =^{p} ∗], [∗^{P}];

Preassociative [¬∗], [ ˙¬ ∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗], [∗ ˙∧ ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗], [∗ ˙∨ ∗]; Preassociative [ ˙∀∗: ∗], [ ˙∃∗: ∗]; Postassociative [∗ ¨⇒ ∗], [∗ ˙⇒ ∗], [∗ ˙⇔ ∗]; Postassociative [∗ : ∗], [∗!∗]; Preassociative

[∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} ];

Preassociative [λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗^{I}], [∗^{⊳} ], [∗^{V}], [∗^{+}], [∗^{−}], [∗^{∗}]; Preassociative [∗ @ ∗], [∗ ⊳ ∗], [∗ ⊳ ⊳ ∗], [∗ ≫ ∗], [∗ ⊵ ∗], [∗ ⊵_{h} ∗]; Postassociative [∗ ⊢ ∗], [∗ ⊢⊢ ∗], [∗ i.e. ∗]; Preassociative [∀∗: ∗]; Postassociative [∗ ⊕ ∗]; Postassociative [∗; ∗]; Preassociative [∗ proves ∗]; Preassociative [∗ proof of ∗ : ∗], [Line ∗ : ∗ ≫ ∗; ∗], [Last line ∗ ≫ ∗ □], [Line ∗ : Premise ≫ ∗; ∗], [Line ∗ : Side-condition ≫ ∗; ∗], [Arbitrary ≫ ∗; ∗], [Local ≫ ∗ = ∗; ∗]; Postassociative [∗ then ∗], [∗[ ∗]∗]; Preassociative [∗&∗]; Preassociative [∗\\∗]; ]

B Index

C Bibliografi

[1] K. Grue. Logiweb. In Fairouz Kamareddine, editor, Mathematical Knowledge Management Symposium 2003, volume 93 of Electronic Notes in Theoretical Computer Science, pages 70–101. Elsevier, 2004.

[2] E. Mendelson. Introduction to Mathematical Logic. Wadsworth and Brooks, 3. edition, 1987.

D Pyk kildetekst