Udvidelse af S-reglerne

Maja Hanne Tønnesen, Rune Christoffer Kildetoft Andresen & Niels Peter Meyn Milthers

28. juni 2006

Indhold

1 Introduktion 2

2 Konklusion 2

3 S-reglerne 2

4 Udsagn 3.2 4 4.1 3.2j . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 4.2 3.2k . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 4.3 3.2l . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 4.4 3.2m . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 4.5 3.2n . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 4.6 3.2o . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

5 Udsagn 3.4 8 5.1 3.4a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 5.2 3.4b . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 5.3 3.4c . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 5.4 3.4d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

6 Udsagn 3.5 10

6.1 Definitioner i forbindelse med ∧ og ∨ . . . . . . . . . . . . . . . . 11 6.1.1 Introduktion af ∧ . . . . . . . . . . . . . . . . . . . . . . . 11 6.1.2 Elimination af ∧ 1 . . . . . . . . . . . . . . . . . . . . . . 11 6.1.3 Elimination af ∧ 2 . . . . . . . . . . . . . . . . . . . . . . 11 6.1.4 Introduktion af ∨ 1 . . . . . . . . . . . . . . . . . . . . . . 12 6.1.5 Introduktion af ∨ 2 . . . . . . . . . . . . . . . . . . . . . . 12 6.1.6 Elimination af ∨ . . . . . . . . . . . . . . . . . . . . . . . 12

6.2 Andre hjælpesætninger . . . . . . . . . . . . . . . . . . . . . . . . 12 6.2.1 A ≠ B . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 6.2.2 ∃ x . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

6.3 3.5a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 6.4 3.5b . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 6.5 3.5c . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 6.6 3.5d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 6.7 3.5e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 6.8 3.5f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 6.9 3.5g . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 6.10 3.5h . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

7 Udsagn 3.7 18 7.1 Definitioner af ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \overline{x} = \overline{y} . . . . . . . . . . 18

A Hjælpe lemmaer 18

1 Introduktion

Dette skriftlige projekt er lavet i forbindelse med Logik-kurset 2006^{1}. Vores mål i denne opgave var at bevise en delmængde af udsagnene^{2} vedrørende læresætningerne^{3} fra S-systemet, som er beskrevet i Mendelson [Men97] i kapitel 3.1. For lethedens skyld er alle nummereringer de samme som i Mendelson. Mere præcist går opgaven ud på at bevise 3.2(j-o), bevise 3.4, bevise 3.5, tilføje aksiomet x < y ⇔ ∃z : z ≠ 0 ∧ z + x = y, bevise 3.7, tilføje aksiomer, der definere ¬∀_{obj}z: ¬\overline{y} = \overline{x} · z, bevise 3.10 og bevise 3.11. I afsnittene 3 til 7 er beviserne for de påviste lemmaer gennemgået. Alle trivielle hjælpelemmaer er bevist i appendix A.

2 Konklusion

Vi har ikke løst opgaven til fulde, men har dog formået at påvise 3.2j - 3.2o, 3.4, 3.5a -g. På grund af problemer med definitionen af reglen svarende til “existensial rule” side 77 i mendelson, har vi som beskrevet i afsnit 6 ikke været i stand til at kunne bevise lemmaerne fra 3.5h og frem. Vi har dog som beskrevet i afsnit 6.10 og 6.2.2 gennemgået hvordan beviserne for 3.5h og “existensial rule” ville have set ud, hvis problemet ikke var opstået. Vi har endvidere kort gennemgået de definitioner, som ville være nødvendige for at kunne påvise Lemma 3.7

3 S-reglerne

S-systemet er en første ordens teori, som er udviklet ud fra Peanos postulater og ved hjælp mængdelære. Det skulle være passende at bruge til at bevise basis-resultaterne for tal-teori. Aksiomerne for S er følgende.

1Kursus 061004/202 Logik

2Eng.: proposition

3Eng.: theorem

[S →^{stmt} x] [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} ⊢ ∀_{obj}\underline{x}: \underline{a}][Gen →^{proof} Rule tactic] [Ded →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: λx.Ded_{0}(⌈\underline{a}⌉, ⌈\underline{b}⌉) ⊢⊢

\underline{a} ⊢ \underline{b}][Ded →^{proof} Rule tactic]

[S2 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ \underline{a}′ = \underline{b}′][S2 →^{proof}

Rule tactic]

[S3 →^{stmt} S ⊢ ∀\underline{a}: ¬0 = \underline{a}′][S3 →^{proof} Rule tactic] [S4 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ = \underline{b}′ ⊢ \underline{a} = \underline{b}][S4 →^{proof} Rule tactic]

[S5 →^{stmt} S ⊢ ∀\underline{a}: \underline{a} + 0 = \underline{a}][S5 →^{proof} Rule tactic] [S6 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′][S6 →^{proof} Rule tactic]

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

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

Endvidere er reglen S9, som er grundlæggende for matematisk induktion, også en del af S-teorien. Denne regel kan på almindeligt sprog udtrykkes som:

Hvis en egenskab holder for 0 og egenskaben holder for efterfølgeren x′ til et naturligt tal x, som egenskaben gælder for, så vil egenskaben gælde for alle naturlige tal.

I pyk er S9 defineret som:

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

\underline{a} ⇒ \underline{c} ⊢ \underline{a}][S9 →^{proof} Rule tactic]

Reglen for bevis ved modsætninger er den sidste grundlæggende regel, der skal bruges i beviserne. Reglen kan på almindeligt sprog udtrykkes som følgende:

Hvis man ud fra en antagelse A kan påvise at en egenskab B gælder, og at man (når antagelsen stadig gælder) kan vise at den modsatte egenskab ¬B også gælder, så må det modsatte af antagelsen gælde, dvs. ¬A.

I pyk er reglen defineret som:

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

4 Udsagn 3.2

Dette udsagn indeholder de grundlæggende regneregler for tal, som opfører sig som de naturlige tal. Hjælpesætningerne eller lemmaerne er generelt set en direkte konsekvens af aksiomerne. Alle lemmaerne i dette afsnit kan udledes ud fra de tidligere nævnte og som det er bevist i både check [Gru06] og Mendelson er der for ethvert udtryk \underline{a}, \underline{b}, \underline{c} følgende velformulerede sætninger^{4} i systemet S:

[Prop 3.2a →^{stmt} S ⊢ ∀\underline{a}: \underline{a} = \underline{a}]

[Prop 3.2b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ \underline{b} = \underline{a}]

[Prop 3.2c →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{b} = \underline{c} ⊢ \underline{a} = \underline{c}]

[Prop 3.2d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{c} ⊢ \underline{b} = \underline{c} ⊢ \underline{a} = \underline{b}]

[Prop 3.2e →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{a} + \underline{c} = \underline{b} + \underline{c}]

[Prop 3.2f →^{stmt} S ⊢ ∀\underline{a}: \underline{a} = 0 + \underline{a}]

[Prop 3.2g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ + \underline{b} = \underline{a} + \underline{b}′]

[Prop 3.2h →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = \underline{b} + \underline{a}]

Da 3.2i ikke er bevist i check, (men er i Mendelson), har vi valgt for øvelsens skyld at indskrive beviset:

[Prop 3.2i →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{c} + \underline{a} = \underline{c} + \underline{b}]

[Prop 3.2i →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ Prop 3.2e ⊳ \underline{a} = \underline{b} ≫ \underline{a} + \underline{c} = \underline{b} + \underline{c}; Prop 3.2h ≫ \underline{a} + \underline{c} = \underline{c} + \underline{a}; Prop 3.2h ≫ \underline{b} + \underline{c} = \underline{c} + \underline{b}; S1 ⊳ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⊳ \underline{a} + \underline{c} = \underline{c} + \underline{a} ≫ \underline{b} + \underline{c} = \underline{c} + \underline{a}; Prop 3.2b ⊳ \underline{b} + \underline{c} = \underline{c} + \underline{a} ≫ \underline{c} + \underline{a} = \underline{b} + \underline{c}; Prop 3.2c ⊳ \underline{c} + \underline{a} = \underline{b} + \underline{c} ⊳ \underline{b} + \underline{c} = \underline{c} + \underline{b} ≫ \underline{c} + \underline{a} = \underline{c} + \underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{c} + \underline{a} = \underline{c} + \underline{b} ≫ \underline{a} = \underline{b} ⊢ \underline{c} + \underline{a} = \underline{c} + \underline{b}⌉, p_{0}, c)]

De følgende lemmaer er opskrevet, men ikke bevist i Mendelson. Disse er blandt dem som vi ønsker at bevise.

[Prop 3.2j →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c}]

[Prop 3.2k →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{a} · \underline{c} = \underline{b} · \underline{c}]

[Prop 3.2l →^{stmt} S ⊢ ∀\underline{a}: 0 · \underline{a} = 0]

[Prop 3.2m →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b}] [Prop 3.2n →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = \underline{b} · \underline{a}]

4Eng.: Wellformed formulas

[Prop 3.2o →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{c} · \underline{a} = \underline{c} · \underline{b}]

Her efter følger beviserne.

4.1 3.2j

[Prop 3.2j_{1} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} + 0 = \underline{a} + \underline{b} + 0]

[Prop 3.2j_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: S5 ≫ \underline{a} + \underline{b} + 0 = \underline{a} + \underline{b}; S5 ≫ \underline{b} + 0 = \underline{b}; Prop 3.2i ⊳ \underline{b} + 0 = \underline{b} ≫ \underline{a} + \underline{b} + 0 = \underline{a} + \underline{b}; Prop 3.2d ⊳ \underline{a} + \underline{b} + 0 = \underline{a} + \underline{b} ⊳ \underline{a} + \underline{b} + 0 = \underline{a} + \underline{b} ≫ \underline{a} + \underline{b} + 0 = \underline{a} + \underline{b} + 0⌉, p_{0}, c)]

[Prop 3.2j_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ⇒ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′]

[Prop 3.2j_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ⊢ S6 ≫ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′; S2 ⊳ \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ≫ \underline{a} + \underline{b} + \underline{c}′ = \underline{a}+\underline{b}+\underline{c}′; Prop 3.2c⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′ ⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′ ≫ \underline{a}+\underline{b}+\underline{c}′ = \underline{a} + \underline{b} + \underline{c}′; S6 ≫ \underline{b} + \underline{c}′ = \underline{b} + \underline{c}′; Prop 3.2i ⊳ \underline{b} + \underline{c}′ = \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{b} + \underline{c}′ = \underline{a}+\underline{b}+\underline{c}′; S6 ≫ \underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′; Prop 3.2c⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′ ≫ \underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′; Prop 3.2d⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′ ⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a} + \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ⊢ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ⇒ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′⌉, p_{0}, c)]

[Prop 3.2j →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c}]

[Prop 3.2j →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: Prop 3.2j_{1} ≫ \overline{x} + \overline{y} + 0 = \overline{x} + \overline{y} + 0; Prop 3.2j_{2} ≫ \overline{x} + \overline{y} + \overline{z} = \overline{x} + \overline{y} + \overline{z} ⇒ \overline{x} + \overline{y} + \overline{z}′ = \overline{x}+\overline{y}+\overline{z}′; S9 @ \overline{z}⊳\overline{x}+\overline{y}+0 = \overline{x}+\overline{y}+0⊳\overline{x}+\overline{y}+\overline{z} = \overline{x}+\overline{y}+\overline{z} ⇒ \overline{x}+\overline{y}+\overline{z}′ = \overline{x}+\overline{y}+\overline{z}′ ≫ \overline{x} + \overline{y} + \overline{z} = \overline{x} + \overline{y} + \overline{z}; Ded ⊳ \overline{x} + \overline{y} + \overline{z} = \overline{x} + \overline{y} + \overline{z} ≫ \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c}⌉, p_{0}, c)]

