projekt i logik

Maja Hanne Tønnesen, Rune Christoffer Kildetoft Andresen

& Niels Peter Meyn Milthers 26. juni 2006

Indhold

1 Introduction 1 2 Proof of Prop 3.2 2 3 Proof of Prop 3.4 7 4 Numerals 11 5 Lemma Prop 3.7 12

5.1 Definitions of x < y . . . . . . . . . . . . . . . . . . . . . . . . . 12 5.2 proof of Prop 3.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

6 Lemma Prop 3.10 13 7 Lemma Prop 3.11 14 A Helping lemmas 14

Resumé

1 Introduction

In this paper we will prove the propositions regarding S starting with proposition Prop 3.2i in mendelson [Men97]. Continuing toProp 3.4 defining numerals neded to prove Prop 3.5 . then we will define rules regarding x < y needed to prove Prop 3.7 . after that we will define x | y nedded to prove Prop 3.10 , and finally we will prove Prop 3.11.

2 Proof of Prop 3.2

A modified version of Mendelsons system S (Peano arithmetic) [Men97] may be formulated thus: [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 Neg: ΠA: ΠB: ¬B ⇒ ¬A ⊢ ¬B ⇒ A ⊢ B] [S rule S1: ΠA, B, C: A = B ⊢ A = C ⊢ B = C] [S rule S9: ΠX , A, B, C: ⟨B≡A|X:=0⟩ ⊢⊢ ⟨C≡A|X:=X′⟩ ⊢⊢ B ⊢ A ⇒ C ⊢ A]

Mendelson [Men97] defines a set of lemma’s [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]

These Lemma’s are proved in [Gru06], and we will continue to prove the following lemma’s, from Mendelson [Men97]. [S lemma Prop 3.2i: ΠA, B, C: A = B ⊢ C + A = C + B] [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] 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  □

[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 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)  □

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

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

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

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

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  □

And thus we hve proved Prop 3.2.

3 Proof of Prop 3.4

