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 3 4.1 3.2j . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 4.2 3.2k . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 4.3 3.2l . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 4.4 3.2m . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 4.5 3.2n . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 4.6 3.2o . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

5 Udsagn 3.4 10 5.1 3.4a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 5.2 3.4b . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 5.3 3.4c . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 5.4 3.4d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

6 Udsagn 3.5 13

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

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

6.3 3.5a . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 6.4 3.5b . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 6.5 3.5c . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 6.6 3.5d . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 6.7 3.5e . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 6.8 3.5f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 6.9 3.5g . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 6.10 3.5h . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

7 Udsagn 3.7 25 7.1 Definitioner af x < y . . . . . . . . . . . . . . . . . . . . . . . . . 25

A Hjælpe lemmaer 25

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 x | y, 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 basisresultaterne for tal-teori. Aksiomerne for S er følgende.

1Kursus 061004/202 Logik

2Eng.: proposition

3Eng.: theorem

[Theory S] [S rule MP: ΠA, B: A ⇒ B ⊢ A ⊢ B]

[S rule Gen: ΠX , A: A ⊢ ∀X : A] [S rule Ded: ΠA, B: Ded(A, B) ⊢⊢ A ⊢ B]

[S rule S2: ΠA, B: A = B ⊢ A′ = B′]

[S rule S3: ΠA: ¬0 = A′] [S rule S4: ΠA, B: A′ = B′ ⊢ A = B]

[S rule S5: ΠA: A + 0 = A] [S rule S6: ΠA, B: A + B′ = (A + B)′]

[S rule S7: ΠA: A · 0 = 0] [S rule S8: ΠA, B: A · (B′) = (A · B) + A]

[S rule S1: ΠA, B, C: A = B ⊢ A = C ⊢ B = C]

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:

[S rule S9: ΠX , A, B, C: ⟨B≡A|X:=0⟩ ⊢⊢ ⟨C≡A|X:=X′⟩ ⊢⊢ B ⊢ A ⇒ C ⊢ A]

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:

[S rule Neg: ΠA: ΠB: ¬B ⇒ ¬A ⊢ ¬B ⇒ A ⊢ B]

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 A, B, C følgende velformulerede sætninger^{4} i systemet S:

4Eng.: Wellformed formulas

[S lemma Prop 3.2a: ΠA: A = A] [S lemma Prop 3.2b: ΠA, B: A = B ⊢ B = A] [S lemma Prop 3.2c: ΠA, B, C: A = B ⊢ B = C ⊢ A = C] [S lemma Prop 3.2d: ΠA, B, C: A = C ⊢ B = C ⊢ A = B] [S lemma Prop 3.2e: ΠA, B, C: A = B ⊢ A + C = B + C] [S lemma Prop 3.2f : ΠA: A = 0 + A] [S lemma Prop 3.2g: ΠA, B: A′ + B = (A + B)′] [S lemma Prop 3.2h: ΠA, B: A + B = B + A]

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

[S lemma Prop 3.2i: ΠA, B, C: A = B ⊢ C + A = C + B] S proof of Prop 3.2i:

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B, C  ;
L04: Premise ≫  A = B  ;
L05: Prop 3.2e ⊳ L04 ≫  A + C = B + C  ;
L06: Prop 3.2h ≫  A + C = C + A  ;
L07: Prop 3.2h ≫  B + C = C + B  ;
L08: S1 ⊳ L05 ⊳ L06 ≫  B + C = C + A  ;
L09: Prop 3.2b ⊳ L08 ≫  C + A = B + C  ;
L10: Prop 3.2c ⊳ L09 ⊳ L07 ≫  C + A = C + B  ;
L11: Block ≫  End  ;
L12: Ded ⊳ L11 ≫  A = B ⊢ C + A = C + B  □

De følgende lemmaer er opskrevet, men ikke bevist i Mendelson. Disse er blandt dem som vi ønsker at bevise. [S lemma Prop 3.2j: ΠA, B, C: (A + B) + C = A + (B + C)] [S lemma Prop 3.2k: ΠA, B, C: A = B ⊢ A · C = B · C] [S lemma Prop 3.2l: ΠA: 0 · A = 0] [S lemma Prop 3.2m: ΠA, B: A′ · B = A · B + B] [S lemma Prop 3.2n: ΠA, B: A · B = B · A] [S lemma Prop 3.2o: ΠA, B, C: A = B ⊢ C · A = C · B]

Her efter følger beviserne.

4.1 3.2j

[S lemma Prop 3.2j_{1} : ΠA, B: (A + B) + 0 = A + (B + 0)] S proof of Prop 3.2j_{1} :

L01: Arbitrary ≫  A, B  ;
L02: S5 ≫  (A + B) + 0 = A + B  ;
L03: S5 ≫  B + 0 = B  ;
L04: Prop 3.2i ⊳ L03 ≫  A + (B + 0) = A + B  ;
L05: Prop 3.2d ⊳ L02 ⊳ L04 ≫  (A + B) + 0 = A + (B + 0)  □

[S lemma Prop 3.2j_{2} : ΠA, B, C: (A + B) + C = A + (B + C) ⇒ (A + B) + C′ = A + (B + C′)] S proof of Prop 3.2j_{2} :

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B, C  ;
L04: Premise ≫  (A + B) + C = A + (B + C) ;
L05: S6 ≫  (A + B) + C′ = ((A + B) + C)′ ;
L06: S2 ⊳ L04 ≫  ((A+B)+C)′ = (A+(B+C))′ ;
L07: Prop 3.2c ⊳ L05 ⊳ L06 ≫  (A + B) + C′ = (A + (B + C))′ ;
L08: S6 ≫ B + C′ = (B + C)′ ;
L09: Prop 3.2i ⊳ L08 ≫  A + (B + C′) = A + (B + C)′ ;
L10: S6 ≫  A + (B + C)′ = (A + (B + C))′ ;
L11: Prop 3.2c ⊳ L09 ⊳ L10 ≫  A + (B + C′) = (A + (B + C))′ ;
L12: Prop 3.2d ⊳ L07 ⊳ L11 ≫  (A + B) + C′ = A + (B + C′) ;
L13: Block ≫ End ;
L14: Ded ⊳ L13 ≫  {(A + B) + C = A + (B + C) ⇒ \atop (A + B) + C′ = A + (B + C′) □}

[S lemma Prop 3.2j: ΠA, B, C: (A + B) + C = A + (B + C)] S proof of Prop 3.2j:

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Prop 3.2j_{1} ≫  (x + y) + 0 = x + (y + 0)  ;

L04: Prop 3.2j_{2} ≫

(x + y) + z = x + (y + z) ⇒
(x + y) + z′ = x + (y + z′) ;
L05: S9 @ z ⊳ L03 ⊳ L04 ≫  (x + y) + z = x + (y + z)  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  (A + B) + C = A + (B + C)  □

4.2 3.2k

[S lemma Prop 3.2k_{1} : ΠA, B: A = B ⇒ A · 0 = B · 0] S proof of Prop 3.2k_{1} :

L01: Arbitrary ≫  A, B  ;

L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A = B  ;
L05: S7 ≫  A · 0 = 0  ;
L06: S7 ≫  B · 0 = 0  ;
L07: Prop 3.2a ≫  0 = 0  ;
L08: Prop 3.2b ⊳ L06 ≫  0 = B · 0  ;
L09: Prop 3.2c ⊳ L05 ⊳ L08 ≫  A · 0 = B · 0  ;
L10: Block ≫  End  ;
L11: Ded ⊳ L10 ≫  A = B ⇒ A · 0 = B · 0  □

[S lemma Prop 3.2k_{2} : ΠA, B, C: (A = B ⇒ A · C = B · C) ⇒ (A = B ⇒ A · C′ = B · C′)] S proof of Prop 3.2k_{2} :

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B, C  ;
L04: Premise ≫  A = B ⇒ A · C = B · C  ;
L05: Premise ≫  A = B  ;
L06: L04 ⊵ L05 ≫  A · C = B · C  ;
L07: S8 ≫  A · C′ = A · C + A  ;
L08: S8 ≫  B · C′ = B · C + B  ;
L09: Prop 3.2e ⊳ L06 ≫  (A · C) + A = (B · C) + A  ;
L10: Prop 3.2i ⊳ L05 ≫  (B · C) + A = (B · C) + B  ;
L11: Prop 3.2c ⊳ L09 ⊳ L10 ≫  A · C + A = B · C + B  ;
L12: Prop 3.2c ⊳ L07 ⊳ L11 ≫  A · C′ = B · C + B  ;
L13: Prop 3.2d ⊳ L12 ⊳ L08 ≫  A · C′ = B · C′  ;
L14: Block ≫  End  ;
L15: Ded ⊳ L14 ≫  {(A = B ⇒ A·C = B·C) ⇒ (A = \atop B ⇒ A · C′ = B · C′)  □}