4.2 3.2k

[Prop 3.2k_{1} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⇒ \underline{a} · 0 = \underline{b} · 0]

[Prop 3.2k_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ S7 ≫ \underline{a} · 0 = 0; S7 ≫ \underline{b} · 0 = 0; Prop 3.2a ≫ 0 = 0; Prop 3.2b ⊳ \underline{b} · 0 = 0 ≫ 0 = \underline{b} · 0; Prop 3.2c ⊳ \underline{a} · 0 = 0 ⊳ 0 = \underline{b} · 0 ≫ \underline{a} · 0 = \underline{b} · 0; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ \underline{a} · 0 = \underline{b} · 0 ≫ \underline{a} = \underline{b} ⇒ \underline{a} · 0 = \underline{b} · 0⌉, p_{0}, c)]

[Prop 3.2k_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⇒ \underline{a} · \underline{c} = \underline{b} · \underline{c} ⇒ \underline{a} = \underline{b} ⇒ \underline{a} · \underline{c}′ = \underline{b} · \underline{c}′]

[Prop 3.2k_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⇒ \underline{a} · \underline{c} = \underline{b} · \underline{c} ⊢ \underline{a} = \underline{b} ⊢ MP⊳\underline{a} = \underline{b} ⇒ \underline{a}·\underline{c} = \underline{b}·\underline{c}⊳\underline{a} = \underline{b} ≫ \underline{a}·\underline{c} = \underline{b}·\underline{c}; S8 ≫ \underline{a}·\underline{c}′ = \underline{a}·\underline{c}+\underline{a}; S8 ≫ \underline{b} · \underline{c}′ = \underline{b} · \underline{c} + \underline{b}; Prop 3.2e ⊳ \underline{a} · \underline{c} = \underline{b} · \underline{c} ≫ \underline{a} · \underline{c} + \underline{a} = \underline{b} · \underline{c} + \underline{a}; Prop 3.2i ⊳ \underline{a} = \underline{b} ≫ \underline{b} · \underline{c} + \underline{a} = \underline{b} · \underline{c} + \underline{b}; Prop 3.2c ⊳ \underline{a} · \underline{c} + \underline{a} = \underline{b} · \underline{c} + \underline{a} ⊳ \underline{b} · \underline{c} + \underline{a} = \underline{b} · \underline{c} + \underline{b} ≫ \underline{a} · \underline{c} + \underline{a} = \underline{b}·\underline{c}+\underline{b}; Prop 3.2c⊳\underline{a}·\underline{c}′ = \underline{a}·\underline{c}+\underline{a}⊳\underline{a}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{b} ≫ \underline{a}·\underline{c}′ = \underline{b}·\underline{c}+\underline{b}; Prop 3.2d⊳ \underline{a}·\underline{c}′ = \underline{b}·\underline{c}+\underline{b}⊳\underline{b}·\underline{c}′ = \underline{b}·\underline{c}+\underline{b} ≫ \underline{a}·\underline{c}′ = \underline{b}·\underline{c}′; Ded⊳∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⇒ \underline{a}·\underline{c} = \underline{b}·\underline{c} ⊢ \underline{a} = \underline{b} ⊢ \underline{a}·\underline{c}′ = \underline{b}·\underline{c}′ ≫ \underline{a} = \underline{b} ⇒ \underline{a}·\underline{c} = \underline{b}·\underline{c} ⇒ \underline{a} = \underline{b} ⇒ \underline{a}·\underline{c}′ = \underline{b}·\underline{c}′⌉, p_{0}, c)]

[Prop 3.2k →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{a} · \underline{c} = \underline{b} · \underline{c}]

[Prop 3.2k →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ Prop 3.2k_{1} ≫ \overline{x} = \overline{y} ⇒ \overline{x} · 0 = \overline{y} · 0; Prop 3.2k_{2} ≫ \overline{x} = \overline{y} ⇒ \overline{x} · \overline{z} = \overline{y} · \overline{z} ⇒ \overline{x} = \overline{y} ⇒ \overline{x} · \overline{z}′ = \overline{y} · \overline{z}′; S9 @ \overline{z} ⊳ \overline{x} = \overline{y} ⇒ \overline{x} · 0 = \overline{y} · 0 ⊳ \overline{x} = \overline{y} ⇒ \overline{x} · \overline{z} = \overline{y} · \overline{z} ⇒ \overline{x} = \overline{y} ⇒ \overline{x} · \overline{z}′ = \overline{y} · \overline{z}′ ≫ \overline{x} = \overline{y} ⇒ \overline{x} · \overline{z} = \overline{y} · \overline{z}; Ded ⊳ \overline{x} = \overline{y} ⇒ \overline{x} · \overline{z} = \overline{y} · \overline{z} ≫ \underline{a} = \underline{b} ⇒ \underline{a} · \underline{c} = \underline{b} · \underline{c}; MP ⊳ \underline{a} = \underline{b} ⇒ \underline{a} · \underline{c} = \underline{b} · \underline{c} ⊳ \underline{a} = \underline{b} ≫ \underline{a} · \underline{c} = \underline{b} · \underline{c}⌉, p_{0}, c)]

4.3 3.2l

[Prop 3.2l_{2} →^{stmt} S ⊢ ∀\underline{a}: 0 · \underline{a} = 0 ⇒ 0 · \underline{a}′ = 0]

[Prop 3.2l_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{a}: 0 · \underline{a} = 0 ⊢ S8 ≫ 0 · \underline{a}′ = 0 · \underline{a} + 0; S5 ≫ 0 · \underline{a} + 0 = 0 · \underline{a}; Prop 3.2c ⊳ 0 · \underline{a}′ = 0 · \underline{a} + 0 ⊳ 0 · \underline{a} + 0 = 0 · \underline{a} ≫ 0 · \underline{a}′ = 0 · \underline{a}; Prop 3.2c ⊳ 0 · \underline{a}′ = 0 · \underline{a} ⊳ 0 · \underline{a} = 0 ≫ 0 · \underline{a}′ = 0; Ded ⊳ ∀\underline{a}: 0 · \underline{a} = 0 ⊢ 0 · \underline{a}′ = 0 ≫ 0 · \underline{a} = 0 ⇒ 0 · \underline{a}′ = 0⌉, p_{0}, c)]

[Prop 3.2l →^{stmt} S ⊢ ∀\underline{a}: 0 · \underline{a} = 0]

[Prop 3.2l →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: S7 ≫ 0 · 0 = 0; Prop 3.2l_{2} ≫ 0 · \overline{x} = 0 ⇒ 0 · \overline{x}′ = 0; S9 @ \overline{x} ⊳ 0 · 0 = 0 ⊳ 0 · \overline{x} = 0 ⇒ 0 · \overline{x}′ = 0 ≫ 0 · \overline{x} = 0; Ded ⊳ 0 · \overline{x} = 0 ≫ 0 · \underline{a} = 0⌉, p_{0}, c)]

4.4 3.2m

[Prop 3.2m_{1} →^{stmt} S ⊢ ∀\underline{a}: \underline{a}′ · 0 = \underline{a} · 0 + 0]

[Prop 3.2m_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: S7 ≫ \underline{a}′ · 0 = 0; Prop 3.2f ≫ 0 = 0 + 0; S7 ≫ \underline{a} · 0 = 0; Prop 3.2b ⊳ \underline{a} · 0 = 0 ≫ 0 = \underline{a} · 0; Prop 3.2e ⊳ 0 = \underline{a} · 0 ≫ 0 + 0 = \underline{a} · 0 + 0; Prop 3.2c ⊳ 0 = 0 + 0 ⊳ 0 + 0 = \underline{a} · 0 + 0 ≫ 0 = \underline{a} · 0 + 0; Prop 3.2c ⊳ \underline{a}′ · 0 = 0 ⊳ 0 = \underline{a} · 0 + 0 ≫ \underline{a}′ · 0 = \underline{a} · 0 + 0⌉, p_{0}, c)]

[Prop 3.2m_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ⇒ \underline{a}′ · \underline{b}′ = \underline{a} · \underline{b}′ + \underline{b}′]

[Prop 3.2m_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ⊢ S8 ≫ \underline{a}′ · \underline{b}′ = \underline{a}′ · \underline{b} + \underline{a}′; Prop 3.2e ⊳ \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ≫ \underline{a}′ · \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{b} + \underline{a}′; S6 ≫ \underline{b} + \underline{a}′ = \underline{b} + \underline{a}′; Prop 3.2g ≫ \underline{b}′ + \underline{a} = \underline{b} + \underline{a}′; Prop 3.2d ⊳ \underline{b} + \underline{a}′ = \underline{b} + \underline{a}′ ⊳ \underline{b}′ + \underline{a} = \underline{b} + \underline{a}′ ≫ \underline{b} + \underline{a}′ = \underline{b}′ + \underline{a}; Prop 3.2h ≫ \underline{b}′ + \underline{a} = \underline{a} + \underline{b}′; Prop 3.2c ⊳ \underline{b} + \underline{a}′ = \underline{b}′ + \underline{a} ⊳ \underline{b}′ + \underline{a} = \underline{a} + \underline{b}′ ≫ \underline{b} + \underline{a}′ = \underline{a} + \underline{b}′; Prop 3.2i ⊳ \underline{b} + \underline{a}′ = \underline{a} + \underline{b}′ ≫ \underline{a} · \underline{b} + \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{a} + \underline{b}′; Prop 3.2j ≫ \underline{a} · \underline{b} + \underline{a} + \underline{b}′ = \underline{a} · \underline{b} + \underline{a} + \underline{b}′; Prop 3.2d ⊳ \underline{a} · \underline{b} + \underline{b} + \underline{a}′ = \underline{a}·\underline{b}+\underline{a}+\underline{b}′ ⊳\underline{a}·\underline{b}+\underline{a}+\underline{b}′ = \underline{a}·\underline{b}+\underline{a}+\underline{b}′ ≫ \underline{a}·\underline{b}+\underline{b}+\underline{a}′ = \underline{a}·\underline{b}+\underline{a}+\underline{b}′; S8 ≫ \underline{a}·\underline{b}′ = \underline{a}·\underline{b}+\underline{a}; Prop 3.2e⊳\underline{a}·\underline{b}′ = \underline{a}·\underline{b}+\underline{a} ≫ \underline{a}·\underline{b}′+\underline{b}′ = \underline{a}·\underline{b}+\underline{a}+\underline{b}′; Prop 3.2d⊳\underline{a}·\underline{b}+\underline{b}+\underline{a}′ = \underline{a} · \underline{b} + \underline{a} + \underline{b}′ ⊳ \underline{a} · \underline{b}′ + \underline{b}′ = \underline{a} · \underline{b} + \underline{a} + \underline{b}′ ≫ \underline{a} · \underline{b} + \underline{b} + \underline{a}′ = \underline{a} · \underline{b}′ + \underline{b}′; Prop 3.2j ≫ \underline{a} · \underline{b} + \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{b} + \underline{a}′; Prop 3.2c ⊳ \underline{a}′ · \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{b} + \underline{a}′ ⊳ \underline{a} · \underline{b} + \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{b} + \underline{a}′ ≫ \underline{a}′ · \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{b} + \underline{a}′; Prop 3.2c ⊳ \underline{a}′ · \underline{b} + \underline{a}′ = \underline{a}·\underline{b}+\underline{b}+\underline{a}′ ⊳\underline{a}·\underline{b}+\underline{b}+\underline{a}′ = \underline{a}·\underline{b}′ +\underline{b}′ ≫ \underline{a}′ ·\underline{b}+\underline{a}′ = \underline{a}·\underline{b}′ +\underline{b}′; Prop 3.2c⊳\underline{a}′ ·\underline{b}′ = \underline{a}′ · \underline{b} + \underline{a}′ ⊳ \underline{a}′ · \underline{b} + \underline{a}′ = \underline{a} · \underline{b}′ + \underline{b}′ ≫ \underline{a}′ · \underline{b}′ = \underline{a} · \underline{b}′ + \underline{b}′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ⊢ \underline{a}′ · \underline{b}′ = \underline{a} · \underline{b}′ + \underline{b}′ ≫ \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ⇒ \underline{a}′ · \underline{b}′ = \underline{a} · \underline{b}′ + \underline{b}′⌉, p_{0}, c)]

