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:

[S →^{stmt} Π\underline{a}: \underline{a} + 0 = \underline{a} ⊕ Π\underline{a}, \underline{b}: \underline{a} ⇒ \underline{b} ⊢ \underline{a} ⊢ \underline{b} ⊕ Π\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{b} ⊢ \underline{b} = \underline{a} ⊕ Π\underline{a}: \underline{a} = 0 + \underline{a} ⊕ Π\underline{x}, \underline{a}, \underline{b}, \underline{c}: ⟨\underline{b}≡\underline{a}|\underline{x}:=0⟩ ⊢⊢ ⟨\underline{c}≡\underline{a}|\underline{x}:=\underline{x}′⟩ ⊢⊢ \underline{b} ⊢ \underline{a} ⇒ \underline{c} ⊢ \underline{a} ⊕ Π\underline{a}: ¬0 = \underline{a}′ ⊕ Π\underline{a}, \underline{b}, \underline{c}: \underline{a} = \underline{c} ⊢ \underline{b} = \underline{c} ⊢ \underline{a} = \underline{b} ⊕ Π\underline{a}, \underline{b}: \underline{a} + \underline{b} = \underline{b} + \underline{a} ⊕ Π\underline{a}: \underline{a} · 0 = 0 ⊕ Π\underline{a}, \underline{b}: \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{a}′ + \underline{b} = \underline{a} + \underline{b}′ ⊕ Π\underline{a}, \underline{b}: Ded(\underline{a}, \underline{b}) ⊢⊢ \underline{a} ⊢ \underline{b} ⊕ Π\underline{a}: \underline{a} = \underline{a} ⊕ Π\underline{a}, \underline{b}: \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a} ⊕ Π\underline{a}, \underline{b}: \underline{a} = \underline{b} ⊢ \underline{a}′ = \underline{b}′ ⊕ Π\underline{a}, \underline{b}, \underline{c}: \underline{a} = \underline{b} ⊢ \underline{b} = \underline{c} ⊢ \underline{a} = \underline{c} ⊕ Π\underline{x}, \underline{a}: \underline{a} ⊢ ∀\underline{x}: \underline{a} ⊕ Π\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{b}′ = \underline{a} + \underline{b}′] [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} ⊢ ∀\underline{x}: \underline{a}][Gen →^{proof} Rule tactic] [Ded →^{stmt} S ⊢ Π\underline{a}, \underline{b}: Ded(\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]

[Neg →^{stmt} S ⊢ Π\underline{a}: Π\underline{b}: ¬\underline{b} ⇒ ¬\underline{a} ⊢ ¬\underline{b} ⇒ \underline{a} ⊢ \underline{b}][Neg →^{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] [S9 →^{stmt} S ⊢ Π\underline{x}, \underline{a}, \underline{b},

\underline{c}: ⟨\underline{b}≡\underline{a}|\underline{x}:=0⟩ ⊢⊢ ⟨\underline{c}≡\underline{a}|\underline{x}:=\underline{x}′⟩ ⊢⊢ \underline{b} ⊢ \underline{a} ⇒ \underline{c} ⊢ \underline{a}][S9 →^{proof} Rule tactic]

[Prop 3.2a →^{stmt} S ⊢ Π\underline{a}: \underline{a} = \underline{a}][Prop 3.2a →^{proof} Rule tactic] [Prop 3.2b →^{stmt} S ⊢ Π\underline{a}, \underline{b}: \underline{a} = \underline{b} ⊢ \underline{b} = \underline{a}][Prop 3.2b →^{proof} Rule tactic] [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.2c →^{proof} Rule tactic] [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.2d →^{proof} Rule tactic] [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.2e →^{proof} Rule tactic] [Prop 3.2f →^{stmt} S ⊢ Π\underline{a}: \underline{a} = 0 + \underline{a}][Prop 3.2f →^{proof} Rule tactic] [Prop 3.2g →^{stmt} S ⊢ Π\underline{a}, \underline{b}: \underline{a}′ + \underline{b} = \underline{a} + \underline{b}′][Prop 3.2g →^{proof} Rule tactic] [Prop 3.2h →^{stmt} S ⊢ Π\underline{a}, \underline{b}: \underline{a} + \underline{b} = \underline{b} + \underline{a}][Prop 3.2h →^{proof} Rule tactic] [Prop 3.2i →^{stmt} S ⊢ Π\underline{a}, \underline{b}, \underline{c}: \underline{a} = \underline{b} ⊢ \underline{c} + \underline{a} = \underline{c} + \underline{b}] we will start by doing Prop 3.2i

[Prop 3.2i →^{proof} λc.λx.P(⌈S ⊢

L_{?}:  Arbitrary ≫  \underline{a}, \underline{b}, \underline{c}  ;
L_{?}:  Block ≫  Begin  ;
L_{?}:  Arbitrary ≫  \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};

L_{?}: 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} ;

L_{g}: Block ≫ End ; Ded⊳ L_{g} ≫ \underline{a} = \underline{b} ⊢ \underline{c} + \underline{a} = \underline{c} + \underline{b}⌉, p_{0}, c)]

Litteratur

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