[S lemma Prop 3.2k: ΠA, B, C: A = B ⊢ A · C = B · C] S proof of Prop 3.2k:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A = B  ;
L03: Block ≫  Begin  ;
L04: Prop 3.2k_{1} ≫  x = y ⇒ x · 0 = y · 0  ;

L05: Prop 3.2k_{2} ≫

(x = y ⇒ x ·z = y ·z) ⇒ (x =
y ⇒ x · z′ = y · z′) ;
L06: S9 @ z ⊳ L04 ⊳ L05 ≫  x = y ⇒ x · z = y · z  ;
L07: Block ≫  End  ;
L08: Ded ⊳ L07 ≫  A = B ⇒ A · C = B · C  ;
L09: L08 ⊵ L02 ≫  A · C = B · C  □

4.3 3.2l

[S lemma Prop 3.2l_{2} : ΠA: 0 · A = 0 ⇒ 0 · A′ = 0] S proof of Prop 3.2l_{2} :

L01: Arbitrary ≫  A  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A  ;
L04: Premise ≫  0 · A = 0  ;
L05: S8 ≫  0 · A′ = 0 · A + 0  ;
L06: S5 ≫  0 · A + 0 = 0 · A  ;
L07: Prop 3.2c ⊳ L05 ⊳ L06 ≫  0 · A′ = 0 · A  ;
L08: Prop 3.2c ⊳ L07 ⊳ L04 ≫  0 · A′ = 0  ;
L09: Block ≫  End  ;
L10: Ded ⊳ L09 ≫  0 · A = 0 ⇒ 0 · A′ = 0  □

[S lemma Prop 3.2l: ΠA: 0 · A = 0] S proof of Prop 3.2l:

L01: Arbitrary ≫  A  ;
L02: Block ≫  Begin  ;
L03: S7 ≫  0 · 0 = 0  ;
L04: Prop 3.2l_{2} ≫  0 · x = 0 ⇒ 0 · x′ = 0  ;
L05: S9 @ x ⊳ L03 ⊳ L04 ≫  0 · x = 0  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  0 · A = 0  □

4.4 3.2m

[S lemma Prop 3.2m_{1} : ΠA: A′ · 0 = A · 0 + 0] S proof of Prop 3.2m_{1} :

L01: Arbitrary ≫  A  ;
L02: S7 ≫  A′ · 0 = 0  ;
L03: Prop 3.2f ≫  0 = 0 + 0  ;
L04: S7 ≫  A · 0 = 0  ;
L05: Prop 3.2b ⊳ L04 ≫  0 = A · 0  ;
L06: Prop 3.2e ⊳ L05 ≫  0 + 0 = A · 0 + 0  ;
L07: Prop 3.2c ⊳ L03 ⊳ L06 ≫  0 = A · 0 + 0  ;
L08: Prop 3.2c ⊳ L02 ⊳ L07 ≫  A′ · 0 = A · 0 + 0  ;

[S lemma Prop 3.2m_{2} : ΠA, B: A′ · B = A · B + B ⇒ A′ · B′ = A · B′ + B′] S proof of Prop 3.2m_{2} :

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A′ · B = A · B + B  ;

L05: S8 ≫  A′ · B′ = A′ · B + A′  ;
L06: Prop 3.2e ⊳ L04 ≫  (A′ ·B)+A′ = (A·B+B)+A′ ;
L07: S6 ≫  B + A′ = (B + A)′  ;
L08: Prop 3.2g ≫  B′ + A = (B + A)′  ;
L09: Prop 3.2d ⊳ L07 ⊳ L08 ≫  B + A′ = B′ + A  ;
L10: Prop 3.2h ≫  B′ + A = A + B′  ;
L11: Prop 3.2c ⊳ L09 ⊳ L10 ≫  B + A′ = A + B′  ;
L12: Prop 3.2i ⊳ L11 ≫  {A·B +(B +A′) = A·B +(A+ \atop B′)  ;}
L13: Prop 3.2j ≫  {(A·B +A)+B′ = A·B +(A+ \atop B′)  ;}
L14: Prop 3.2d ⊳ L12 ⊳ L13 ≫  {A · B + (B + A′) = (A · B + \atop A) + B′  ;}
L15: S8 ≫  A · B′ = A · B + A  ;
L16: Prop 3.2e ⊳ L15 ≫  A · B′ + B′ = (A · B + A) + B′ ;
L17: Prop 3.2d ⊳ L14 ⊳ L16 ≫  A · B + (B + A′) = A · B′ + B′ ;
L18: Prop 3.2j ≫ {(A·B +B)+A′ = A·B +(B + \atop A′) ;}
L19: Prop 3.2c ⊳ L06 ⊳ L18 ≫  (A′ ·B)+A′ = A·B+(B+A′) ;
L20: Prop 3.2c ⊳ L19 ⊳ L17 ≫  (A′ · B) + A′ = A · B′ + B′  ;
L21: Prop 3.2c ⊳ L05 ⊳ L20 ≫  A′ · B′ = A · B′ + B′  ;
L22: Block ≫  End  ;
L23: Ded ⊳ L22 ≫  {A′ · B = A · B + B ⇒ A′ · B′ = \atop A · B′ + B′  □}

[S lemma Prop 3.2m: ΠA, B: A′ · B = A · B + B] S proof of Prop 3.2m:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Prop 3.2m_{1} ≫  x′ · 0 = x · 0 + 0  ;

L04: Prop 3.2m_{2} ≫

(x′ · y = x · y + y) ⇒ (x′ · y′ =
x · y′ + y′) ;
L05: S9 @ y ⊳ L03 ⊳ L04 ≫  x′ · y = x · y + y  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  A′ · B = A · B + B  □

4.5 3.2n

[S lemma Prop 3.2n_{1} : ΠA: A · 0 = 0 · A] S proof of Prop 3.2n_{1} :

L01: Arbitrary ≫  A  ;
L02: S7 ≫  A · 0 = 0  ;
L03: Prop 3.2l ≫  0 · A = 0  ;
L04: Prop 3.2d ⊳ L02 ⊳ L03 ≫  A · 0 = 0 · A  □

[S lemma Prop 3.2n_{2} : ΠA, B: A · B = B · A ⇒ A · B′ = B′ · A] S proof of Prop 3.2n_{2} :

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A · B = B · A  ;
L05: S8 ≫  A · B′ = A · B + A  ;
L06: Prop 3.2e ⊳ L04 ≫  A · B + A = B · A + A  ;
L07: Prop 3.2m ≫  B′ · A = B · A + A  ;
L08: Prop 3.2b ⊳ L07 ≫  B · A + A = B′ · A  ;
L09: Prop 3.2c ⊳ L06 ⊳ L08 ≫  A · B + A = B′ · A  ;
L10: Prop 3.2c ⊳ L05 ⊳ L09 ≫  A · B′ = B′ · A  ;
L11: Block ≫  End  ;
L12: Ded ⊳ L11 ≫  A · B = B · A ⇒ A · B′ = B′ · A □

[S lemma Prop 3.2n: ΠA, B: A · B = B · A] S proof of Prop 3.2n:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Prop 3.2n_{1} ≫  x · 0 = 0 · x  ;
L04: Prop 3.2n_{2} ≫  (x ·y = y ·x) ⇒ (x ·y′ = y′ ·x) ;
L05: S9 @ y ⊳ L03 ⊳ L04 ≫  x · y = y · x  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  A · B = B · A  □

4.6 3.2o

[S lemma Prop 3.2o: ΠA, B, C: A = B ⊢ C · A = C · B] S proof of Prop 3.2o:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A = B  ;
L03: Block ≫  Begin  ;
L04: Arbitrary ≫  A, B, C  ;
L05: Premise ≫  A = B  ;
L06: Prop 3.2k ⊳ L05 ≫  A · C = B · C  ;
L07: Prop 3.2n ≫  A · C = C · A  ;
L08: Prop 3.2n ≫  B · C = C · B  ;
L09: Prop 3.2c ⊳ L06 ⊳ L08 ≫  A · C = C · B  ;
L10: S1 ⊳ L07 ⊳ L09 ≫  C · A = C · B  ;
L11: Block ≫  End  ;
L12: Ded ⊳ L11 ≫  A = B ⇒ C · A = C · B  ;
L13: L12 ⊵ L02 ≫  C · A = C · B  □