[Prop 3.2m →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b}]

[Prop 3.2m →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: Prop 3.2m_{1} ≫ \overline{x}′ · 0 = \overline{x} · 0 + 0; Prop 3.2m_{2} ≫ \overline{x}′ · \overline{y} = \overline{x} · \overline{y} + \overline{y} ⇒ \overline{x}′ · \overline{y}′ = \overline{x} · \overline{y}′ + \overline{y}′; S9 @ \overline{y} ⊳ \overline{x}′ · 0 = \overline{x} · 0 + 0 ⊳ \overline{x}′ · \overline{y} = \overline{x} · \overline{y} + \overline{y} ⇒ \overline{x}′ · \overline{y}′ = \overline{x} · \overline{y}′ + \overline{y}′ ≫ \overline{x}′ · \overline{y} = \overline{x} · \overline{y} + \overline{y}; Ded ⊳ \overline{x}′ · \overline{y} = \overline{x} · \overline{y} + \overline{y} ≫ \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b}⌉, p_{0}, c)]

4.5 3.2n

[Prop 3.2n_{1} →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0 = 0 · \underline{a}]

[Prop 3.2n_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: S7 ≫ \underline{a} · 0 = 0; Prop 3.2l ≫ 0 · \underline{a} = 0; Prop 3.2d ⊳ \underline{a} · 0 = 0 ⊳ 0 · \underline{a} = 0 ≫ \underline{a} · 0 = 0 · \underline{a}⌉, p_{0}, c)]

[Prop 3.2n_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = \underline{b} · \underline{a} ⇒ \underline{a} · \underline{b}′ = \underline{b}′ · \underline{a}]

[Prop 3.2n_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = \underline{b} · \underline{a} ⊢ S8 ≫ \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a}; Prop 3.2e ⊳ \underline{a} · \underline{b} = \underline{b} · \underline{a} ≫ \underline{a} · \underline{b} + \underline{a} = \underline{b} · \underline{a} + \underline{a}; Prop 3.2m ≫ \underline{b}′ · \underline{a} = \underline{b}·\underline{a}+\underline{a}; Prop 3.2b⊳\underline{b}′·\underline{a} = \underline{b}·\underline{a}+\underline{a} ≫ \underline{b}·\underline{a}+\underline{a} = \underline{b}′·\underline{a}; Prop 3.2c⊳\underline{a}·\underline{b}+\underline{a} = \underline{b}·\underline{a}+\underline{a}⊳ \underline{b}·\underline{a}+\underline{a} = \underline{b}′·\underline{a} ≫ \underline{a}·\underline{b}+\underline{a} = \underline{b}′·\underline{a}; Prop 3.2c⊳\underline{a}·\underline{b}′ = \underline{a}·\underline{b}+\underline{a}⊳\underline{a}·\underline{b}+\underline{a} = \underline{b}′·\underline{a} ≫ \underline{a}·\underline{b}′ = \underline{b}′ ·\underline{a}; Ded⊳∀\underline{a}: ∀\underline{b}: \underline{a}·\underline{b} = \underline{b}·\underline{a} ⊢ \underline{a}·\underline{b}′ = \underline{b}′ ·\underline{a} ≫ \underline{a}·\underline{b} = \underline{b}·\underline{a} ⇒ \underline{a}·\underline{b}′ = \underline{b}′ ·\underline{a}⌉, p_{0}, c)]

[Prop 3.2n →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = \underline{b} · \underline{a}]

[Prop 3.2n →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: Prop 3.2n_{1} ≫ \overline{x} · 0 = 0 · \overline{x}; Prop 3.2n_{2} ≫ \overline{x} · \overline{y} = \overline{y} · \overline{x} ⇒ \overline{x} · \overline{y}′ = \overline{y}′ · \overline{x}; S9 @ \overline{y} ⊳ \overline{x} · 0 = 0 · \overline{x} ⊳ \overline{x} · \overline{y} = \overline{y} · \overline{x} ⇒ \overline{x} · \overline{y}′ = \overline{y}′ · \overline{x} ≫ \overline{x} · \overline{y} = \overline{y} · \overline{x}; Ded ⊳ \overline{x} · \overline{y} = \overline{y} · \overline{x} ≫ \underline{a} · \underline{b} = \underline{b} · \underline{a}⌉, p_{0}, c)]

4.6 3.2o

[Prop 3.2o →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{c} · \underline{a} = \underline{c} · \underline{b}]

[Prop 3.2o →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ Prop 3.2k ⊳ \underline{a} = \underline{b} ≫ \underline{a} · \underline{c} = \underline{b} · \underline{c}; Prop 3.2n ≫ \underline{a} · \underline{c} = \underline{c} · \underline{a}; Prop 3.2n ≫ \underline{b} · \underline{c} = \underline{c} · \underline{b}; Prop 3.2c ⊳ \underline{a} · \underline{c} = \underline{b} · \underline{c} ⊳ \underline{b} · \underline{c} = \underline{c} · \underline{b} ≫ \underline{a} · \underline{c} = \underline{c} · \underline{b}; S1 ⊳ \underline{a} · \underline{c} = \underline{c} · \underline{a} ⊳ \underline{a} · \underline{c} = \underline{c} · \underline{b} ≫ \underline{c} · \underline{a} = \underline{c} · \underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{c} · \underline{a} = \underline{c} · \underline{b} ≫ \underline{a} = \underline{b} ⇒ \underline{c} · \underline{a} = \underline{c} · \underline{b}; MP ⊳ \underline{a} = \underline{b} ⇒ \underline{c} · \underline{a} = \underline{c} · \underline{b} ⊳ \underline{a} = \underline{b} ≫ \underline{c} · \underline{a} = \underline{c} · \underline{b}⌉, p_{0}, c)]

5 Udsagn 3.4

De følgende udsagn er en udvidelse af egenskaberne ved addition og multiplikation.

[Prop 3.4a →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} + \underline{c} = \underline{a} · \underline{b} + \underline{a} · \underline{c}]

[Prop 3.4b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{b} + \underline{c} · \underline{a} = \underline{b} · \underline{a} + \underline{c} · \underline{a}]

[Prop 3.4c →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c}]

[Prop 3.4d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} = \underline{b}]

5.1 3.4a

[Prop 3.4a_{1} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} + 0 = \underline{a} · \underline{b} + \underline{a} · 0]

[Prop 3.4a_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: S5 ≫ \underline{b} + 0 = \underline{b}; Prop 3.2o ⊳ \underline{b} + 0 = \underline{b} ≫ \underline{a}·\underline{b}+0 = \underline{a}·\underline{b}; S5 ≫ \underline{a}·\underline{b}+0 = \underline{a}·\underline{b}; Prop 3.2d⊳\underline{a}·\underline{b}+0 = \underline{a}·\underline{b}⊳\underline{a}·\underline{b}+0 = \underline{a}·\underline{b} ≫ \underline{a} · \underline{b} + 0 = \underline{a} · \underline{b} + 0; S7 ≫ \underline{a} · 0 = 0; Prop 3.2i ⊳ \underline{a} · 0 = 0 ≫ \underline{a} · \underline{b} + \underline{a} · 0 = \underline{a} · \underline{b} + 0; Prop 3.2d⊳\underline{a}·\underline{b}+0 = \underline{a}·\underline{b}+0⊳\underline{a}·\underline{b}+\underline{a}·0 = \underline{a}·\underline{b}+0 ≫ \underline{a}·\underline{b}+0 = \underline{a}·\underline{b}+\underline{a}·0⌉, p_{0}, c)]

[Prop 3.4a_{2} →^{stmt} S ⊢ ∀\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} · \underline{b} + \underline{a} · \underline{c}′]

[Prop 3.4a_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} + \underline{c} = \underline{a} · \underline{b} + \underline{a} · \underline{c} ⊢ S6 ≫ \underline{b}+\underline{c}′ = \underline{b}+\underline{c}′; Prop 3.2o⊳\underline{b}+\underline{c}′ = \underline{b}+\underline{c}′ ≫ \underline{a}·\underline{b}+\underline{c}′ = \underline{a}·\underline{b}+\underline{c}′; S8 ≫ \underline{a}·\underline{b}+\underline{c}′ = \underline{a}·\underline{b}+\underline{c}+\underline{a}; Prop 3.2e⊳\underline{a}·\underline{b}+\underline{c} = \underline{a}·\underline{b}+\underline{a}·\underline{c} ≫ \underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}; Prop 3.2j ≫ \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}; Prop 3.2c⊳\underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}⊳\underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a} ≫ \underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}; S8 ≫ \underline{a}·\underline{c}′ = \underline{a}·\underline{c}+\underline{a}; Prop 3.2i⊳\underline{a}·\underline{c}′ = \underline{a}·\underline{c}+\underline{a} ≫ \underline{a}·\underline{b}+\underline{a}·\underline{c}′ = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}; Prop 3.2d⊳\underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}⊳\underline{a}·\underline{b}+\underline{a}·\underline{c}′ = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a} ≫ \underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}′; Prop 3.2c⊳\underline{a}·\underline{b}+\underline{c}′ = \underline{a}·\underline{b}+\underline{c}+\underline{a}⊳\underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a} · \underline{b} + \underline{a} · \underline{c}′ ≫ \underline{a} · \underline{b} + \underline{c}′ = \underline{a} · \underline{b} + \underline{a} · \underline{c}′; Prop 3.2c ⊳ \underline{a} · \underline{b} + \underline{c}′ = \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} · \underline{b} + \underline{a} · \underline{c}′; Ded ⊳ ∀\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} · \underline{b} + \underline{a} · \underline{c}′ ≫ \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}′⌉, p_{0}, c)]

[Prop 3.4a →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} + \underline{c} = \underline{a} · \underline{b} + \underline{a} · \underline{c}]

[Prop 3.4a →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: Prop 3.4a_{1} ≫ \overline{x} · \overline{y} + 0 = \overline{x} · \overline{y} + \overline{x} · 0; Prop 3.4a_{2} ≫ \overline{x} · \overline{y} + \overline{z} = \overline{x} · \overline{y} + \overline{x} · \overline{z} ⇒ \overline{x} · \overline{y} + \overline{z}′ = \overline{x}·\overline{y}+\overline{x}·\overline{z}′; S9 @ \overline{z}⊳\overline{x}·\overline{y}+0 = \overline{x}·\overline{y}+\overline{x}·0⊳\overline{x}·\overline{y}+\overline{z} = \overline{x}·\overline{y}+\overline{x}·\overline{z} ⇒ \overline{x}·\overline{y}+\overline{z}′ = \overline{x}·\overline{y}+\overline{x}·\overline{z}′ ≫ \overline{x} · \overline{y} + \overline{z} = \overline{x} · \overline{y} + \overline{x} · \overline{z}; Ded ⊳ \overline{x} · \overline{y} + \overline{z} = \overline{x} · \overline{y} + \overline{x} · \overline{z} ≫ \underline{a} · \underline{b} + \underline{c} = \underline{a} · \underline{b} + \underline{a} · \underline{c}⌉, p_{0}, c)]

