projekt i logik

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

Indhold

1 Introduction 1

2  1

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 rule Prop 3.2a: ΠA: A = A] [S rule Prop 3.2b: ΠA, B: A = B ⊢ B = A] [S rule Prop 3.2c: ΠA, B, C: A = B ⊢ B = C ⊢ A = C] [S rule Prop 3.2d: ΠA, B, C: A = C ⊢ B = C ⊢ A = B] [S rule Prop 3.2e: ΠA, B, C: A = B ⊢ A + C = B + C] [S rule Prop 3.2f: ΠA: A = 0 + A] [S rule Prop 3.2g: ΠA, B: A′ + B = (A + B)′] [S rule Prop 3.2h: ΠA, B: A + B = B + A] [S lemma Prop 3.2i: ΠA, B, C: A = B ⊢ C + A = C + B]

we will start by doing Prop 3.2i 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  □

Litteratur

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