5 Udsagn 3.4

De følgende udsagn er en udvidelse af egenskaberne ved addition og multiplikation. [S lemma Prop 3.4a: ΠA, B, C: A · (B + C) = (A · B) + (A · C)] [S lemma Prop 3.4b: ΠA, B, C: (B + C) · A = (B · A) + (C · A)] [S lemma Prop 3.4c: ΠA, B, C: (A · B) · C = A · (B · C)] [S lemma Prop 3.4d: ΠA, B, C: A + C = B + C ⇒ A = B]

5.1 3.4a

[S lemma Prop 3.4a_{1} : ΠA, B: A · (B + 0) = A · B + A · 0] S proof of Prop 3.4a_{1} :

L01: Arbitrary ≫  A, B  ;
L02: S5 ≫  (B + 0) = (B)  ;
L03: Prop 3.2o ⊳ L02 ≫  A · (B + 0) = A · (B)  ;
L04: S5 ≫  A · B + 0 = A · B  ;
L05: Prop 3.2d ⊳ L03 ⊳ L04 ≫  A · (B + 0) = A · B + 0  ;
L06: S7 ≫  A · 0 = 0  ;
L07: Prop 3.2i ⊳ L06 ≫  A · B + A · 0 = A · B + 0  ;
L08: Prop 3.2d ⊳ L05 ⊳ L07 ≫  A · (B + 0) = A · B + A · 0  □

[S lemma Prop 3.4a_{2} : ΠA, B, C: A · (B + C) = A · B + A · C ⇒ A · (B + C′) = A · B + A · C′] S proof of Prop 3.4a_{2} :

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B, C  ;
L04: Premise ≫  A · (B + C) = A · B + A · C  ;
L05: S6 ≫  B + C′ = (B + C)′  ;
L06: Prop 3.2o ⊳ L05 ≫  A · (B + C′) = A · (B + C)′  ;
L07: S8 ≫  A · (B + C)′ = A · (B + C) + A ;
L08: Prop 3.2e ⊳ L04 ≫  {(A · (B + C)) + A = (A · B + \atop A · C) + A  ;}
L09: Prop 3.2j ≫  {(A · B + A · C) + A = A · B + \atop (A · C + A)  ;}
L10: Prop 3.2c ⊳ L08 ⊳ L09 ≫  {(A · (B + C)) + A = A · B + \atop (A · C + A)  ;}
L11: S8 ≫  A · C′ = A · C + A  ;
L12: Prop 3.2i ⊳ L11 ≫  A·B+A·C′ = A·B+(A·C+A) ;
L13: Prop 3.2d ⊳ L10 ⊳ L12 ≫  A·(B +C)+A = A·B +A·C′ ;
L14: Prop 3.2c ⊳ L07 ⊳ L13 ≫  A · (B + C)′ = A · B + A · C′ ;

L15: Prop 3.2c ⊳ L06 ⊳ L14 ≫  A · (B + C′) = A · B + A · C′ ;
L16: Block ≫  End  ;
L17: Ded ⊳ L16 ≫  {(A · (B + C) = A · B + A · C) ⇒ \atop A · (B + C′) = A · B + A · C′  □}

[S lemma Prop 3.4a: ΠA, B, C: A · (B + C) = (A · B) + (A · C)] S proof of Prop 3.4a:

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Prop 3.4a_{1} ≫  x · (y + 0) = x · y + x · 0  ;

L04: Prop 3.4a_{2} ≫

(x · (y + z) = x · y + x · z) ⇒
(x · (y + z′) = x · y + x · z′) ;
L05: S9 @ z ⊳ L03 ⊳ L04 ≫  x · (y + z) = x · y + x · z  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  A · (B + C) = A · B + A · C  □

5.2 3.4b

[S lemma Prop 3.4b: ΠA, B, C: (B + C) · A = (B · A) + (C · A)] S proof of Prop 3.4b:

L01: Arbitrary ≫  A, B, C  ;
L02: Prop 3.4a ≫  A · (B + C) = A · B + A · C  ;
L03: Prop 3.2n ≫  A · (B + C) = (B + C) · A  ;
L04: Prop 3.2n ≫  A · B = B · A  ;
L05: Prop 3.2n ≫  A · C = C · A  ;
L06: S1 ⊳ L03 ⊳ L02 ≫  (B + C) · A = A · B + A · C  ;
L07: Prop 3.2e ⊳ L04 ≫  A · B + A · C = B · A + A · C  ;
L08: Prop 3.2i ⊳ L05 ≫  B · A + A · C = B · A + C · A  ;
L09: Prop 3.2c ⊳ L07 ⊳ L08 ≫  A · B + A · C = B · A + C · A  ;
L10: Prop 3.2c ⊳ L06 ⊳ L09 ≫  (B + C) · A = B · A + C · A  □

5.3 3.4c

[S lemma Prop 3.4c_{1} : ΠA, B: (A · B) · 0 = A · (B · 0)] S proof of Prop 3.4c_{1} :

L01: Arbitrary ≫  A, B  ;
L02: S7 ≫  (A · B) · 0 = 0  ;
L03: S7 ≫  B · 0 = 0  ;
L04: Prop 3.2o ⊳ L03 ≫  A · (B · 0) = A · 0  ;
L05: S7 ≫  A · 0 = 0  ;
L06: Prop 3.2c ⊳ L04 ⊳ L05 ≫  A · (B · 0) = 0  ;
L07: Prop 3.2d ⊳ L02 ⊳ L06 ≫  (A · B) · 0 = A · (B · 0)  □

[S lemma Prop 3.4c_{2} : ΠA, B, C: (A·B)·C = A·(B·C) ⇒ (A·B)·C′ = A·(B·C′)] S proof of Prop 3.4c_{2} :

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B, C  ;
L04: Premise ≫  (A · B) · C = A · (B · C)  ;
L05: S8 ≫  (A·B)·C′ = (A·B)·C +(A·B) ;
L06: Prop 3.2e ⊳ L04 ≫ {((A · B) · C) + (A · B) = (A · \atop (B · C)) + (A · B) ;}
L07: Prop 3.2c ⊳ L05 ⊳ L06 ≫  (A·B)·C′ = (A·(B·C))+(A·B) ;
L08: Prop 3.4a ≫ {A · ((B · C) + B) = A · (B · C) + \atop A · B ;}
L09: Prop 3.2d ⊳ L07 ⊳ L08 ≫  (A · B) · C′ = A · ((B · C) + B) ;
L10: S8 ≫ B · C′ = B · C + B ;
L11: Prop 3.2o ⊳ L10 ≫  A · (B · C′) = A · (B · C + B) ;
L12: Prop 3.2d ⊳ L09 ⊳ L11 ≫  (A · B) · C′ = A · (B · C′)  ;
L13: Block ≫  End  ;
L14: Ded ⊳ L13 ≫  {(A · B) · C = A · (B · C) ⇒ (A · \atop B) · C′ = A · (B · C′)  □}

[S lemma Prop 3.4c: ΠA, B, C: (A · B) · C = A · (B · C)] S proof of Prop 3.4c:

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Prop 3.4c_{1} ≫  (x · y) · 0 = x · (y · 0)  ;

L04: Prop 3.4c_{2} ≫

(x · y) · z = x · (y · z) ⇒ (x ·
y) · z′ = x · (y · z′) ;
L05: S9 @ z ⊳ L03 ⊳ L04 ≫  (x · y) · z = x · (y · z)  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  (A · B) · C = A · (B · C)  □

5.4 3.4d

[S lemma Prop 3.4d_{1} : ΠA, B: A + 0 = B + 0 ⇒ A = B] S proof of Prop 3.4d_{1} :

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A + 0 = B + 0  ;
L05: S5 ≫  A + 0 = A  ;
L06: S5 ≫  B + 0 = B  ;
L07: S1 ⊳ L05 ⊳ L04 ≫  A = B + 0  ;
L08: Prop 3.2c ⊳ L07 ⊳ L06 ≫  A = B  ;
L09: Block ≫  End  ;
L10: Ded ⊳ L09 ≫  A + 0 = B + 0 ⇒ A = B  □

[S lemma Prop 3.4d_{2} : ΠA, B, C: (A + C = B + C ⇒ A = B) ⇒ A + C′ = B + C′ ⇒ A = B]