5.2 3.4b

[Prop 3.4b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{b} + \underline{c} · \underline{a} = \underline{b} · \underline{a} + \underline{c} · \underline{a}] [Prop 3.4b →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: Prop 3.4a ≫ \underline{a} · \underline{b} + \underline{c} = \underline{a} · \underline{b} + \underline{a} · \underline{c}; Prop 3.2n ≫ \underline{a} · \underline{b} + \underline{c} = \underline{b} + \underline{c} · \underline{a}; Prop 3.2n ≫ \underline{a} · \underline{b} = \underline{b} · \underline{a}; Prop 3.2n ≫ \underline{a} · \underline{c} = \underline{c} · \underline{a}; S1 ⊳ \underline{a} · \underline{b} + \underline{c} = \underline{b} + \underline{c} · \underline{a} ⊳ \underline{a} · \underline{b} + \underline{c} = \underline{a} · \underline{b} + \underline{a} · \underline{c} ≫ \underline{b} + \underline{c} · \underline{a} = \underline{a} · \underline{b} + \underline{a} · \underline{c}; Prop 3.2e ⊳ \underline{a} · \underline{b} = \underline{b} · \underline{a} ≫ \underline{a} · \underline{b} + \underline{a} · \underline{c} = \underline{b} · \underline{a} + \underline{a} · \underline{c}; Prop 3.2i ⊳ \underline{a} · \underline{c} = \underline{c} · \underline{a} ≫ \underline{b} · \underline{a} + \underline{a} · \underline{c} = \underline{b} · \underline{a} + \underline{c} · \underline{a}; Prop 3.2c ⊳ \underline{a} · \underline{b} + \underline{a} · \underline{c} = \underline{b} · \underline{a} + \underline{a} · \underline{c} ⊳ \underline{b} · \underline{a} + \underline{a} · \underline{c} = \underline{b} · \underline{a} + \underline{c} · \underline{a} ≫ \underline{a} · \underline{b} + \underline{a} · \underline{c} = \underline{b} · \underline{a} + \underline{c} · \underline{a}; Prop 3.2c ⊳ \underline{b} + \underline{c} · \underline{a} = \underline{a} · \underline{b} + \underline{a} · \underline{c} ⊳ \underline{a} · \underline{b} + \underline{a} · \underline{c} = \underline{b} · \underline{a} + \underline{c} · \underline{a} ≫ \underline{b} + \underline{c} · \underline{a} = \underline{b} · \underline{a} + \underline{c} · \underline{a}⌉, p_{0}, c)]

5.3 3.4c

[Prop 3.4c_{1} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} · 0 = \underline{a} · \underline{b} · 0]

[Prop 3.4c_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: S7 ≫ \underline{a} · \underline{b} · 0 = 0; S7 ≫ \underline{b} · 0 = 0; Prop 3.2o⊳\underline{b}·0 = 0 ≫ \underline{a}·\underline{b}·0 = \underline{a}·0; S7 ≫ \underline{a}·0 = 0; Prop 3.2c⊳\underline{a}·\underline{b}·0 = \underline{a}·0⊳\underline{a}·0 = 0 ≫ \underline{a} · \underline{b} · 0 = 0; Prop 3.2d ⊳ \underline{a} · \underline{b} · 0 = 0 ⊳ \underline{a} · \underline{b} · 0 = 0 ≫ \underline{a} · \underline{b} · 0 = \underline{a} · \underline{b} · 0⌉, p_{0}, c)]

[Prop 3.4c_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c} ⇒ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c}′]

[Prop 3.4c_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c} ⊢ S8 ≫ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b}; Prop 3.2e ⊳ \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c} ≫ \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b}; Prop 3.2c ⊳ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} ⊳ \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} ≫ \underline{a}·\underline{b}·\underline{c}′ = \underline{a}·\underline{b}·\underline{c}+\underline{a}·\underline{b}; Prop 3.4a ≫ \underline{a}·\underline{b}·\underline{c}+\underline{b} = \underline{a}·\underline{b}·\underline{c}+\underline{a}·\underline{b}; Prop 3.2d⊳\underline{a}·\underline{b}·\underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} ⊳ \underline{a} · \underline{b} · \underline{c} + \underline{b} = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} ≫ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{b}; S8 ≫ \underline{b} · \underline{c}′ = \underline{b} · \underline{c} + \underline{b}; Prop 3.2o ⊳ \underline{b} · \underline{c}′ = \underline{b} · \underline{c} + \underline{b} ≫ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{b}; Prop 3.2d ⊳ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{b} ⊳ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{b} ≫ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c}′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c} ⊢ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c}′ ≫ \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c} ⇒ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c}′⌉, p_{0}, c)]

[Prop 3.4c →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c}]

[Prop 3.4c →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: Prop 3.4c_{1} ≫ \overline{x} · \overline{y} · 0 = \overline{x}·\overline{y}·0; Prop 3.4c_{2} ≫ \overline{x}·\overline{y}·\overline{z} = \overline{x}·\overline{y}·\overline{z} ⇒ \overline{x}·\overline{y}·\overline{z}′ = \overline{x}·\overline{y}·\overline{z}′; S9 @ \overline{z}⊳\overline{x}·\overline{y}·0 = \overline{x}·\overline{y}·0⊳\overline{x}·\overline{y}·\overline{z} = \overline{x}·\overline{y}·\overline{z} ⇒ \overline{x}·\overline{y}·\overline{z}′ = \overline{x}·\overline{y}·\overline{z}′ ≫ \overline{x}·\overline{y}·\overline{z} = \overline{x}·\overline{y}·\overline{z}; Ded⊳\overline{x}·\overline{y}·\overline{z} = \overline{x}·\overline{y}·\overline{z} ≫ \underline{a}·\underline{b}·\underline{c} = \underline{a}·\underline{b}·\underline{c}⌉, p_{0}, c)]

5.4 3.4d

[Prop 3.4d_{1} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + 0 = \underline{b} + 0 ⇒ \underline{a} = \underline{b}]

[Prop 3.4d_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} + 0 = \underline{b} + 0 ⊢ S5 ≫ \underline{a} + 0 = \underline{a}; S5 ≫ \underline{b} + 0 = \underline{b}; S1 ⊳ \underline{a} + 0 = \underline{a} ⊳ \underline{a} + 0 = \underline{b} + 0 ≫ \underline{a} = \underline{b} + 0; Prop 3.2c ⊳ \underline{a} = \underline{b} + 0 ⊳ \underline{b} + 0 = \underline{b} ≫ \underline{a} = \underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} + 0 = \underline{b} + 0 ⊢ \underline{a} = \underline{b} ≫ \underline{a} + 0 = \underline{b} + 0 ⇒ \underline{a} = \underline{b}⌉, p_{0}, c)]

[Prop 3.4d_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a}+\underline{c} = \underline{b}+\underline{c} ⇒ \underline{a} = \underline{b} ⇒ \underline{a}+\underline{c}′ = \underline{b}+\underline{c}′ ⇒ \underline{a} = \underline{b}]

[Prop 3.4d_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} = \underline{b} ⊢ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′ ⊢ S6 ≫ \underline{a} + \underline{c}′ = \underline{a} + \underline{c}′; S6 ≫ \underline{b} + \underline{c}′ = \underline{b} + \underline{c}′; S1 ⊳ \underline{a} + \underline{c}′ = \underline{a} + \underline{c}′ ⊳ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′; Prop 3.2c ⊳ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′ ⊳ \underline{b} + \underline{c}′ = \underline{b}+\underline{c}′ ≫ \underline{a}+\underline{c}′ = \underline{b}+\underline{c}′; S4⊳\underline{a}+\underline{c}′ = \underline{b}+\underline{c}′ ≫ \underline{a}+\underline{c} = \underline{b}+\underline{c}; MP⊳\underline{a}+\underline{c} = \underline{b}+\underline{c} ⇒ \underline{a} = \underline{b}⊳\underline{a}+\underline{c} = \underline{b}+\underline{c} ≫ \underline{a} = \underline{b}; Ded⊳∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a}+\underline{c} = \underline{b}+\underline{c} ⇒ \underline{a} = \underline{b} ⊢ \underline{a}+\underline{c}′ = \underline{b} + \underline{c}′ ⊢ \underline{a} = \underline{b} ≫ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} = \underline{b} ⇒ \underline{a} + \underline{c}′ = \underline{b} + \underline{c}′ ⇒ \underline{a} = \underline{b}⌉, p_{0}, c)]

[Prop 3.4d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} = \underline{b}]

[Prop 3.4d →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: Prop 3.4d_{1} ≫ \overline{x} + 0 = \overline{y} + 0 ⇒ \overline{x} = \overline{y}; Prop 3.4d_{2} ≫ \overline{x}+\overline{z} = \overline{y} +\overline{z} ⇒ \overline{x} = \overline{y} ⇒ \overline{x}+\overline{z}′ = \overline{y} +\overline{z}′ ⇒ \overline{x} = \overline{y}; S9 @ \overline{z}⊳\overline{x}+0 = \overline{y} + 0 ⇒ \overline{x} = \overline{y} ⊳ \overline{x} + \overline{z} = \overline{y} + \overline{z} ⇒ \overline{x} = \overline{y} ⇒ \overline{x} + \overline{z}′ = \overline{y} + \overline{z}′ ⇒ \overline{x} = \overline{y} ≫ \overline{x} + \overline{z} = \overline{y} + \overline{z} ⇒ \overline{x} = \overline{y}; Ded ⊳ \overline{x} + \overline{z} = \overline{y} + \overline{z} ⇒ \overline{x} = \overline{y} ≫ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} = \underline{b}⌉, p_{0}, c)]

6 Udsagn 3.5

I denne del har vi kun kunne løse indtil h, da denne og de efterfølgende kræver reglen “existensial rule”. Dog er der i afsnit 6.2.2 genemgået hvilket problem der forhindrer os i at bevise ” existencial rule”, og hvordan vi ville have bevist reglen, hvis problemet ikke var opstået. Endvidere er der i 6.2.2 genemgået hvordan vi ville have løst 3.5h. I de følgende udsagn indgår numeraler opfører sig som de naturlige tal og er defineret i forhold til 0 på følgende måde:

\begin{aligned}0 & = & \overline{0} \\ 0′ & = & \overline{1} \\ 0′′ & = & \overline{2} \\ ⋮ & & ⋮ \\ 0^{n∗′} & = & \overline{n} \end{aligned}

Dvs. hvis \overline{0} er et numeral, og hvis \overline{n} er et numeral, så er \overline{n}′ også.

[Prop 3.5a →^{stmt} S ⊢ ∀\underline{a}: \underline{a} + 0′ = \underline{a}′]

[Prop 3.5b →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0′ = \underline{a}]

[Prop 3.5c →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0′′ = \underline{a} + \underline{a}]

[Prop 3.5d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0]

[Prop 3.5e →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ \underline{a} · \underline{b} = 0 ⇒ \underline{a} = 0]

[Prop 3.5f →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0]

[Prop 3.5g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′] [Prop 3.5h →^{stmt} S ⊢ ∀\underline{a}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}\underline{b}: ¬\underline{a} = \underline{b}′]

[Prop 3.5i →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{c} = 0 ⇒ \underline{a} · \underline{c} = \underline{b} · \underline{c} ⇒ \underline{a} = \underline{b}]

[Prop 3.5j →^{stmt} S ⊢ ∀\underline{a}: ¬\underline{a} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬∀_{obj}\underline{b}: ¬\underline{a} = \underline{b}′′]

Efterfø[]lgende vil vi gennemgåde nø[]dvendige hjælpesætninger og definitioner for at kunne bevise 3.5a-3.5g.

