¡¡¡¡¡¡¡ opgave.pyk ======= ¿¿¿¿¿¿¿ 1.6 1

projekt i logik

Maja Hanne Tønnesen, Rune Kildetoft Andresen & Niels Peter Meyn Milthers 21. juni 2006

Indhold

1 Introduction 2

2  2

Resumé

1 Introduction

In this paper we will prove the propositions regarding S starting with proposition Prop 3.2i. continuing to 3.4, bevise 3.5, aksiomer, der definerer x—y, bevise 3.10, og bevise 3.11.

We chose to prove chapter 3 from mendelson, starting with Lemma 3.2, since the first ten wfs’ are proved in Mendelson, we will start with Lemma 3.2.i.

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

we will start by doing Prop 3.2i [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: Prop 3.2e ≫  A = B ⇒ A + C = B + C  ;
L05: Prop 3.2h ≫  A + C = C + A  ;
L06: Prop 3.2h ≫  B + C = C + B  ;
L07: Premise ≫  A = B  ;
L08: MP ⊳ L04 ⊳ L07 ≫  A + C = B + C  ;
L09: S1 ≫  {A + C = B + C ⇒ (A + C = \atop C + A ⇒ B + C = C + A)  ;}
L10: MP ⊳ L09 ⊳ L08 ≫  A+C = C+A ⇒ B+C = C+A ;
L08: MP ⊳ L10 ⊳ L05 ≫  B + C = C + A  ;
L11: Prop 3.2b ⊳ L08 ≫  C + A = B + C  ;

L12: Prop 3.2e ≫  {C + A = B + C ⇒ (B + C = \atop C + B ⇒ C + A = C + B)  ;}
L13: MP ⊳ L12 ⊳ L11 ≫  B+C = C+B ⇒ C+A = C+B ;
L14: MP ⊳ L13 ⊳ L06 ≫  C + A = C + B  ;
L15: Block ≫  End  ;
L16: Ded ⊳ L15 ≫  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: S7 ≫  A · 0 = 0  ;
L03: S7 ≫  B · 0 = 0  ;
L04: Prop 3.2a ≫  0 = 0  ;
L05: Prop 3.2b ⊳ L03 ≫  0 = B · 0  ;
L06: Prop 3.2c ≫  {A · 0 = 0 ⇒ 0 = B · 0 ⇒ A · 0 = \atop B · 0  ;}
L07: L06 ⊳ L02 ⊳ L05 ≫  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 ≫  {A · C = B · C ⇒ A · C + A = \atop B · C + A  ;}
L10: L09 ⊳ L06 ≫  A · C + A = B · C + A  ;
L11: Prop 3.2i ≫  A = B ⇒ B ·C +A = B ·C +B ;
L12: L11 ⊳ L06 ≫  B · C + A = B · C + B  ;
L13: Prop 3.2c ≫  A·C +A = B ·C +A ⇒ B ·C + ; A = B · C + B ⇒ A · C + A = ; B · C + B  ;
L14: L13 ⊳ L10 ⊳ L12 ≫  A · C + A = B · C + B  ;
L15: L14 ⊳ L07 ⊳ L08 ≫  A · C′ = B · C′  ;
L12: Block ≫  End  ;
L16: Ded ⊳ L12 ≫  {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: Block ≫  Begin  ;
L03: Prop 3.2k_{1} ≫  x = y ⇒ x · 0 = y · 0  ;

L04: Prop 3.2k_{2} ≫

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

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

L01: S7 ≫  0 · 0 = 0  □

[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 ⊳ L06 ⊳ L05 ≫  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: Prop 3.2l_{1} ≫  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 = T · 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 ≫  0 = A · 0  ;
L05: Prop 3.2e ≫  0 = A · 0 ⇒ 0 + 0 = A · 0 + 0  ;
L06: L05 ⊳ L04 ≫  0 + 0 = A · 0 + 0  ;
L07: Prop 3.2c ≫  {0 = 0 + 0 ⇒ 0 + 0 = A · 0 + 0 ⇒ \atop 0 = A · 0 + 0  ;}
L08: L07 ⊳ L03 ⊳ L06 ≫  0 = A · 0 + 0  ;
L09: Prop 3.2c ≫  {A′ · 0 = 0 ⇒ 0 = A · 0 + 0 ⇒ \atop A′ · 0 = A · 0 + 0  ;}
L10: L09 ⊳ L02 ⊳ L09 ≫  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 ≫  {A′ · B = A · B + B ⇒ A′ · B + \atop A′ = A · B + B + A′  ;}

L07: L06 ⊳ L04 ≫  A′ · B + A′ = A · B + B + A′ ;
L08: S6 ≫  B + A′ = (B + A)′  ;
L09: Prop 3.2g ≫  B′ + A = (B + A)′  ;
L10: Prop 3.2d ⊳ L08 ⊳ L09 ≫  B + A′ = B′ + A  ;
L11: Prop 3.2h ≫  B′ + A = A + B′  ;
L12: Prop 3.2c ⊳ L10 ⊳ L11 ≫  B + A′ = A + B′  ;
L13: Prop 3.2i ⊳ L12 ≫  A·B +B +A′ = A·B +A+B′ ;
L14: S8 ≫ A · B′ = A · B + A ;
L15: Prop 3.2e ⊳ L14 ≫  A · B′ + B′ = A · B + A + B′ ;
L16: Prop 3.2d ⊳ L15 ⊳ L13 ≫  A · B + B + A′ = A · B′ + B′ ;
L17: Prop 3.2c ⊳ L07 ⊳ L16 ≫  A′ · B + A′ = A · B′ + B′  ;
L18: Prop 3.2c ⊳ L05 ⊳ L17 ≫  A′ · B′ = A · B′ + B′  ;
L19: Block ≫  End  ;
L20: Ded ⊳ L19 ≫  {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.2c ⊳ 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.2b ⊳ Prop 3.2m ≫  B · A + A = B′ · A  ;
L08: Prop 3.2c ⊳ L08 ⊳ L07 ≫  A · B + A = B′ · A  ;
L09: Prop 3.2c ⊳ L05 ⊳ L08 ≫  A · B′ = B′ · A  ;
L10: Block ≫  End  ;
L11: Ded ⊳ L10 ≫  A · B = B · A ⇒ A · B′ = B′ · S □

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: Block ≫  Begin  ;
L03: Arbitrary ≫  A, B, C  ;
L04: Premise ≫  A = B  ;
L05: Prop 3.2k ≫  A = B ⇒ A · C = B · C  ;
L06: L05 ⊳ L04 ≫  A · C = B · C  ;
L07: Prop 3.2n ≫  A · C = C · A  ;
L08: Prop 3.2n ≫  B · C = C · B  ;
L09: Prop 3.2c ≫  {A·C = B ·C ⇒ B ·C = C ·B ⇒ \atop A · C = C · B  ;}
L10: L09 ⊳ L06 ⊳ L08 ≫  A · C = C · B  ;
L11: S1 ≫  {A·C = C ·B ⇒ A·C = C ·A ⇒ \atop C · A = C · B  ;}
L12: L11 ⊳ L10 ⊳ L07 ≫  C · A = C · B  ;
L13: Block ≫  End  ;
L14: Ded ⊳ L13 ≫  A = B ⇒ C · A = C · B  □

[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 · B)] [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]

Litteratur

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