S proof of Prop 3.4d_{2} :

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B, C  ;
L04: Premise ≫  A + C = B + C ⇒ A = B  ;
L05: Premise ≫  A + C′ = B + C′  ;
L06: S6 ≫  A + C′ = (A + C)′  ;
L07: S6 ≫  B + C′ = (B + C)′  ;
L08: S1 ⊳ L06 ⊳ L05 ≫  (A + C)′ = B + C′  ;
L09: Prop 3.2c ⊳ L08 ⊳ L07 ≫  (A + C)′ = (B + C)′  ;
L10: S4 ⊳ L09 ≫  (A + C) = (B + C)  ;
L11: L04 ⊵ L10 ≫  A = B  ;
L12: Block ≫  End  ;
L13: Ded ⊳ L12 ≫  {(A + C = B + C ⇒ A = B) ⇒ \atop A + C′ = B + C′ ⇒ A = B  □}

[S lemma Prop 3.4d: ΠA, B, C: A + C = B + C ⇒ A = B]

S proof of Prop 3.4d:

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Prop 3.4d_{1} ≫  x + 0 = y + 0 ⇒ x = y  ;

L04: Prop 3.4d_{2} ≫

(x + z = y + z ⇒ x = y) ⇒
x + z′ = y + z′ ⇒ x = y ;
L05: S9 @ z ⊳ L03 ⊳ L04 ≫  x + z = y + z ⇒ x = y  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  A + C = B + C ⇒ A = B  □

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å.

[S lemma Prop 3.5a: ΠA: A + \overline{1} = A′] [S lemma Prop 3.5b: ΠA: A · \overline{1} = A] [S lemma Prop 3.5c: ΠA: A · \overline{2} = A + A] [S lemma Prop 3.5d: ΠA, B: A + B = 0 ⇒ A = 0 ∧ B = 0] [S lemma Prop 3.5e: ΠA, B: B ≠ 0 ⇒ (A · B = 0 ⇒ A = 0)] [S lemma Prop 3.5f : ΠA, B: A + B = \overline{1} ⇒ (A = 0 ∧ B = \overline{1}) ∨ (A = \overline{1} ∧ B = 0)] [S lemma Prop 3.5g: ΠA, B: A · B = \overline{1} ⇒ (A = \overline{1} ∧ B = \overline{1})] [S lemma Prop 3.5h: ΠA: A ≠ 0 ⇒ ∃B: A = B′] [S lemma Prop 3.5i: ΠA, B, C: C ≠ 0 ⇒ (A · C = B · C ⇒ A = B)] [S lemma Prop 3.5j: ΠA: A ≠ 0 ⇒ A ≠ \overline{1} ⇒ ∃B: A = 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 ¨= ¬(x ⇒ ¬y)] [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 ∧ [S lemma Con: ΠA, B: A ⊢ B ⊢ A ∧ B] S proof of Con:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A  ;
L03: Premise ≫  B  ;
L04: Block ≫  Begin  ;
L05: Arbitrary ≫  A, B  ;
L06: Premise ≫  A ⇒ ¬B  ;
L07: Repetition ⊳ L02 ≫  A  ;
L08: L06 ⊵ L07 ≫  ¬B  ;

L09: Block ≫  End  ;
L10: Ded ⊳ L09 ≫  (A ⇒ ¬B) ⇒ ¬B  ;
L11: Lem1.11b ≫  B ⇒ ¬¬B  ;
L12: L11 ⊵ L03 ≫  ¬¬B  ;
L13: MT ⊳ L10 ⊳ L12 ≫  ¬(A ⇒ ¬B)  □

6.1.2 Elimination af ∧ 1 [S lemma Con1: ΠA, B: A ∧ B ⊢ A] S proof of Con1:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  ¬(A ⇒ ¬B)  ;
L03: Block ≫  Begin  ;
L04: Arbitrary ≫  A, B  ;
L05: Premise ≫  ¬A  ;
L06: A1′ ≫  ¬A ⇒ ¬¬B ⇒ ¬A  ;
L07: L06 ⊵ L05 ≫  ¬¬B ⇒ ¬A  ;
L08: Lem1.11d ≫  (¬¬B ⇒ ¬A) ⇒ A ⇒ ¬B  ;
L09: L08 ⊵ L07 ≫  A ⇒ ¬B  ;
L10: Block ≫  End  ;
L11: Ded ⊳ L10 ≫  (¬A) ⇒ (A ⇒ ¬B)  ;
L12: MT ⊳ L11 ⊳ L02 ≫  ¬¬A  ;
L13: Lem1.11a ≫  ¬¬A ⇒ A  ;
L14: L13 ⊵ L12 ≫  A  □

6.1.3 Elimination af ∧ 2 [S lemma Con2: ΠA, B: A ∧ B ⊢ B] S proof of Con2:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  ¬(A ⇒ ¬B)  ;
L03: Block ≫  Begin  ;
L04: Arbitrary ≫  A, B  ;
L05: Premise ≫  ¬B  ;
L06: A1′ ≫  ¬B ⇒ A ⇒ ¬B  ;
L07: L06 ⊵ L05 ≫  A ⇒ ¬B  ;
L08: Block ≫  End  ;
L09: Ded ⊳ L08 ≫  ¬B ⇒ A ⇒ ¬B  ;
L10: MT ⊳ L09 ⊳ L02 ≫  ¬¬B  ;
L11: Lem1.11a ≫  ¬¬B ⇒ B  ;
L12: L11 ⊵ L10 ≫  B  □

6.1.4 Introduktion af ∨ 1 [S lemma Dis1: ΠA, B: A ⊢ A ∨ B] S proof of Dis1:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A  ;
L03: Lem1.11c ≫  ¬¬A ⇒ (¬A ⇒ B)  ;
L04: Lem1.11b ≫  A ⇒ ¬¬A  ;
L05: L04 ⊵ L02 ≫  ¬¬A  ;
L06: L03 ⊵ L05 ≫  ¬A ⇒ B  □

6.1.5 Introduktion af ∨ 2 [S lemma Dis2: ΠA, B: B ⊢ A ∨ B] S proof of Dis2:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  B  ;
L03: A1′ ≫  B ⇒ ¬A ⇒ B  ;
L04: L03 ⊵ L02 ≫  ¬A ⇒ B  □

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).