6.1 Definitioner i forbindelse med ∧ og ∨

Fra 3.5d bruges ∧ og ∨, som begge er makrodefinerede udtryk.

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

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

Endvidere er det klart at reglerne for introduktion og eliminering af ∧ og ∨ dermed også skal bruges. Alle disse er bevist i de følgende afsnit.

6.1.1 Introduktion af ∧

[Con →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ \underline{b} ⊢ ¬\underline{a} ⇒ ¬\underline{b}]

[Con →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ \underline{b} ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ ¬\underline{b} ⊢ Repetition ⊳ \underline{a} ≫ \underline{a}; MP ⊳ \underline{a} ⇒ ¬\underline{b} ⊳ \underline{a} ≫ ¬\underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ ¬\underline{b} ⊢ ¬\underline{b} ≫ \underline{a} ⇒ ¬\underline{b} ⇒ ¬\underline{b}; Lem1.11b ≫ \underline{b} ⇒ ¬¬\underline{b}; MP ⊳ \underline{b} ⇒ ¬¬\underline{b} ⊳ \underline{b} ≫ ¬¬\underline{b}; MT ⊳ \underline{a} ⇒ ¬\underline{b} ⇒ ¬\underline{b} ⊳ ¬¬\underline{b} ≫ ¬\underline{a} ⇒ ¬\underline{b}⌉, p_{0}, c)]

6.1.2 Elimination af ∧ 1

[Con1 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⇒ ¬\underline{b} ⊢ \underline{a}]

[Con1 →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⇒ ¬\underline{b} ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⊢ A1′ ≫ ¬\underline{a} ⇒ ¬¬\underline{b} ⇒ ¬\underline{a}; MP ⊳ ¬\underline{a} ⇒ ¬¬\underline{b} ⇒ ¬\underline{a} ⊳ ¬\underline{a} ≫ ¬¬\underline{b} ⇒ ¬\underline{a}; Lem1.11d ≫ ¬¬\underline{b} ⇒ ¬\underline{a} ⇒ \underline{a} ⇒ ¬\underline{b}; MP ⊳ ¬¬\underline{b} ⇒ ¬\underline{a} ⇒ \underline{a} ⇒ ¬\underline{b} ⊳ ¬¬\underline{b} ⇒ ¬\underline{a} ≫ \underline{a} ⇒ ¬\underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⊢ \underline{a} ⇒ ¬\underline{b} ≫ ¬\underline{a} ⇒ \underline{a} ⇒ ¬\underline{b}; MT ⊳ ¬\underline{a} ⇒ \underline{a} ⇒ ¬\underline{b} ⊳ ¬\underline{a} ⇒ ¬\underline{b} ≫ ¬¬\underline{a}; Lem1.11a ≫ ¬¬\underline{a} ⇒ \underline{a}; MP ⊳ ¬¬\underline{a} ⇒ \underline{a} ⊳ ¬¬\underline{a} ≫ \underline{a}⌉, p_{0}, c)]

6.1.3 Elimination af ∧ 2

[Con2 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⇒ ¬\underline{b} ⊢ \underline{b}]

[Con2 →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⇒ ¬\underline{b} ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⊢ A1′ ≫ ¬\underline{b} ⇒ \underline{a} ⇒ ¬\underline{b}; MP ⊳ ¬\underline{b} ⇒ \underline{a} ⇒ ¬\underline{b} ⊳ ¬\underline{b} ≫ \underline{a} ⇒ ¬\underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⊢ \underline{a} ⇒ ¬\underline{b} ≫ ¬\underline{b} ⇒ \underline{a} ⇒ ¬\underline{b}; MT ⊳ ¬\underline{b} ⇒ \underline{a} ⇒ ¬\underline{b} ⊳ ¬\underline{a} ⇒ ¬\underline{b} ≫ ¬¬\underline{b}; Lem1.11a ≫ ¬¬\underline{b} ⇒ \underline{b}; MP ⊳ ¬¬\underline{b} ⇒ \underline{b} ⊳ ¬¬\underline{b} ≫ \underline{b}⌉, p_{0}, c)] 6.1.4 Introduktion af ∨ 1

[Dis1 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ ¬\underline{a} ⇒ \underline{b}]

[Dis1 →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ Lem1.11c ≫ ¬¬\underline{a} ⇒ ¬\underline{a} ⇒ \underline{b}; Lem1.11b ≫ \underline{a} ⇒ ¬¬\underline{a}; MP ⊳ \underline{a} ⇒ ¬¬\underline{a} ⊳ \underline{a} ≫ ¬¬\underline{a}; MP ⊳ ¬¬\underline{a} ⇒ ¬\underline{a} ⇒ \underline{b} ⊳ ¬¬\underline{a} ≫ ¬\underline{a} ⇒ \underline{b}⌉, p_{0}, c)]

6.1.5 Introduktion af ∨ 2

[Dis2 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{b} ⊢ ¬\underline{a} ⇒ \underline{b}]

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

6.1.6 Elimination af ∨

Da vi ikke har haft brug for at fjerne ∨, har vi ikke bevist denne regel.

6.2 Andre hjælpesætninger

Vi har til beviset af 3.5a-3.5g haft brug for nogle af reglerne fra [Gru06], dog med imply istedet for infer. Sådanne regler er navngivet med det <oprindelige navn>’ og beviserne for disse kan ses i Appendix A.

6.2.1 A ≠ B

En ny hjælperegel er regel H3 , som skal bruges i forbindelse med A ≠ B for at kunne konkludere sammenhænge i mellem (x = y) ∧ (x ≠ 3) ⇒ (y ≠ 3).

[H3 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⊢ ¬\underline{c} ⊢ ¬\underline{b}]

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

6.2.2 ∃ x

Selv om vi ikke har nået at implementere fra opgave 3.5h, hvor der gøres brug af ∃, har vi alligevel makrodefineret kvantoren som følger. [∃x: y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[∃x: y ¨= ¬(∀x: ¬y)]⌉)] Vores problem har været, at vi ikke har kunne udtrykke “B(x, t), hvor t kan indsættes i stedet for x’erne uden at blive bundet til en alkvantor”, i pyk. Beviset for hjælpesætningen, der indfører eksistenskvantoren, ville dog have været opbygget nogenlunde som følger. Følgende tautologi,

(A ⇒ ¬B) ⇒ (B ⇒ ¬A)

antages vist nogenlunde som Modus Tollens, dog med variation. Ved axiom A4′ kan vi få instansen:

(∀x)¬A(x, t) ⇒ ¬A(t, t)

Idet man kan få følgende instans af tautologien:

((∀x)¬A(x, t) ⇒ ¬A(t, t)) ⇒ (A(t, t) ⇒ ¬(∀x)¬A(x, t))

kan man vha. MP på instansen og axiomet få:

(A(t, t) ⇒ ¬(∀x)¬A(x, t))

og pga. af makrodefinitionen er denne nu vist. Herefter vises Lemmaerne 3.5a-3.5g

6.3 3.5a

[Prop 3.5a →^{stmt} S ⊢ ∀\underline{a}: \underline{a} + 0′ = \underline{a}′]

[Prop 3.5a →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: S6 ≫ \underline{a} + 0′ = \underline{a} + 0′; S5 ≫ \underline{a} + 0 = \underline{a}; S2⊳\underline{a}+0 = \underline{a} ≫ \underline{a}+0′ = \underline{a}′; Prop 3.2c⊳\underline{a}+0′ = \underline{a}+0′ ⊳\underline{a}+0′ = \underline{a}′ ≫ \underline{a}+0′ = \underline{a}′; Prop 3.2a ≫ \underline{a}+0′ = \underline{a}+0′; S1⊳\underline{a}+0′ = \underline{a}+0′⊳\underline{a}+0′ = \underline{a}′ ≫ \underline{a}+0′ = \underline{a}′⌉, p_{0}, c)]

6.4 3.5b

[Prop 3.5b →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0′ = \underline{a}]

[Prop 3.5b →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: S8 ≫ \underline{a} · 0′ = \underline{a} · 0 + \underline{a}; S7 ≫ \underline{a} · 0 = 0; Prop 3.2e ⊳ \underline{a} · 0 = 0 ≫ \underline{a} · 0 + \underline{a} = 0 + \underline{a}; Prop 3.2c ⊳ \underline{a} · 0′ = \underline{a} · 0 + \underline{a} ⊳ \underline{a} · 0 + \underline{a} = 0 + \underline{a} ≫ \underline{a} · 0′ = 0 + \underline{a}; Prop 3.2f ≫ \underline{a} = 0 + \underline{a}; Prop 3.2b ⊳ \underline{a} = 0 + \underline{a} ≫ 0 + \underline{a} = \underline{a}; Prop 3.2c ⊳ \underline{a} · 0′ = 0 + \underline{a} ⊳ 0 + \underline{a} = \underline{a} ≫ \underline{a} · 0′ = \underline{a}; Prop 3.2a ≫ \underline{a} · 0′ = \underline{a} · 0′; S1 ⊳ \underline{a} · 0′ = \underline{a} · 0′ ⊳ \underline{a} · 0′ = \underline{a} ≫ \underline{a} · 0′ = \underline{a}⌉, p_{0}, c)]

6.5 3.5c

[Prop 3.5c →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0′′ = \underline{a} + \underline{a}]

[Prop 3.5c →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: S8 ≫ \underline{a} · 0′′ = \underline{a} · 0′ + \underline{a}; Prop 3.5b ≫ \underline{a} · 0′ = \underline{a}; Prop 3.2e ⊳ \underline{a} · 0′ = \underline{a} ≫ \underline{a} · 0′ + \underline{a} = \underline{a} + \underline{a}; Prop 3.2c ⊳ \underline{a} · 0′′ = \underline{a} · 0′ + \underline{a} ⊳ \underline{a} · 0′ + \underline{a} = \underline{a} + \underline{a} ≫ \underline{a} · 0′′ = \underline{a} + \underline{a}; Prop 3.2a ≫ \underline{a} · 0′′ = \underline{a} · 0′′; S1 ⊳ \underline{a} · 0′′ = \underline{a} · 0′′ ⊳ \underline{a} · 0′′ = \underline{a} + \underline{a} ≫ \underline{a} · 0′′ = \underline{a} + \underline{a}⌉, p_{0}, c)]

6.6 3.5d

[Prop 3.5d_{1} →^{stmt} S ⊢ ∀\underline{a}: \underline{a} + 0 = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬0 = 0] [Prop 3.5d_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{a}: \underline{a} + 0 = 0 ⊢ S5 ≫ \underline{a} + 0 = \underline{a}; S1 ⊳ \underline{a} + 0 = \underline{a} ⊳ \underline{a} + 0 = 0 ≫ \underline{a} = 0; Prop 3.2a ≫ 0 = 0; Con ⊳ \underline{a} = 0 ⊳ 0 = 0 ≫ ¬\underline{a} = 0 ⇒ ¬0 = 0; Ded ⊳ ∀\underline{a}: \underline{a} + 0 = 0 ⊢ ¬\underline{a} = 0 ⇒ ¬0 = 0 ≫ \underline{a} + 0 = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬0 = 0⌉, p_{0}, c)]

[Prop 3.5d_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ⇒ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0]