in this section we will prove Prop 3.4 from [Men97] [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] [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 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  □

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  □

[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 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)  □

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

4 Numerals

We will for the remainder of the project need to construct some numerals, the numerals are the names for 0, 0′, 0′′ … we will define them as folows \overline{0}, \overline{1}, \overline{2} …

With these definitions we will now continue to prove Prop 3.5 that states different things about numerals. [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: A ≠ 0 ⇒ (B · A = 0 ⇒ B = 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′′] 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′  □

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  □

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  □

[S lemma Prop 3.5d_{1} : ΠA: A + 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]

5 Lemma Prop 3.7

5.1 Definitions of x < y

in the folowing we need some definitions, we will macro define them as: [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] with these definitions, we will continue to prove the following statements:

[S lemma Prop 3.7a: ΠA: A ≮ A]

[S lemma Prop 3.7b: ΠA, B, C: A < B ⇒ B < C ⇒ A < C]

[S lemma Prop 3.7c: ΠA, B: A < B ⇒ B ≮ A]

[S lemma Prop 3.7d: ΠA, B, C: A < B ⇒ A + C < B + C]

[S lemma Prop 3.7e: ΠA: A ≤ A]

[S lemma Prop 3.7f : ΠA, B, C: A ≤ B ⇒ B ≤ C ⇒ A ≤ C]

[S lemma Prop 3.7g: ΠA, B, C: A ≤ B ⇒ A + C ≤ B + C]

[S lemma Prop 3.7g′: ΠA, B, C: A + C ≤ B + C ⇒ A ≤ B] [S lemma Prop 3.7h: ΠA, B, C: A ≤ B ⇒ B < C ⇒ A < C] [S lemma Prop 3.7i: ΠA: 0 ≤ A] [S lemma Prop 3.7j: ΠA: 0 < A′] [S lemma Prop 3.7k: ΠA, B: A < B ⇒ A′ ≤ B] [S lemma Prop 3.7k′: ΠA, B: A′ ≤ B ⇒ A < B] [S lemma Prop 3.7l: ΠA, B: A ≤ B ⇒ A < B′] [S lemma Prop 3.7l′: ΠA, B: A < B′ ⇒ A ≤ B] [S lemma Prop 3.7m: ΠA: A < A′] [S lemma Prop 3.7o: ΠA, B: A ≠ B ⇒ (A < B ∨ B < A)] [S lemma Prop 3.7p: ΠA, B: A = B ∨ A < B ∨ B < A] [S lemma Prop 3.7q: ΠA, B: A ≤ B ∨ B ≤ A] [S lemma Prop 3.7r: ΠA, B: A + B ≥ A] [S lemma Prop 3.7s: ΠA, B: B ≠ 0 ⇒ A + B > A] [S lemma Prop 3.7t: ΠA, B: B ≠ 0 ⇒ A · B ≥ A] [S lemma Prop 3.7u: ΠA: A ≠ 0 ⇒ A > 0] [S lemma Prop 3.7u′: ΠA: A > 0 ⇒ A ≠ 0] [S lemma Prop 3.7v: ΠA, B: A > 0 ⇒ B > 0 ⇒ A · B > 0] [S lemma Prop 3.7w: ΠA, B: A ≠ 0 ⇒ B > \overline{1} ⇒ B · A > A] [S lemma Prop 3.7x: ΠA, B, C: A ≠ 0 ⇒ B < C ⇒ B · A < C · A] [S lemma Prop 3.7x′: ΠA, B, C: A ≠ 0 ⇒ B · A < C · A ⇒ B < C] [S lemma Prop 3.7y: ΠA, B, C: A ≠ 0 ⇒ B ≤ C ⇒ B · A ≤ C · A] [S lemma Prop 3.7y′: ΠA, B, C: A ≠ 0 ⇒ B · A ≤ C · A ⇒ B ≤ C] [S lemma Prop 3.7z: ΠA: A ≮ 0] [S lemma Prop 3.7z′: ΠA, B: A ≤ B ∧ B ≤ A ⇒ A = B]

5.2 proof of Prop 3.7

6 Lemma Prop 3.10

[S lemma Prop 3.10a: ΠA: A | A] [S lemma Prop 3.10b: ΠA: \overline{1} | A] [S lemma Prop 3.10c: ΠA: A | 0] [S lemma Prop 3.10d: ΠA, B, C: A | B ∧ B | C ⇒ A | C] [S lemma Prop 3.10e: ΠA, B: A ≠ 0 ∧ B | B ⇒ A ≤ A] [S lemma Prop 3.10f : ΠA, B: A | B ∧ B | A ⇒ A = B] [S lemma Prop 3.10g: ΠA, B, C: A | B ⇒ A | (B · C)] [S lemma Prop 3.10h: ΠA, B, C: A | B ∧ A | C ⇒ A | (B + C)]

7 Lemma Prop 3.11

[S lemma Prop 3.11: ΠA, B: A ≠ 0 ⇒ ∃C, D: (B = A · C + D ∧ D < A ∧ ∀E, F: ((B = A · E + F ∧ F < A) ⇒ C = E ∧ D = F))]

A Helping lemmas

for some of our proofs we need to prove some lemmas concerning ∧ and ∨ these will be proved here. [S lemma T0: ΠA, B: B ⇒ (A ⇒ B)] [S lemma T1: ΠA, B: ¬A ⇒ (A ⇒ B)] [S lemma H0a: ΠA, B, C: (A ⇒ B) ⊢ (B ⇒ C) ⊢ A ⇒ C] [S lemma H0b: ΠA, B, C: A ⇒ (B ⇒ C) ⊢ B ⊢ A ⇒ C] [S lemma H1: ΠA: ¬¬A ⇒ A] [S lemma H2: ΠA: A ⇒ ¬¬A] [S lemma Con1: ΠA, B: A ∧ B ⊢ A] [S lemma Con2: ΠA, B: A ∧ B ⊢ B] [S lemma Con: ΠA, B: A ⊢ B ⊢ A ∧ B] [S lemma Dis1: ΠA, B: A ⊢ A ∨ B] [S lemma Dis2: ΠA, B: B ⊢ A ∨ B] S proof of T0:

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

L04: Premise ≫  B  ;
L05: Block ≫  Begin  ;
L06: Arbitrary ≫  A, B  ;
L07: Premise ≫  A  ;
L08: Repetition ⊳ L04 ≫  B  ;
L09: Block ≫  End  ;
L10: Ded ⊳ L09 ≫  A ⇒ B  ;
L11: Block ≫  End  ;
L12: Ded ⊳ L11 ≫  B ⇒ (A ⇒ B)  □

S proof of T1:

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: T0 ≫  A ⇒ (¬B ⇒ A)  ;
L10: L09 ⊵ L07 ≫  ¬B ⇒ A  ;
L11: T0 ≫  ¬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 proof of H0a:

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 proof of H0b:

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: T0 ≫  B ⇒ A ⇒ B  ;
L07: L06 ⊵ L03 ≫  A ⇒ B  ;
L08: L05 ⊵ L07 ≫  A ⇒ C  □

S proof of H1:

L01: Arbitrary ≫  A  ;
L02: Neg ≫  {(¬A ⇒ ¬(¬A)) ⇒ ((¬A ⇒ \atop (¬A)) ⇒ A)  ;}
L03: Repetition ≫  ¬A ⇒ ¬A  ;
L04: H0b ⊳ L02 ⊳ L03 ≫  (¬A ⇒ ¬(¬A)) ⇒ A  ;
L05: A1′ ≫  ¬(¬A) ⇒ (¬A ⇒ ¬(¬A))  ;
L06: H0a ⊳ L05 ⊳ L04 ≫  ¬(¬A) ⇒ A  □

S proof of H2:

L01: Arbitrary ≫  A  ;
L02: Neg ≫  {(¬¬¬A ⇒ ¬A) ⇒ ((¬¬¬A ⇒ \atop A) ⇒ ¬¬A)  ;}
L03: H1 ≫  ¬¬¬A ⇒ ¬A  ;
L04: L02 ⊵ L03 ≫  (¬¬¬A ⇒ A) ⇒ ¬¬A  ;
L05: A1′ ≫  A ⇒ (¬¬¬A ⇒ A)  ;
L06: H1 ⊳ L04 ⊳ L05 ≫  A ⇒ ¬¬A  □

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.