[S lemma H3: ΠA, B, C: A ⇒ (B ⇒ C) ⊢ A ⊢ ¬C ⊢ ¬B] S proof of H3:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A ⇒ (B ⇒ C)  ;
L03: Premise ≫  A  ;
L04: Premise ≫  ¬C  ;
L05: L02 ⊵ L03 ≫  B ⇒ C  ;
L06: MT ⊳ L05 ⊳ L04 ≫  ¬B  □

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 ¨= ¬(∀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

[S lemma Prop 3.5a: ΠA: A + \overline{1} = A′]

S proof of Prop 3.5a:

L01: Arbitrary ≫  A  ;
L02: S6 ≫  A + 0′ = (A + 0)′  ;
L03: S5 ≫  A + 0 = A  ;
L04: S2 ⊳ L03 ≫  (A + 0)′ = A′  ;
L05: Prop 3.2c ⊳ L02 ⊳ L04 ≫  A + 0′ = A′  ;
L06: Prop 3.2a ≫  A + 0′ = A + \overline{1}  ;
L07: S1 ⊳ L06 ⊳ L05 ≫  A + \overline{1} = A′  □

6.4 3.5b

[S lemma Prop 3.5b: ΠA: A · \overline{1} = A] S proof of Prop 3.5b:

L01: Arbitrary ≫  A  ;
L02: S8 ≫  A · 0′ = A · 0 + A  ;
L03: S7 ≫  A · 0 = 0  ;
L04: Prop 3.2e ⊳ L03 ≫  A · 0 + A = 0 + A  ;
L05: Prop 3.2c ⊳ L02 ⊳ L04 ≫  A · 0′ = 0 + A  ;
L06: Prop 3.2f ≫  A = 0 + A  ;
L07: Prop 3.2b ⊳ L06 ≫  0 + A = A  ;
L08: Prop 3.2c ⊳ L05 ⊳ L07 ≫  A · 0′ = A  ;
L09: Prop 3.2a ≫  A · 0′ = A · \overline{1}  ;
L10: S1 ⊳ L09 ⊳ L08 ≫  A · \overline{1} = A  □

6.5 3.5c

[S lemma Prop 3.5c: ΠA: A · \overline{2} = A + A] S proof of Prop 3.5c:

L01: Arbitrary ≫  A  ;
L02: S8 ≫  A · \overline{1}′ = A · \overline{1} + A  ;
L03: Prop 3.5b ≫  A · \overline{1} = A  ;
L04: Prop 3.2e ⊳ L03 ≫  A · \overline{1} + A = A + A  ;
L05: Prop 3.2c ⊳ L02 ⊳ L04 ≫  A · \overline{1}′ = A + A  ;
L06: Prop 3.2a ≫  A · \overline{1}′ = A · \overline{2}  ;
L07: S1 ⊳ L06 ⊳ L05 ≫  A · \overline{2} = A + A  □

6.6 3.5d

[S lemma Prop 3.5d_{1} : ΠA: A + 0 = 0 ⇒ (A = 0) ∧ (0 = 0)] S proof of Prop 3.5d_{1} :

L01: Arbitrary ≫  A  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A  ;
L04: Premise ≫  A + 0 = 0  ;
L05: S5 ≫  A + 0 = A  ;
L06: S1 ⊳ L05 ⊳ L04 ≫  A = 0  ;
L07: Prop 3.2a ≫  0 = 0  ;
L08: Con ⊳ L06 ⊳ L07 ≫  A = 0 ∧ 0 = 0  ;
L09: Block ≫  End  ;
L10: Ded ⊳ L09 ≫  A + 0 = 0 ⇒ (A = 0) ∧ (0 = 0) □

[S lemma Prop 3.5d_{2} : ΠA, B: (A + B = 0 ⇒ A = 0 ∧ B = 0) ⇒ A + B′ = 0 ⇒ A = 0 ∧ B′ = 0] S proof of Prop 3.5d_{2} :

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;

L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A + B = 0 ⇒ A = 0 ∧ B = 0 ;
L05: Block ≫  Begin  ;
L06: Arbitrary ≫  A, B  ;
L07: Premise ≫  A + B′ = 0  ;
L08: S3 ≫  0 ≠ (A + B)′  ;
L09: Prop3.2b′ ≫  (A + B)′ = 0 ⇒ 0 = (A + B)′ ;
L10: Lem1.11e ≫  ((A + B)′ = 0 ⇒ 0 = (A + ; B)′) ⇒ 0 ≠ (A + B)′ ⇒ (A + ; B)′ ≠ 0  ;
L11: L10 ⊵ L09 ≫  0 ≠ (A + B)′ ⇒ (A + B)′ ≠ 0 ;
L12: L11 ⊵ L08 ≫  (A + B)′ ≠ 0  ;
L13: S6 ≫  (A + B′) = (A + B)′  ;
L14: S1′′ ≫  {A+B′ = (A+B)′ ⇒ A+B′ = \atop 0 ⇒ (A + B)′ = 0  ;}
L15: H3 ⊳ L14 ⊳ L13 ⊳ L12 ≫  A + B′ ≠ 0  ;
L16: Lem1.11c ≫  {A + B′ ≠ 0 ⇒ A + B′ = 0 ⇒ \atop A = 0 ∧ B′ = 0  ;}
L17: L16 ⊵ L15 ≫  A + B′ = 0 ⇒ A = 0 ∧ B′ = 0 ;
L18: L17 ⊵ L07 ≫  A = 0 ∧ B′ = 0  ;
L19: Block ≫  End  ;
L20: Ded ⊳ L19 ≫  A + B′ = 0 ⇒ A = 0 ∧ B′ = 0 ;
L21: Block ≫ End ;
L22: Ded ⊳ L21 ≫  {(A+B = 0 ⇒ A = 0∧B = 0) ⇒ \atop A + B′ = 0 ⇒ A = 0 ∧ B′ = 0 □}

[S lemma Prop 3.5d: ΠA, B: A + B = 0 ⇒ A = 0 ∧ B = 0] S proof of Prop 3.5d:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Prop 3.5d_{1} ≫  x + 0 = 0 ⇒ x = 0 ∧ 0 = 0  ;

L04: Prop 3.5d_{2} ≫

(x + y = 0 ⇒ x = 0 ∧ y =
0) ⇒ x + y′ = 0 ⇒ x = 0 ∧
y′ = 0 ;
L05: S9 @ y ⊳ L03 ⊳ L04 ≫  x + y = 0 ⇒ x = 0 ∧ y = 0  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  A + B = 0 ⇒ A = 0 ∧ B = 0  □

6.7 3.5e

[S lemma Prop 3.5e_{1} : ΠA: 0 ≠ 0 ⇒ (A · 0 = 0 ⇒ A = 0)] S proof of Prop 3.5e_{1} :

L01: Arbitrary ≫  A  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A  ;

L04: Premise ≫  0 ≠ 0  ;
L05: Prop 3.2a ≫  0 = 0  ;
L06: Lem1.11c ≫  {¬(0 = 0) ⇒ ((0 = 0) ⇒ (A · \atop 0 = 0 ⇒ A = 0))  ;}
L07: L06 ⊵ L04 ≫  {(0 = 0) ⇒ (A · 0 = 0 ⇒ A = \atop 0)  ;}
L08: L07 ⊵ L05 ≫  A · 0 = 0 ⇒ A = 0  ;
L09: Block ≫  End  ;
L10: Ded ⊳ L09 ≫  0 ≠ 0 ⇒ A · 0 = 0 ⇒ A = 0  □

[S lemma Prop 3.5e_{2} : ΠA, B: (B ≠ 0 ⇒ (A · B = 0 ⇒ A = 0)) ⇒ B′ ≠ 0 ⇒ (A · B′ = 0 ⇒ A = 0)] S proof of Prop 3.5e_{2} :

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  B ≠ 0 ⇒ (A·B = 0 ⇒ A = 0) ;
L05: Block ≫  Begin  ;
L06: Arbitrary ≫  A, B  ;
L07: Premise ≫  B′ ≠ 0  ;
L08: Block ≫  Begin  ;
L09: Arbitrary ≫  A, B  ;
L10: Premise ≫  A · B′ = 0  ;
L11: S8 ≫  A · B′ = A · B + A  ;
L12: S1 ⊳ L11 ⊳ L10 ≫  (A · B) + A = 0  ;
L13: Prop 3.5d ≫  {(A · B) + A = 0 ⇒ (A · B) = \atop 0 ∧ A = 0  ;}
L14: L13 ⊵ L12 ≫  (A · B) = 0 ∧ A = 0  ;
L15: Con2 ⊳ L14 ≫  A = 0  ;
L16: Block ≫  End  ;
L17: Ded ⊳ L16 ≫  A · B′ = 0 ⇒ A = 0  ;
L18: Block ≫  End  ;
L19: Ded ⊳ L18 ≫  {B′ ≠ 0 ⇒ (A · B′ = 0 ⇒ A = \atop 0)  ;}
L20: Block ≫  End  ;
L21: Ded ⊳ L20 ≫  (B ≠ 0 ⇒ (A · B = 0 ⇒ A = ; 0)) ⇒ B′ ≠ 0 ⇒ (A · B′ = 0 ⇒ ; A = 0)  □

[S lemma Prop 3.5e: ΠA, B: B ≠ 0 ⇒ (A · B = 0 ⇒ A = 0)] S proof of Prop 3.5e:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Prop 3.5e_{1} ≫  0 ≠ 0 ⇒ (x · 0 = 0 ⇒ x = 0) ;

L04: Prop 3.5e_{2} ≫ (y ≠ 0 ⇒ (x · y = 0 ⇒ x = 0)) ⇒ y′ ≠ 0 ⇒ (x · y′ = 0 ⇒ x = 0) ;

L05: S9 @ y ⊳ L03 ⊳ L04 ≫  y ≠ 0 ⇒ (x · y = 0 ⇒ x = 0) ;
L06: Block ≫ End ;
L07: Ded ⊳ L06 ≫  B ≠ 0 ⇒ (A · B = 0 ⇒ A = 0) □

6.8 3.5f

[S lemma Prop 3.5f_{1} : ΠA: A + 0 = \overline{1} ⇒ (A = 0 ∧ 0 = \overline{1}) ∨ (A = \overline{1} ∧ 0 = 0)]

S proof of Prop 3.5f_{1} :

L01: Arbitrary ≫  A  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A  ;
L04: Premise ≫  A + 0 = \overline{1}  ;
L05: S5 ≫  A + 0 = A  ;
L06: S1 ⊳ L05 ⊳ L04 ≫  A = \overline{1}  ;
L07: Prop 3.2a ≫  0 = 0  ;
L08: Con ⊳ L06 ⊳ L07 ≫  A = \overline{1} ∧ 0 = 0  ;
L09: Dis2 ⊳ L08 ≫  {(A = 0∧0 = \overline{1})∨(A = \overline{1}∧0 = \atop 0)  ;}
L10: Block ≫  End  ;
L11: Ded ⊳ L10 ≫  {A + 0 = \overline{1} ⇒ (A = 0 ∧ 0 = \atop \overline{1}) ∨ (A = \overline{1} ∧ 0 = 0)  □}

[S lemma Prop 3.5f_{2} : ΠA, B: (A + B = \overline{1} ⇒ ((A = 0 ∧ B = \overline{1}) ∨ (A = \overline{1} ∧ B = 0))) ⇒ (A + B′ = \overline{1} ⇒ ((A = 0 ∧ B′ = \overline{1}) ∨ (A = \overline{1} ∧ B′ = 0)))]

S proof of Prop 3.5f_{2} :

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  {A + B = \overline{1} ⇒ ((A = 0 ∧ B = \atop \overline{1}) ∨ (A = \overline{1} ∧ B = 0))  ;}
L05: Block ≫  Begin  ;
L06: Arbitrary ≫  A, B  ;
L07: Premise ≫  A + B′ = \overline{1}  ;
L08: S6 ≫  A + B′ = (A + B)′  ;
L09: S1 ⊳ L08 ⊳ L07 ≫  (A + B)′ = \overline{1}  ;
L10: S4 ⊳ L09 ≫  A + B = 0  ;
L11: Prop 3.5d ≫  A + B = 0 ⇒ A = 0 ∧ B = 0 ;
L12: L11 ⊵ L10 ≫  A = 0 ∧ B = 0  ;
L13: Con1 ⊳ L12 ≫  A = 0  ;
L14: Con2 ⊳ L12 ≫  B = 0  ;
L15: S2 ⊳ L14 ≫  B′ = \overline{1}  ;
L16: Con ⊳ L13 ⊳ L15 ≫  A = 0 ∧ B′ = \overline{1}  ;

L17: Dis1 ⊳ L16 ≫  {(A = 0 ∧ B′ = \overline{1}) ∨ (A = \overline{1} ∧ \atop B′ = 0)  ;}
L18: Block ≫  End  ;
L19: Ded ⊳ L18 ≫  {A + B′ = \overline{1} ⇒ (A = 0 ∧ B′ = \atop \overline{1}) ∨ (A = \overline{1} ∧ B′ = 0)  ;}
L20: Block ≫  End  ;
L21: Ded ⊳ L20 ≫  (A+B = \overline{1} ⇒ ((A = 0∧B = \overline{1})∨ ; (A = \overline{1} ∧ B = 0))) ⇒ A + B′ = ; \overline{1} ⇒ (A = 0 ∧ B′ = \overline{1}) ∨ (A = ; \overline{1} ∧ B′ = 0)  □

[S lemma Prop 3.5f : ΠA, B: A + B = \overline{1} ⇒ (A = 0 ∧ B = \overline{1}) ∨ (A = \overline{1} ∧ B = 0)] S proof of Prop 3.5f :

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Prop 3.5f_{1} ≫  {x + 0 = \overline{1} ⇒ (x = 0 ∧ 0 = \atop \overline{1}) ∨ (x = \overline{1} ∧ 0 = 0)  ;}

L04: Prop 3.5f_{2} ≫

(x + y = \overline{1} ⇒ ((x = 0 ∧ y =
\overline{1}) ∨ (x = \overline{1} ∧ y = 0))) ⇒ x +
y′ = \overline{1} ⇒ (x = 0 ∧ y′ = \overline{1}) ∨
(x = \overline{1} ∧ y′ = 0) ;
L05: S9 @ y ⊳ L03 ⊳ L04 ≫  {x + y = \overline{1} ⇒ ((x = 0 ∧ y = \atop \overline{1}) ∨ (x = \overline{1} ∧ y = 0))  ;}
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  {A + B = \overline{1} ⇒ (A = 0 ∧ B = \atop \overline{1}) ∨ (A = \overline{1} ∧ B = 0)  □}

6.9 3.5g

[S lemma Prop 3.5g_{1} : ΠA: A · 0 = \overline{1} ⇒ (A = \overline{1}) ∧ (0 = \overline{1})] S proof of Prop 3.5g_{1} :

L01: Arbitrary ≫  A  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A  ;
L04: Premise ≫  A · 0 = \overline{1}  ;
L05: S7 ≫  A · 0 = 0  ;
L06: S1 ⊳ L05 ⊳ L04 ≫  0 = \overline{1}  ;
L07: S3 ≫  0 ≠ \overline{1}  ;
L08: Lem1.11c ≫  {¬(0 = \overline{1}) ⇒ ((0 = \overline{1}) ⇒ (A = \atop \overline{1} ∧ 0 = \overline{1}))  ;}
L09: L08 ⊵ L07 ≫  (0 = \overline{1}) ⇒ (A = \overline{1} ∧ 0 = \overline{1})  ;
L10: L09 ⊵ L06 ≫  (A = \overline{1} ∧ 0 = \overline{1})  ;
L11: Block ≫  End  ;
L12: Ded ⊳ L11 ≫  A · 0 = \overline{1} ⇒ (A = \overline{1} ∧ 0 = \overline{1})  □

[S lemma Prop 3.5g_{2} : ΠA, B: (A · B = 0 ∧ A = \overline{1}) ⇒ (A = \overline{1} ∧ B′ = \overline{1})] S proof of Prop 3.5g_{2} :

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A · B = 0 ∧ A = \overline{1}  ;
L05: Con2 ⊳ L04 ≫  A = \overline{1}  ;
L06: Con1 ⊳ L04 ≫  A · B = 0  ;
L07: S3 ≫  0 ≠ \overline{1}  ;
L08: H10 ⊳ L07 ≫  \overline{1} ≠ 0  ;
L09: S1′′ ≫  A = \overline{1} ⇒ A = 0 ⇒ \overline{1} = 0  ;
L10: H3 ⊳ L09 ⊳ L05 ⊳ L08 ≫  A ≠ 0  ;
L11: Prop 3.2n ≫  A · B = B · A  ;
L12: S1 ⊳ L11 ⊳ L06 ≫  B · A = 0  ;
L13: Prop 3.5e ≫  A ≠ 0 ⇒ B · A = 0 ⇒ B = 0 ;
L14: L13 ⊵ L10 ≫  B · A = 0 ⇒ B = 0  ;
L15: L14 ⊵ L12 ≫  B = 0  ;
L16: S2 ⊳ L15 ≫  B′ = \overline{1}  ;
L17: Con ⊳ L05 ⊳ L16 ≫  A = \overline{1} ∧ B′ = \overline{1}  ;
L18: Block ≫  End  ;
L19: Ded ⊳ L18 ≫  {(A · B = 0 ∧ A = \overline{1}) ⇒ (A = \atop \overline{1} ∧ B′ = \overline{1})  □}

[S lemma Prop 3.5g_{3} : ΠA, B: (A·B = \overline{1} ⇒ (A = \overline{1}∧B = \overline{1})) ⊢ (A·B = \overline{1}∧A = 0) ⇒ (A = \overline{1} ∧ B′ = \overline{1})]

S proof of Prop 3.5g_{3} :

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A · B = \overline{1} ⇒ (A = \overline{1} ∧ B = \overline{1})  ;
L03: Block ≫  Begin  ;
L04: Arbitrary ≫  A, B  ;
L05: Premise ≫  A · B = \overline{1} ∧ A = 0  ;
L06: Con1 ⊳ L05 ≫  A · B = \overline{1}  ;
L07: L02 ⊵ L06 ≫  (A = \overline{1} ∧ B = \overline{1})  ;
L08: Con1 ⊳ L07 ≫  A = \overline{1}  ;
L09: Con2 ⊳ L05 ≫  A = 0  ;
L10: S1 ⊳ L09 ⊳ L08 ≫  0 = \overline{1}  ;
L11: S3 ≫  0 ≠ \overline{1}  ;
L12: Lem1.11c ≫  {0 ≠ \overline{1} ⇒ ((0 = \overline{1}) ⇒ (A = \atop \overline{1} ∧ B′ = \overline{1}))  ;}
L13: L12 ⊵ L11 ≫  (0 = \overline{1}) ⇒ (A = \overline{1} ∧ B′ = \overline{1}) ;
L14: L13 ⊵ L10 ≫  (A = \overline{1} ∧ B′ = \overline{1})  ;
L15: Block ≫  End  ;
L16: Ded ⊳ L15 ≫  {(A · B = \overline{1} ∧ A = 0) ⇒ (A = \atop \overline{1} ∧ B′ = \overline{1})  □}

[S lemma Prop 3.5g_{4} : ΠA, B: (A · B = \overline{1} ⇒ (A = \overline{1} ∧ B = \overline{1})) ⇒ (A · B′ = \overline{1} ⇒ (A = \overline{1} ∧ B′ = \overline{1}))] S proof of Prop 3.5g_{4} :

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A · B = \overline{1} ⇒ (A = \overline{1} ∧ B = \overline{1}) ;
L05: Premise ≫  A · B′ = \overline{1}  ;
L06: S8 ≫  A · B′ = A · B + A  ;
L07: S1 ⊳ L06 ⊳ L05 ≫  A · B + A = \overline{1}  ;
L08: Prop 3.5f ≫  {(A · B + A = \overline{1}) ⇒ (A · B = \atop 0∧A = \overline{1})∨(A·B = \overline{1}∧A = 0) ;}
L09: L08 ⊵ L07 ≫  {(A · B = 0 ∧ A = \overline{1}) ∨ (A · B = \atop \overline{1} ∧ A = 0)  ;}
L10: Prop 3.5g_{2} ≫  {(A · B = 0 ∧ A = \overline{1}) ⇒ (A = \atop \overline{1} ∧ B′ = \overline{1})  ;}
L11: Prop 3.5g_{3} ⊳ L04 ≫  {(A · B = \overline{1} ∧ A = 0) ⇒ (A = \atop \overline{1} ∧ B′ = \overline{1})  ;}
L12: H11 ⊳ L09 ⊳ L10 ⊳ L11 ≫  A = \overline{1} ∧ B′ = \overline{1}  ;
L13: Block ≫  End  ;
L14: Ded ⊳ L13 ≫  (A · B = \overline{1} ⇒ (A = \overline{1} ∧ B = ; \overline{1})) ⇒ A · B′ = \overline{1} ⇒ (A = \overline{1} ∧ ; B′ = \overline{1})  □

[S lemma Prop 3.5g: ΠA, B: A · B = \overline{1} ⇒ (A = \overline{1} ∧ B = \overline{1})] S proof of Prop 3.5g:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Prop 3.5g_{1} ≫  x · 0 = \overline{1} ⇒ (x = \overline{1} ∧ 0 = \overline{1}) ;

L04: Prop 3.5g_{4} ≫

(x · y = \overline{1} ⇒ (x = \overline{1} ∧ y =
\overline{1})) ⇒ (x · y′ = \overline{1} ⇒ (x =
\overline{1} ∧ y′ = \overline{1})) ;
L05: S9 @ y ⊳ L03 ⊳ L04 ≫  x · y = \overline{1} ⇒ (x = \overline{1} ∧ y = \overline{1}) ;
L06: Block ≫ End ;
L07: Ded ⊳ L06 ≫  A · B = \overline{1} ⇒ (A = \overline{1} ∧ B = \overline{1}) □

6.10 3.5h

[S lemma Prop 3.5h: ΠA: A ≠ 0 ⇒ ∃B: A = 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 x < y

Vi har makrodefineret følgende definitioner:

[x < y ¨= ∃z: (z ≠ 0 ∧ z + x = y)] [x ≤ y ¨= x < y ∨ x = y] [x > y ¨= y < x] [x ≥ y ¨= y ≤ x] [x ≮ y ¨= ¬(x < y)] [x ≯ y ¨= y ≮ x] [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 [S lemma Lem1.11c: ΠA, B: ¬A ⇒ (A ⇒ B)] [S lemma Cor1.10a: ΠA, B, C: (A ⇒ B) ⊢ (B ⇒ C) ⊢ A ⇒ C] [S lemma Cor1.10b: ΠA, B, C: A ⇒ (B ⇒ C) ⊢ B ⊢ A ⇒ C] [S lemma Lem1.11a: ΠA: ¬¬A ⇒ A] [S lemma Lem1.11b: ΠA: A ⇒ ¬¬A] [S lemma Prop3.2c′: ΠA, B, C: A = B ⇒ B = C ⇒ A = C] [S lemma S1′′: ΠA, B, C: A = B ⇒ A = C ⇒ B = C] [S lemma Neg′: ΠA, B: (¬B ⇒ ¬A) ⇒ (¬B ⇒ A) ⇒ B] [S lemma Repetition′: ΠA: A ⇒ A] [S lemma Lem1.11e: ΠA, B: (A ⇒ B) ⇒ (¬B ⇒ ¬A)] [S lemma Lem1.11d: ΠA, B: (¬B ⇒ ¬A) ⇒ (A ⇒ B)] [S lemma Prop3.2b′: ΠA, B: A = B ⇒ B = A] [S lemma H10: ΠA, B: B ≠ A ⊢ A ≠ B] [S lemma H11: ΠA, B, C: A ∨ B ⊢ A ⇒ C ⊢ B ⇒ C ⊢ C] [S lemma Lem1.11g: ΠA, B: (A ⇒ B) ⊢ (¬A ⇒ B) ⊢ B] [S lemma MT: ΠA, B: (A ⇒ B) ⊢ ¬B ⊢ ¬A] [S lemma Lem1.11c: ΠA, B: ¬A ⇒ (A ⇒ B)] S proof of Lem1.11c:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  ¬A  ;
L05: Block ≫  Begin  ;
L06: Arbitrary ≫  A, B  ;
L07: Premise ≫  A  ;
L08: Repetition ⊳ L04 ≫  ¬A  ;
L09: A1′ ≫  A ⇒ (¬B ⇒ A)  ;
L10: L09 ⊵ L07 ≫  ¬B ⇒ A  ;
L11: A1′ ≫  ¬A ⇒ (¬B ⇒ ¬A)  ;
L12: L11 ⊵ L08 ≫  ¬B ⇒ ¬A  ;
L13: Neg ⊳ L12 ⊳ L10 ≫  B  ;
L14: Block ≫  End  ;
L15: Ded ⊳ L14 ≫  A ⇒ B  ;
L16: Block ≫  End  ;
L17: Ded ⊳ L16 ≫  ¬A ⇒ (A ⇒ B)  □

[S lemma Cor1.10a: ΠA, B, C: (A ⇒ B) ⊢ (B ⇒ C) ⊢ A ⇒ C] S proof of Cor1.10a:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A ⇒ B  ;
L03: Premise ≫  B ⇒ C  ;
L04: Block ≫  Begin  ;
L05: Arbitrary ≫  A, B, C  ;
L06: Premise ≫  A ⇒ B  ;
L07: Premise ≫  B ⇒ C  ;
L08: Premise ≫  A  ;
L09: L06 ⊵ L08 ≫  B  ;
L10: L07 ⊵ L09 ≫  C  ;
L11: Block ≫  End  ;
L12: Ded ⊳ L11 ≫  (A ⇒ B) ⇒ (B ⇒ C) ⇒ A ⇒ C ;
L13: L12 ⊵ L02 ≫  (B ⇒ C) ⇒ A ⇒ C  ;
L14: L13 ⊵ L03 ≫  A ⇒ C  □

[S lemma Cor1.10b: ΠA, B, C: A ⇒ (B ⇒ C) ⊢ B ⊢ A ⇒ C] S proof of Cor1.10b:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A ⇒ B ⇒ C  ;
L03: Premise ≫  B  ;
L04: A2′ ≫  {(A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ \atop A ⇒ C  ;}
L05: L04 ⊵ L02 ≫  (A ⇒ B) ⇒ A ⇒ C  ;
L06: A1′ ≫  B ⇒ A ⇒ B  ;
L07: L06 ⊵ L03 ≫  A ⇒ B  ;
L08: L05 ⊵ L07 ≫  A ⇒ C  □

[S lemma Lem1.11a: ΠA: ¬¬A ⇒ A] S proof of Lem1.11a:

L01: Arbitrary ≫  A  ;
L02: Neg′ ≫  {(¬(A) ⇒ ¬(¬A)) ⇒ ((¬(A) ⇒ \atop (¬A)) ⇒ A)  ;}
L03: Repetition′ ≫  ¬A ⇒ ¬A  ;
L04: Cor1.10b ⊳ L02 ⊳ L03 ≫  (¬A ⇒ ¬(¬A)) ⇒ A  ;
L05: A1′ ≫  ¬(¬A) ⇒ (¬A ⇒ ¬(¬A))  ;
L06: Cor1.10a ⊳ L05 ⊳ L04 ≫  ¬¬A ⇒ A  □

[S lemma Lem1.11b: ΠA: A ⇒ ¬¬A] S proof of Lem1.11b:

L01: Arbitrary ≫  A  ;
L02: Neg′ ≫  {(¬¬¬A ⇒ ¬A) ⇒ ((¬¬¬A ⇒ \atop A) ⇒ ¬¬A)  ;}

L03: Lem1.11a ≫  ¬¬(¬A) ⇒ (¬A)  ;
L04: L02 ⊵ L03 ≫  (¬¬¬A ⇒ A) ⇒ ¬¬A  ;
L05: A1′ ≫  A ⇒ (¬¬¬A ⇒ A)  ;
L06: Cor1.10a ⊳ L05 ⊳ L04 ≫  A ⇒ ¬¬A  □

[S lemma Prop3.2c′: ΠA, B, C: A = B ⇒ B = C ⇒ A = C] S proof of Prop3.2c′:

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B, C  ;
L04: Premise ≫  A = B  ;
L05: Block ≫  Begin  ;
L06: Arbitrary ≫  A, B, C  ;
L07: Premise ≫  B = C  ;
L08: Prop 3.2c ⊳ L04 ⊳ L07 ≫  A = C  ;
L09: Block ≫  End  ;
L10: Ded ⊳ L09 ≫  B = C ⇒ A = C  ;
L11: Block ≫  End  ;
L12: Ded ⊳ L11 ≫  A = B ⇒ B = C ⇒ A = C  □

[S lemma S1′′: ΠA, B, C: A = B ⇒ A = C ⇒ B = C] S proof of S1′′:

L01: Arbitrary ≫  A, B, C  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B, C  ;
L04: Premise ≫  A = B  ;
L05: Block ≫  Begin  ;
L06: Arbitrary ≫  A, B, C  ;
L07: Premise ≫  A = C  ;
L08: S1 ⊳ L04 ⊳ L07 ≫  B = C  ;
L09: Block ≫  End  ;
L10: Ded ⊳ L09 ≫  A = C ⇒ B = C  ;
L11: Block ≫  End  ;
L12: Ded ⊳ L11 ≫  A = B ⇒ A = C ⇒ B = C  □

[S lemma Neg′: ΠA, B: (¬B ⇒ ¬A) ⇒ (¬B ⇒ A) ⇒ B] S proof of Neg′:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  ¬B ⇒ ¬A  ;
L05: Block ≫  Begin  ;
L06: Arbitrary ≫  A, B  ;
L07: Premise ≫  ¬B ⇒ A  ;
L08: Neg ⊳ L04 ⊳ L07 ≫  B  ;

L09: Block ≫  End  ;
L10: Ded ⊳ L09 ≫  (¬B ⇒ A) ⇒ B  ;
L11: Block ≫  End  ;
L12: Ded ⊳ L11 ≫  (¬B ⇒ ¬A) ⇒ (¬B ⇒ A) ⇒ B □

[S lemma Repetition′: ΠA: A ⇒ A] S proof of Repetition′:

L01: Arbitrary ≫  A  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A  ;
L04: Premise ≫  A  ;
L05: Repetition ⊳ L04 ≫  A  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  A ⇒ A  □

[S lemma H10: ΠA, B: B ≠ A ⊢ A ≠ B] S proof of H10:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  B ≠ A  ;
L03: Prop3.2b′ ≫  A = B ⇒ B = A  ;
L04: Lem1.11e ≫  {(A = B ⇒ B = A) ⇒ B ≠ A ⇒ \atop A ≠ B  ;}
L05: L04 ⊵ L03 ≫  B ≠ A ⇒ A ≠ B  ;
L06: L05 ⊵ L02 ≫  A ≠ B  □

[S lemma MT: ΠA, B: (A ⇒ B) ⊢ ¬B ⊢ ¬A] S proof of MT:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ⇒ B  ;
L03: Premise ≫  ¬B  ;
L04: Lem1.11a ≫  ¬¬A ⇒ A  ;
L05: Cor1.10a ⊳ L04 ⊳ L02 ≫  ¬¬A ⇒ B  ;
L06: Block ≫  Begin  ;
L07: Arbitrary ≫  A, B  ;
L08: Premise ≫  ¬¬A ⇒ B  ;
L09: Premise ≫  ¬B  ;
L10: A1′ ≫  ¬B ⇒ ¬¬A ⇒ ¬B  ;
L11: L10 ⊵ L09 ≫  ¬¬A ⇒ ¬B  ;
L12: Neg ⊳ L11 ⊳ L08 ≫  ¬A  ;
L13: Block ≫  End  ;
L14: Ded ⊳ L13 ≫  (¬¬A ⇒ B) ⇒ ¬B ⇒ ¬A  ;
L15: L14 ⊵ L05 ≫  ¬B ⇒ ¬A  ;
L16: L15 ⊵ L03 ≫  ¬A  □

[S lemma Lem1.11e: ΠA, B: (A ⇒ B) ⇒ (¬B ⇒ ¬A)] S proof of Lem1.11e:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A ⇒ B  ;
L05: Lem1.11a ≫  ¬¬A ⇒ A  ;
L06: Cor1.10a ⊳ L05 ⊳ L04 ≫  ¬¬A ⇒ B  ;
L07: Lem1.11b ≫  B ⇒ ¬¬B  ;
L08: Cor1.10a ⊳ L06 ⊳ L07 ≫  ¬¬A ⇒ ¬¬B  ;
L09: Lem1.11d ≫  (¬¬A ⇒ ¬¬B) ⇒ ¬B ⇒ ¬A ;
L10: L09 ⊵ L08 ≫  ¬B ⇒ ¬A  ;
L11: Block ≫  End  ;
L12: Ded ⊳ L11 ≫  (A ⇒ B) ⇒ ¬B ⇒ ¬A  □

[S lemma Lem1.11d: ΠA, B: (¬B ⇒ ¬A) ⇒ (A ⇒ B)] S proof of Lem1.11d:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  ¬B ⇒ ¬A  ;
L05: Neg′ ≫  {(¬B ⇒ ¬A) ⇒ ((¬B ⇒ \atop A) ⇒ B)  ;}
L06: A1′ ≫  A ⇒ (¬B ⇒ A)  ;
L07: L05 ⊵ L04 ≫  (¬B ⇒ A) ⇒ B  ;
L08: Cor1.10a ⊳ L06 ⊳ L07 ≫  A ⇒ B  ;
L09: Block ≫  End  ;
L10: Ded ⊳ L09 ≫  (¬B ⇒ ¬A) ⇒ (A ⇒ B)  □

[S lemma Prop3.2b′: ΠA, B: A = B ⇒ B = A] S proof of Prop3.2b′:

L01: Arbitrary ≫  A, B  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B  ;
L04: Premise ≫  A = B  ;
L05: Prop 3.2b ⊳ L04 ≫  B = A  ;
L06: Block ≫  End  ;
L07: Ded ⊳ L06 ≫  A = B ⇒ B = A  □

[S lemma Lem1.11g: ΠA, B: (A ⇒ B) ⊢ (¬A ⇒ B) ⊢ B] S proof of Lem1.11g:

L01: Arbitrary ≫  A, B  ;
L02: Premise ≫  A ⇒ B  ;
L03: Premise ≫  ¬A ⇒ B  ;
L04: Lem1.11e ≫  (A ⇒ B) ⇒ ¬B ⇒ ¬A  ;
L05: L04 ⊵ L02 ≫  ¬B ⇒ ¬A  ;

L06: Lem1.11e ≫  (¬A ⇒ B) ⇒ ¬B ⇒ ¬¬A  ;
L07: L06 ⊵ L03 ≫  ¬B ⇒ ¬¬A  ;
L08: Neg ⊳ L07 ⊳ L05 ≫  B  □

[S lemma H11: ΠA, B, C: A ∨ B ⊢ A ⇒ C ⊢ B ⇒ C ⊢ C]

S proof of H11:

L01: Arbitrary ≫  A, B, C  ;
L02: Premise ≫  A ∨ B  ;
L03: Premise ≫  A ⇒ C  ;
L04: Premise ≫  B ⇒ C  ;
L05: Cor1.10a ⊳ L02 ⊳ L04 ≫  ¬A ⇒ C  ;
L06: Lem1.11g ⊳ L03 ⊳ L05 ≫  C  □

Litteratur

[Gru06] K. Grue.  A logiweb base page.  Technical report, Lo-

        giweb, 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.