[Prop 3.5d_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b}′ = 0 ⊢ S3 ≫ ¬0 = \underline{a} + \underline{b}′; Prop3.2b′ ≫ \underline{a} + \underline{b}′ = 0 ⇒ 0 = \underline{a} + \underline{b}′; Lem1.11e ≫ \underline{a} + \underline{b}′ = 0 ⇒ 0 = \underline{a} + \underline{b}′ ⇒ ¬0 = \underline{a} + \underline{b}′ ⇒ ¬\underline{a} + \underline{b}′ = 0; MP ⊳ \underline{a} + \underline{b}′ = 0 ⇒ 0 = \underline{a} + \underline{b}′ ⇒ ¬0 = \underline{a} + \underline{b}′ ⇒ ¬\underline{a} + \underline{b}′ = 0 ⊳ \underline{a} + \underline{b}′ = 0 ⇒ 0 = \underline{a} + \underline{b}′ ≫ ¬0 = \underline{a} + \underline{b}′ ⇒ ¬\underline{a} + \underline{b}′ = 0; MP ⊳ ¬0 = \underline{a} + \underline{b}′ ⇒ ¬\underline{a} + \underline{b}′ = 0 ⊳ ¬0 = \underline{a} + \underline{b}′ ≫ ¬\underline{a} + \underline{b}′ = 0; S6 ≫ \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′; S1′′ ≫ \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′ ⇒ \underline{a} + \underline{b}′ = 0 ⇒ \underline{a} + \underline{b}′ = 0; H3 ⊳ \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′ ⇒ \underline{a} + \underline{b}′ = 0 ⇒ \underline{a} + \underline{b}′ = 0 ⊳ \underline{a} + \underline{b}′ = \underline{a} + \underline{b}′ ⊳ ¬\underline{a} + \underline{b}′ = 0 ≫ ¬\underline{a} + \underline{b}′ = 0; Lem1.11c ≫ ¬\underline{a} + \underline{b}′ = 0 ⇒ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0; MP ⊳ ¬\underline{a} + \underline{b}′ = 0 ⇒ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0 ⊳ ¬\underline{a} + \underline{b}′ = 0 ≫ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0; MP ⊳ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0 ⊳ \underline{a} + \underline{b}′ = 0 ≫ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b}′ = 0 ⊢ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0 ≫ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ⊢ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0 ≫ \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ⇒ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0⌉, p_{0}, c)]

[Prop 3.5d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0]

[Prop 3.5d →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: Prop 3.5d_{1} ≫ \overline{x} + 0 = 0 ⇒ ¬\overline{x} = 0 ⇒ ¬0 = 0; Prop 3.5d_{2} ≫ \overline{x} + \overline{y} = 0 ⇒ ¬\overline{x} = 0 ⇒ ¬\overline{y} = 0 ⇒ \overline{x} + \overline{y}′ = 0 ⇒ ¬\overline{x} = 0 ⇒ ¬\overline{y}′ = 0; S9 @ \overline{y} ⊳ \overline{x} + 0 = 0 ⇒ ¬\overline{x} = 0 ⇒ ¬0 = 0 ⊳ \overline{x} + \overline{y} = 0 ⇒ ¬\overline{x} = 0 ⇒ ¬\overline{y} = 0 ⇒ \overline{x} + \overline{y}′ = 0 ⇒ ¬\overline{x} = 0 ⇒ ¬\overline{y}′ = 0 ≫ \overline{x} + \overline{y} = 0 ⇒ ¬\overline{x} = 0 ⇒ ¬\overline{y} = 0; Ded⊳\overline{x}+\overline{y} = 0 ⇒ ¬\overline{x} = 0 ⇒ ¬\overline{y} = 0 ≫ \underline{a}+\underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0⌉, p_{0}, c)]

6.7 3.5e

[Prop 3.5e_{1} →^{stmt} S ⊢ ∀\underline{a}: ¬0 = 0 ⇒ \underline{a} · 0 = 0 ⇒ \underline{a} = 0]

[Prop 3.5e_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{a}: ¬0 = 0 ⊢ Prop 3.2a ≫ 0 = 0; Lem1.11c ≫ ¬0 = 0 ⇒ 0 = 0 ⇒ \underline{a} · 0 = 0 ⇒ \underline{a} = 0; MP ⊳ ¬0 = 0 ⇒ 0 = 0 ⇒ \underline{a} · 0 = 0 ⇒ \underline{a} = 0 ⊳ ¬0 = 0 ≫ 0 = 0 ⇒ \underline{a} · 0 = 0 ⇒ \underline{a} = 0; MP ⊳ 0 = 0 ⇒ \underline{a} · 0 = 0 ⇒ \underline{a} = 0 ⊳ 0 = 0 ≫ \underline{a} · 0 = 0 ⇒ \underline{a} = 0; Ded ⊳ ∀\underline{a}: ¬0 = 0 ⊢ \underline{a} · 0 = 0 ⇒ \underline{a} = 0 ≫ ¬0 = 0 ⇒ \underline{a} · 0 = 0 ⇒ \underline{a} = 0⌉, p_{0}, c)]

[Prop 3.5e_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ \underline{a} · \underline{b} = 0 ⇒ \underline{a} = 0 ⇒ ¬\underline{b}′ = 0 ⇒ \underline{a} · \underline{b}′ = 0 ⇒ \underline{a} = 0]

[Prop 3.5e_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ \underline{a} · \underline{b} = 0 ⇒ \underline{a} = 0 ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b}′ = 0 ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b}′ = 0 ⊢ S8 ≫ \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a}; S1 ⊳ \underline{a} · \underline{b}′ = \underline{a}·\underline{b}+\underline{a}⊳\underline{a}·\underline{b}′ = 0 ≫ \underline{a}·\underline{b}+\underline{a} = 0; Prop 3.5d ≫ \underline{a}·\underline{b}+\underline{a} = 0 ⇒ ¬\underline{a}·\underline{b} = 0 ⇒ ¬\underline{a} = 0; MP ⊳ \underline{a} · \underline{b} + \underline{a} = 0 ⇒ ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⊳ \underline{a} · \underline{b} + \underline{a} = 0 ≫ ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0; Con2⊳¬\underline{a}·\underline{b} = 0 ⇒ ¬\underline{a} = 0 ≫ \underline{a} = 0; Ded⊳∀\underline{a}: ∀\underline{b}: \underline{a}·\underline{b}′ = 0 ⊢ \underline{a} = 0 ≫ \underline{a}·\underline{b}′ = 0 ⇒ \underline{a} = 0; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬\underline{b}′ = 0 ⊢ \underline{a} · \underline{b}′ = 0 ⇒ \underline{a} = 0 ≫ ¬\underline{b}′ = 0 ⇒ \underline{a} · \underline{b}′ = 0 ⇒ \underline{a} = 0; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ \underline{a} · \underline{b} = 0 ⇒ \underline{a} = 0 ⊢ ¬\underline{b}′ = 0 ⇒ \underline{a} · \underline{b}′ = 0 ⇒ \underline{a} = 0 ≫ ¬\underline{b} = 0 ⇒ \underline{a} · \underline{b} = 0 ⇒ \underline{a} = 0 ⇒ ¬\underline{b}′ = 0 ⇒ \underline{a} · \underline{b}′ = 0 ⇒ \underline{a} = 0⌉, p_{0}, c)]

[Prop 3.5e →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ \underline{a} · \underline{b} = 0 ⇒ \underline{a} = 0]

[Prop 3.5e →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: Prop 3.5e_{1} ≫ ¬0 = 0 ⇒ \overline{x} · 0 = 0 ⇒ \overline{x} = 0; Prop 3.5e_{2} ≫ ¬\overline{y} = 0 ⇒ \overline{x} · \overline{y} = 0 ⇒ \overline{x} = 0 ⇒ ¬\overline{y}′ = 0 ⇒ \overline{x} · \overline{y}′ = 0 ⇒ \overline{x} = 0; S9 @ \overline{y} ⊳ ¬0 = 0 ⇒ \overline{x} · 0 = 0 ⇒ \overline{x} = 0 ⊳ ¬\overline{y} = 0 ⇒ \overline{x} · \overline{y} = 0 ⇒ \overline{x} = 0 ⇒ ¬\overline{y}′ = 0 ⇒ \overline{x} · \overline{y}′ = 0 ⇒ \overline{x} = 0 ≫ ¬\overline{y} = 0 ⇒ \overline{x} · \overline{y} = 0 ⇒ \overline{x} = 0; Ded ⊳ ¬\overline{y} = 0 ⇒ \overline{x} · \overline{y} = 0 ⇒ \overline{x} = 0 ≫ ¬\underline{b} = 0 ⇒ \underline{a} · \underline{b} = 0 ⇒ \underline{a} = 0⌉, p_{0}, c)]

6.8 3.5f

[Prop 3.5f_{1} →^{stmt} S ⊢ ∀\underline{a}: \underline{a} + 0 = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0]

[Prop 3.5f_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{a}: \underline{a} + 0 = 0′ ⊢ S5 ≫ \underline{a} + 0 = \underline{a}; S1 ⊳ \underline{a} + 0 = \underline{a} ⊳ \underline{a} + 0 = 0′ ≫ \underline{a} = 0′; Prop 3.2a ≫ 0 = 0; Con ⊳ \underline{a} = 0′ ⊳ 0 = 0 ≫ ¬\underline{a} = 0′ ⇒ ¬0 = 0; Dis2 ⊳ ¬\underline{a} = 0′ ⇒ ¬0 = 0 ≫ ¬¬\underline{a} = 0 ⇒ ¬0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0; Ded ⊳ ∀\underline{a}: \underline{a} + 0 = 0′ ⊢ ¬¬\underline{a} = 0 ⇒ ¬0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0 ≫ \underline{a} + 0 = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0⌉, p_{0}, c)]

[Prop 3.5f_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0 ⇒ \underline{a} + \underline{b}′ = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0]

[Prop 3.5f_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0 ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}+\underline{b}′ = 0′ ⊢ S6 ≫ \underline{a}+\underline{b}′ = \underline{a}+\underline{b}′; S1⊳\underline{a}+\underline{b}′ = \underline{a}+\underline{b}′⊳\underline{a}+\underline{b}′ = 0′ ≫ \underline{a}+\underline{b}′ = 0′; S4⊳\underline{a}+\underline{b}′ = 0′ ≫ \underline{a}+\underline{b} = 0; Prop 3.5d ≫ \underline{a}+\underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0; MP ⊳ \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ⊳ \underline{a} + \underline{b} = 0 ≫ ¬\underline{a} = 0 ⇒ ¬\underline{b} = 0; Con1⊳¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ≫ \underline{a} = 0; Con2⊳¬\underline{a} = 0 ⇒ ¬\underline{b} = 0 ≫ \underline{b} = 0; S2⊳\underline{b} = 0 ≫ \underline{b}′ = 0′; Con⊳\underline{a} = 0⊳\underline{b}′ = 0′ ≫ ¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′; Dis1⊳¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ≫ ¬¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b}′ = 0′ ⊢ ¬¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0 ≫ \underline{a} + \underline{b}′ = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0 ⊢ \underline{a} + \underline{b}′ = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0 ≫ \underline{a} + \underline{b} = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0 ⇒ \underline{a} + \underline{b}′ = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0⌉, p_{0}, c)]

[Prop 3.5f →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0]

[Prop 3.5f →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: Prop 3.5f_{1} ≫ \overline{x} + 0 = 0′ ⇒ ¬¬\overline{x} = 0 ⇒ ¬0 = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬0 = 0; Prop 3.5f_{2} ≫ \overline{x} + \overline{y} = 0′ ⇒ ¬¬\overline{x} = 0 ⇒ ¬\overline{y} = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬\overline{y} = 0 ⇒ \overline{x} + \overline{y}′ = 0′ ⇒ ¬¬\overline{x} = 0 ⇒ ¬\overline{y}′ = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬\overline{y}′ = 0; S9 @ \overline{y} ⊳ \overline{x} + 0 = 0′ ⇒ ¬¬\overline{x} = 0 ⇒ ¬0 = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬0 = 0 ⊳ \overline{x} + \overline{y} = 0′ ⇒ ¬¬\overline{x} = 0 ⇒ ¬\overline{y} = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬\overline{y} = 0 ⇒ \overline{x} + \overline{y}′ = 0′ ⇒ ¬¬\overline{x} = 0 ⇒ ¬\overline{y}′ = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬\overline{y}′ = 0 ≫ \overline{x} + \overline{y} = 0′ ⇒ ¬¬\overline{x} = 0 ⇒ ¬\overline{y} = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬\overline{y} = 0; Ded ⊳ \overline{x} + \overline{y} = 0′ ⇒ ¬¬\overline{x} = 0 ⇒ ¬\overline{y} = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬\overline{y} = 0 ≫ \underline{a} + \underline{b} = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ ¬\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0⌉, p_{0}, c)]

6.9 3.5g

[Prop 3.5g_{1} →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0′]

[Prop 3.5g_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{a}: \underline{a} · 0 = 0′ ⊢ S7 ≫ \underline{a} · 0 = 0; S1 ⊳ \underline{a} · 0 = 0 ⊳ \underline{a} · 0 = 0′ ≫ 0 = 0′; S3 ≫ ¬0 = 0′; Lem1.11c ≫ ¬0 = 0′ ⇒ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0′; MP ⊳ ¬0 = 0′ ⇒ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0′ ⊳ ¬0 = 0′ ≫ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0′; MP ⊳ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0′ ⊳ 0 = 0′ ≫ ¬\underline{a} = 0′ ⇒ ¬0 = 0′; Ded ⊳ ∀\underline{a}: \underline{a} · 0 = 0′ ⊢ ¬\underline{a} = 0′ ⇒ ¬0 = 0′ ≫ \underline{a} · 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬0 = 0′⌉, p_{0}, c)]

[Prop 3.5g_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′]

[Prop 3.5g_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⊢ Con2 ⊳ ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ≫ \underline{a} = 0′; Con1 ⊳ ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ≫ \underline{a} · \underline{b} = 0; S3 ≫ ¬0 = 0′; H10 ⊳ ¬0 = 0′ ≫ ¬0′ = 0; S1′′ ≫ \underline{a} = 0′ ⇒ \underline{a} = 0 ⇒ 0′ = 0; H3 ⊳ \underline{a} = 0′ ⇒ \underline{a} = 0 ⇒ 0′ = 0 ⊳ \underline{a} = 0′ ⊳ ¬0′ = 0 ≫ ¬\underline{a} = 0; Prop 3.2n ≫ \underline{a} · \underline{b} = \underline{b} · \underline{a}; S1 ⊳ \underline{a} · \underline{b} = \underline{b} · \underline{a} ⊳ \underline{a} · \underline{b} = 0 ≫ \underline{b} · \underline{a} = 0; Prop 3.5e ≫ ¬\underline{a} = 0 ⇒ \underline{b} · \underline{a} = 0 ⇒ \underline{b} = 0; MP ⊳ ¬\underline{a} = 0 ⇒ \underline{b} · \underline{a} = 0 ⇒ \underline{b} = 0 ⊳ ¬\underline{a} = 0 ≫ \underline{b} · \underline{a} = 0 ⇒ \underline{b} = 0; MP ⊳ \underline{b} · \underline{a} = 0 ⇒ \underline{b} = 0 ⊳ \underline{b} · \underline{a} = 0 ≫ \underline{b} = 0; S2 ⊳ \underline{b} = 0 ≫ \underline{b}′ = 0′; Con ⊳ \underline{a} = 0′ ⊳ \underline{b}′ = 0′ ≫ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⊢ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ≫ ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′⌉, p_{0}, c)]

[Prop 3.5g_{3} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⊢ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′]

[Prop 3.5g_{3} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⊢ Con1 ⊳ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ≫ \underline{a} · \underline{b} = 0′; MP ⊳ \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⊳ \underline{a} · \underline{b} = 0′ ≫ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′; Con1 ⊳ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ≫ \underline{a} = 0′; Con2 ⊳ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ≫ \underline{a} = 0; S1 ⊳ \underline{a} = 0 ⊳ \underline{a} = 0′ ≫ 0 = 0′; S3 ≫ ¬0 = 0′; Lem1.11c ≫ ¬0 = 0′ ⇒ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; MP ⊳ ¬0 = 0′ ⇒ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ⊳ ¬0 = 0′ ≫ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; MP ⊳ 0 = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ⊳ 0 = 0′ ≫ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⊢ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ≫ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′⌉, p_{0}, c)]

[Prop 3.5g_{4} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⇒ \underline{a} · \underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′] [Prop 3.5g_{4} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⊢ \underline{a} · \underline{b}′ = 0′ ⊢ S8 ≫ \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a}; S1 ⊳ \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a} ⊳ \underline{a} · \underline{b}′ = 0′ ≫ \underline{a} · \underline{b} + \underline{a} = 0′; Prop 3.5f ≫ \underline{a} · \underline{b} + \underline{a} = 0′ ⇒ ¬¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0; MP ⊳ \underline{a} · \underline{b} + \underline{a} = 0′ ⇒ ¬¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0⊳\underline{a}·\underline{b}+\underline{a} = 0′ ≫ ¬¬\underline{a}·\underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a}·\underline{b} = 0′ ⇒ ¬\underline{a} = 0; Prop 3.5g_{2} ≫ ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; Prop 3.5g_{3} ⊳ \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ≫ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; H11 ⊳ ¬¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⊳ ¬\underline{a} · \underline{b} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ⊳ ¬\underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ≫ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⊢ \underline{a} · \underline{b}′ = 0′ ⊢ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′ ≫ \underline{a}·\underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′ ⇒ \underline{a}·\underline{b}′ = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b}′ = 0′⌉, p_{0}, c)]

[Prop 3.5g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′]

[Prop 3.5g →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: Prop 3.5g_{1} ≫ \overline{x}·0 = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬0 = 0′; Prop 3.5g_{4} ≫ \overline{x}·\overline{y} = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬\overline{y} = 0′ ⇒ \overline{x}·\overline{y}′ = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬\overline{y}′ = 0′; S9 @ \overline{y} ⊳ \overline{x} · 0 = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬0 = 0′ ⊳ \overline{x} · \overline{y} = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬\overline{y} = 0′ ⇒ \overline{x} · \overline{y}′ = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬\overline{y}′ = 0′ ≫ \overline{x} · \overline{y} = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬\overline{y} = 0′; Ded ⊳ \overline{x} · \overline{y} = 0′ ⇒ ¬\overline{x} = 0′ ⇒ ¬\overline{y} = 0′ ≫ \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ ¬\underline{b} = 0′⌉, p_{0}, c)]

6.10 3.5h

[Prop 3.5h →^{stmt} S ⊢ ∀\underline{a}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}\underline{b}: ¬\underline{a} = \underline{b}′] Beviset for 3.5.h ville i pyk have set ud nogenlunde som følgende:

t ≠ 0 ⇒ (∃y)(t = y′)

Part I

\begin{matrix}L01 & prem & 0 ≠ 0 \\ L02 & abbr.L01 & ¬(0 = 0) \\ L03 & 3.2.a & 0 = 0 \\ L04 & Lemma1.11.c & ¬(0 = 0) ⇒ ((0 = 0) ⇒ (∃w)(0 = w′)) \\ L05 & MP, L02, L03 & (∃w)(0 = w′) \\ L06 & Ded, L05 & (0 ≠ 0) ⇒ (∃w)(0 = w′) \end{matrix}

Part II

\begin{matrix}L01 : & premise & (x ≠ 0) ⇒ (∃w)(x = w′) \\ L02 : & S3′ & x′ ≠ 0 \\ L03 : & T aut. : A ∨ ¬A & (x = 0) ∨ ¬(x = 0) \\ L04 : & prem. & (x = 0) \\ L05 : & S2′ & 0′ = x′ \\ L06 : & E4 & (x = 0) ⇒ (∃w)(x′ = w′) \\ L07 : & prem & ¬(x = 0) \\ L08 : & MP, L01, L07 & (∃w)(x = w′) \\ L09 : & rulec & x = b′ \\ L10 : & S2′ & (∃w)(x′ = w′) \\ L11 : & E4 & ¬(x = 0) ⇒ (∃w)(x′ = w′) \\ L12 & Lemma H11, L06.L11 & (x′ ≠ 0) ⇒ (∃w)(x′ = w′) \end{matrix}

Tilbage er blot at bruge sætning S9 for at fuldende induktionsbeviset.

7 Udsagn 3.7

Vi har kun lavet de indledende definitioner, da hele 3.7 kræver ”existential rule”.

7.1 Definitioner af ¬∀_{obj}z: ¬¬¬z = 0 ⇒ ¬z + \overline{x} = \overline{y}

Vi har makrodefineret følgende definitioner: [x < y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x < y ¨= ∃z: (z ≠ 0 ∧ z + x = y)]⌉)] [x ≤ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ≤ y ¨= x < y ∨ x = y]⌉)] [x > y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x > y ¨= y < x]⌉)] [x ≥ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ≥ y ¨= y ≤ x]⌉)] [x ≮ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ≮ y ¨= ¬(x < y)]⌉)] [x ≯ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ≯ y ¨= y ≮ x]⌉)] [x | y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x | y ¨= ∃z: y = x · z]⌉)] Ved hjælp af disse definitioner og ”existential rule” ville 3.7 kunne bevises.

A Hjælpe lemmaer

Til flere af vores beviser har vi brug for nogle hjælpe-lemmaer, disse er bevist i det følgende afsnit

[Lem1.11c →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⇒ \underline{a} ⇒ \underline{b}]

[Cor1.10a →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⊢ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⇒ \underline{c}]

[Cor1.10b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{b} ⊢ \underline{a} ⇒ \underline{c}]

[Lem1.11a →^{stmt} S ⊢ ∀\underline{a}: ¬¬\underline{a} ⇒ \underline{a}] [Lem1.11b →^{stmt} S ⊢ ∀\underline{a}: \underline{a} ⇒ ¬¬\underline{a}]

[Prop3.2c′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⇒ \underline{b} = \underline{c} ⇒ \underline{a} = \underline{c}]

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

[Neg′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⇒ ¬\underline{b} ⇒ \underline{a} ⇒ \underline{b}]

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

[Lem1.11e →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a}]

[Lem1.11d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⇒ \underline{a} ⇒ \underline{b}]

[Prop3.2b′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⇒ \underline{b} = \underline{a}]

[H10 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = \underline{a} ⊢ ¬\underline{a} = \underline{b}]

[H11 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} ⇒ \underline{b} ⊢ \underline{a} ⇒ \underline{c} ⊢ \underline{b} ⇒ \underline{c} ⊢ \underline{c}]

[Lem1.11g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ ¬\underline{a} ⇒ \underline{b} ⊢ \underline{b}]

[MT →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ ¬\underline{b} ⊢ ¬\underline{a}]

[Lem1.11c →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⇒ \underline{a} ⇒ \underline{b}]

[Lem1.11c →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ Repetition ⊳ ¬\underline{a} ≫ ¬\underline{a}; A1′ ≫ \underline{a} ⇒ ¬\underline{b} ⇒ \underline{a}; MP ⊳ \underline{a} ⇒ ¬\underline{b} ⇒ \underline{a} ⊳ \underline{a} ≫ ¬\underline{b} ⇒ \underline{a}; A1′ ≫ ¬\underline{a} ⇒ ¬\underline{b} ⇒ ¬\underline{a}; MP ⊳ ¬\underline{a} ⇒ ¬\underline{b} ⇒ ¬\underline{a} ⊳ ¬\underline{a} ≫ ¬\underline{b} ⇒ ¬\underline{a}; Neg ⊳ ¬\underline{b} ⇒ ¬\underline{a} ⊳ ¬\underline{b} ⇒ \underline{a} ≫ \underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ \underline{b} ≫ \underline{a} ⇒ \underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⊢ \underline{a} ⇒ \underline{b} ≫ ¬\underline{a} ⇒ \underline{a} ⇒ \underline{b}⌉, p_{0}, c)]

[Cor1.10a →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⊢ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⇒ \underline{c}]

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

[Cor1.10b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{b} ⊢ \underline{a} ⇒ \underline{c}]

[Cor1.10b →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{b} ⊢ 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}; A1′ ≫ \underline{b} ⇒ \underline{a} ⇒ \underline{b}; MP ⊳ \underline{b} ⇒ \underline{a} ⇒ \underline{b} ⊳ \underline{b} ≫ \underline{a} ⇒ \underline{b}; MP ⊳ \underline{a} ⇒ \underline{b} ⇒ \underline{a} ⇒ \underline{c} ⊳ \underline{a} ⇒ \underline{b} ≫ \underline{a} ⇒ \underline{c}⌉, p_{0}, c)]

[Lem1.11a →^{stmt} S ⊢ ∀\underline{a}: ¬¬\underline{a} ⇒ \underline{a}] [Lem1.11a →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: Neg′ ≫ ¬\underline{a} ⇒ ¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬\underline{a} ⇒ \underline{a}; Repetition′ ≫ ¬\underline{a} ⇒ ¬\underline{a}; Cor1.10b ⊳ ¬\underline{a} ⇒ ¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬\underline{a} ⇒ \underline{a} ⊳ ¬\underline{a} ⇒ ¬\underline{a} ≫ ¬\underline{a} ⇒ ¬¬\underline{a} ⇒ \underline{a}; A1′ ≫ ¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬¬\underline{a}; Cor1.10a ⊳ ¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬¬\underline{a} ⊳ ¬\underline{a} ⇒ ¬¬\underline{a} ⇒ \underline{a} ≫ ¬¬\underline{a} ⇒ \underline{a}⌉, p_{0}, c)]

[Lem1.11b →^{stmt} S ⊢ ∀\underline{a}: \underline{a} ⇒ ¬¬\underline{a}]

[Lem1.11b →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: Neg′ ≫ ¬¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬¬¬\underline{a} ⇒ \underline{a} ⇒ ¬¬\underline{a}; Lem1.11a ≫ ¬¬¬\underline{a} ⇒ ¬\underline{a}; MP ⊳ ¬¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬¬¬\underline{a} ⇒ \underline{a} ⇒ ¬¬\underline{a} ⊳ ¬¬¬\underline{a} ⇒ ¬\underline{a} ≫ ¬¬¬\underline{a} ⇒ \underline{a} ⇒ ¬¬\underline{a}; A1′ ≫ \underline{a} ⇒ ¬¬¬\underline{a} ⇒ \underline{a}; Cor1.10a ⊳ \underline{a} ⇒ ¬¬¬\underline{a} ⇒ \underline{a} ⊳ ¬¬¬\underline{a} ⇒ \underline{a} ⇒ ¬¬\underline{a} ≫ \underline{a} ⇒ ¬¬\underline{a}⌉, p_{0}, c)]

[Prop3.2c′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⇒ \underline{b} = \underline{c} ⇒ \underline{a} = \underline{c}]

[Prop3.2c′ →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{b} = \underline{c} ⊢ Prop 3.2c ⊳ \underline{a} = \underline{b} ⊳ \underline{b} = \underline{c} ≫ \underline{a} = \underline{c}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{b} = \underline{c} ⊢ \underline{a} = \underline{c} ≫ \underline{b} = \underline{c} ⇒ \underline{a} = \underline{c}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{b} = \underline{c} ⇒ \underline{a} = \underline{c} ≫ \underline{a} = \underline{b} ⇒ \underline{b} = \underline{c} ⇒ \underline{a} = \underline{c}⌉, p_{0}, c)]

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

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

[Neg′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⇒ ¬\underline{b} ⇒ \underline{a} ⇒ \underline{b}]

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

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

[Repetition′ →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{a}: \underline{a} ⊢ Repetition ⊳ \underline{a} ≫ \underline{a}; Ded ⊳ ∀\underline{a}: \underline{a} ⊢ \underline{a} ≫ \underline{a} ⇒ \underline{a}⌉, p_{0}, c)]

[H10 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = \underline{a} ⊢ ¬\underline{a} = \underline{b}]

[H10 →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = \underline{a} ⊢ Prop3.2b′ ≫ \underline{a} = \underline{b} ⇒ \underline{b} = \underline{a}; Lem1.11e ≫ \underline{a} = \underline{b} ⇒ \underline{b} = \underline{a} ⇒ ¬\underline{b} = \underline{a} ⇒ ¬\underline{a} = \underline{b}; MP ⊳ \underline{a} = \underline{b} ⇒ \underline{b} = \underline{a} ⇒ ¬\underline{b} = \underline{a} ⇒ ¬\underline{a} = \underline{b} ⊳ \underline{a} = \underline{b} ⇒ \underline{b} = \underline{a} ≫ ¬\underline{b} = \underline{a} ⇒ ¬\underline{a} = \underline{b}; MP ⊳ ¬\underline{b} = \underline{a} ⇒ ¬\underline{a} = \underline{b} ⊳ ¬\underline{b} = \underline{a} ≫ ¬\underline{a} = \underline{b}⌉, p_{0}, c)]

[MT →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ ¬\underline{b} ⊢ ¬\underline{a}]

[MT →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ ¬\underline{b} ⊢ Lem1.11a ≫ ¬¬\underline{a} ⇒ \underline{a}; Cor1.10a ⊳ ¬¬\underline{a} ⇒ \underline{a} ⊳ \underline{a} ⇒ \underline{b} ≫ ¬¬\underline{a} ⇒ \underline{b}; ∀\underline{a}: ∀\underline{b}: ¬¬\underline{a} ⇒ \underline{b} ⊢ ¬\underline{b} ⊢ A1′ ≫ ¬\underline{b} ⇒ ¬¬\underline{a} ⇒ ¬\underline{b}; MP ⊳ ¬\underline{b} ⇒ ¬¬\underline{a} ⇒ ¬\underline{b} ⊳ ¬\underline{b} ≫ ¬¬\underline{a} ⇒ ¬\underline{b}; Neg ⊳ ¬¬\underline{a} ⇒ ¬\underline{b} ⊳ ¬¬\underline{a} ⇒ \underline{b} ≫ ¬\underline{a}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬¬\underline{a} ⇒ \underline{b} ⊢ ¬\underline{b} ⊢ ¬\underline{a} ≫ ¬¬\underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a}; MP ⊳ ¬¬\underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a} ⊳ ¬¬\underline{a} ⇒ \underline{b} ≫ ¬\underline{b} ⇒ ¬\underline{a}; MP ⊳ ¬\underline{b} ⇒ ¬\underline{a} ⊳ ¬\underline{b} ≫ ¬\underline{a}⌉, p_{0}, c)]

[Lem1.11e →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a}]

[Lem1.11e →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ Lem1.11a ≫ ¬¬\underline{a} ⇒ \underline{a}; Cor1.10a ⊳ ¬¬\underline{a} ⇒ \underline{a} ⊳ \underline{a} ⇒ \underline{b} ≫ ¬¬\underline{a} ⇒ \underline{b}; Lem1.11b ≫ \underline{b} ⇒ ¬¬\underline{b}; Cor1.10a ⊳ ¬¬\underline{a} ⇒ \underline{b} ⊳ \underline{b} ⇒ ¬¬\underline{b} ≫ ¬¬\underline{a} ⇒ ¬¬\underline{b}; Lem1.11d ≫ ¬¬\underline{a} ⇒ ¬¬\underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a}; MP ⊳ ¬¬\underline{a} ⇒ ¬¬\underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a} ⊳ ¬¬\underline{a} ⇒ ¬¬\underline{b} ≫ ¬\underline{b} ⇒ ¬\underline{a}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ ¬\underline{b} ⇒ ¬\underline{a} ≫ \underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a}⌉, p_{0}, c)]

[Lem1.11d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⇒ \underline{a} ⇒ \underline{b}]

[Lem1.11d →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⊢ Neg′ ≫ ¬\underline{b} ⇒ ¬\underline{a} ⇒ ¬\underline{b} ⇒ \underline{a} ⇒ \underline{b}; A1′ ≫ \underline{a} ⇒ ¬\underline{b} ⇒ \underline{a}; MP ⊳ ¬\underline{b} ⇒ ¬\underline{a} ⇒ ¬\underline{b} ⇒ \underline{a} ⇒ \underline{b} ⊳ ¬\underline{b} ⇒ ¬\underline{a} ≫ ¬\underline{b} ⇒ \underline{a} ⇒ \underline{b}; Cor1.10a ⊳ \underline{a} ⇒ ¬\underline{b} ⇒ \underline{a} ⊳ ¬\underline{b} ⇒ \underline{a} ⇒ \underline{b} ≫ \underline{a} ⇒ \underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⊢ \underline{a} ⇒ \underline{b} ≫ ¬\underline{b} ⇒ ¬\underline{a} ⇒ \underline{a} ⇒ \underline{b}⌉, p_{0}, c)]

[Prop3.2b′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⇒ \underline{b} = \underline{a}]

[Prop3.2b′ →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ Prop 3.2b ⊳ \underline{a} = \underline{b} ≫ \underline{b} = \underline{a}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ \underline{b} = \underline{a} ≫ \underline{a} = \underline{b} ⇒ \underline{b} = \underline{a}⌉, p_{0}, c)]

[Lem1.11g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ ¬\underline{a} ⇒ \underline{b} ⊢ \underline{b}]

[Lem1.11g →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⇒ \underline{b} ⊢ ¬\underline{a} ⇒ \underline{b} ⊢ Lem1.11e ≫ \underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a}; MP ⊳ \underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬\underline{a} ⊳ \underline{a} ⇒ \underline{b} ≫ ¬\underline{b} ⇒ ¬\underline{a}; Lem1.11e ≫ ¬\underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬¬\underline{a}; MP ⊳ ¬\underline{a} ⇒ \underline{b} ⇒ ¬\underline{b} ⇒ ¬¬\underline{a} ⊳ ¬\underline{a} ⇒ \underline{b} ≫ ¬\underline{b} ⇒ ¬¬\underline{a}; Neg ⊳ ¬\underline{b} ⇒ ¬¬\underline{a} ⊳ ¬\underline{b} ⇒ ¬\underline{a} ≫ \underline{b}⌉, p_{0}, c)]

[H11 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} ⇒ \underline{b} ⊢ \underline{a} ⇒ \underline{c} ⊢ \underline{b} ⇒ \underline{c} ⊢ \underline{c}]

[H11 →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} ⇒ \underline{b} ⊢ \underline{a} ⇒ \underline{c} ⊢ \underline{b} ⇒ \underline{c} ⊢ Cor1.10a ⊳ ¬\underline{a} ⇒ \underline{b} ⊳ \underline{b} ⇒ \underline{c} ≫ ¬\underline{a} ⇒ \underline{c}; Lem1.11g ⊳ \underline{a} ⇒ \underline{c} ⊳ ¬\underline{a} ⇒ \underline{c} ≫ \underline{c}⌉, p_{0}, c)]

Litteratur

[Gru06] K. Grue. A logiweb base page. Technical report, Logiweb, 2006.

        http://www.diku.dk/cgi-bin/cginetd/grue/relay/go/
        01693B66F0C393B695F3F15770898897A683141109C083AC838ADCA20806/2/.

[Men97] E. Mendelson. Introduction to Mathematical Logic. Chapmann & Hall, 4. edition, 1997.