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} x] [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} ⊢ ∀_{obj}\underline{x}: \underline{a}][Gen →^{proof} Rule tactic] [Ded →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: λx.Ded_{0}(⌈\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}⌉≡^{0}⌈\underline{a}⌉|⌈\underline{x}⌉:=⌈0⌉⟩ ⊢⊢ ⟨⌈\underline{c}⌉≡^{0}⌈\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.2b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ \underline{b} = \underline{a}] [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.2d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{c} ⊢ \underline{b} = \underline{c} ⊢ \underline{a} = \underline{b}] [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.2f →^{stmt} S ⊢ ∀\underline{a}: \underline{a} = 0 + \underline{a}] [Prop 3.2g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ + \underline{b} = \underline{a} + \underline{b}′] [Prop 3.2h →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = \underline{b} + \underline{a}] [Prop 3.2i →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{c} + \underline{a} = \underline{c} + \underline{b}] [Prop 3.2j →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c}] [Prop 3.2k →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{a} · \underline{c} = \underline{b} · \underline{c}] [Prop 3.2l →^{stmt} S ⊢ ∀\underline{a}: 0 · \underline{a} = 0] [Prop 3.2m →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b}] [Prop 3.2n →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = \underline{b} · \underline{a}] [Prop 3.2o →^{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 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{c} + \underline{a} = \underline{c} + \underline{b}] [Prop 3.2i →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: 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}; \underline{a} = \underline{b} ⊢ MP ⊳ \underline{a} = \underline{b} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⊳ \underline{a} = \underline{b} ≫ \underline{a} + \underline{c} = \underline{b} + \underline{c}; 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}; MP ⊳ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} + \underline{c} = \underline{c} + \underline{a} ⇒ \underline{b} + \underline{c} = \underline{c} + \underline{a} ⊳ \underline{a} + \underline{c} = \underline{b} + \underline{c} ≫ \underline{a} + \underline{c} = \underline{c} + \underline{a} ⇒ \underline{b} + \underline{c} = \underline{c} + \underline{a}; MP ⊳ \underline{a} + \underline{c} = \underline{c} + \underline{a} ⇒ \underline{b} + \underline{c} = \underline{c} + \underline{a} ⊳ \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}; Prop 3.2e ≫ \underline{c} + \underline{a} = \underline{b} + \underline{c} ⇒ \underline{b} + \underline{c} = \underline{c} + \underline{b} ⇒ \underline{c} + \underline{a} = \underline{c} + \underline{b}; MP ⊳ \underline{c} + \underline{a} = \underline{b} + \underline{c} ⇒ \underline{b} + \underline{c} = \underline{c} + \underline{b} ⇒ \underline{c} + \underline{a} = \underline{c} + \underline{b} ⊳ \underline{c} + \underline{a} = \underline{b} + \underline{c} ≫ \underline{b} + \underline{c} = \underline{c} + \underline{b} ⇒ \underline{c} + \underline{a} = \underline{c} + \underline{b}; MP ⊳ \underline{b} + \underline{c} = \underline{c} + \underline{b} ⇒ \underline{c} + \underline{a} = \underline{c} + \underline{b} ⊳ \underline{b} + \underline{c} = \underline{c} + \underline{b} ≫ \underline{c} + \underline{a} = \underline{c} + \underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{c} + \underline{a} = \underline{c} + \underline{b} ≫ \underline{a} = \underline{b} ⇒ \underline{c} + \underline{a} = \underline{c} + \underline{b}⌉, p_{0}, c)]

[Prop 3.2j_{1} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} + 0 = \underline{a} + \underline{b} + 0]

[Prop 3.2j_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: S5 ≫ \underline{a} + \underline{b} + 0 = \underline{a} + \underline{b}; S5 ≫ \underline{b} + 0 = \underline{b}; Prop 3.2i ⊳ \underline{b} + 0 = \underline{b} ≫ \underline{a} + \underline{b} + 0 = \underline{a} + \underline{b}; Prop 3.2d ⊳ \underline{a} + \underline{b} + 0 = \underline{a} + \underline{b} ⊳ \underline{a} + \underline{b} + 0 = \underline{a} + \underline{b} ≫ \underline{a} + \underline{b} + 0 = \underline{a} + \underline{b} + 0⌉, p_{0}, c)]

[Prop 3.2j_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ⇒ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′]

[Prop 3.2j_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ⊢ S6 ≫ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′; S2 ⊳ \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ≫ \underline{a} + \underline{b} + \underline{c}′ = \underline{a}+\underline{b}+\underline{c}′; Prop 3.2c⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′ ⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′ ≫ \underline{a}+\underline{b}+\underline{c}′ = \underline{a} + \underline{b} + \underline{c}′; S6 ≫ \underline{b} + \underline{c}′ = \underline{b} + \underline{c}′; Prop 3.2i ⊳ \underline{b} + \underline{c}′ = \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{b} + \underline{c}′ = \underline{a}+\underline{b}+\underline{c}′; S6 ≫ \underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′; Prop 3.2c⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′ ≫ \underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′; Prop 3.2d⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a}+\underline{b}+\underline{c}′ ⊳\underline{a}+\underline{b}+\underline{c}′ = \underline{a} + \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ⊢ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′ ≫ \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c} ⇒ \underline{a} + \underline{b} + \underline{c}′ = \underline{a} + \underline{b} + \underline{c}′⌉, p_{0}, c)]

[Prop 3.2j →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: Prop 3.2j_{1} ≫ \overline{x} + \overline{y} + 0 = \overline{x} + \overline{y} + 0; Prop 3.2j_{2} ≫ \overline{x} + \overline{y} + \overline{z} = \overline{x} + \overline{y} + \overline{z} ⇒ \overline{x} + \overline{y} + \overline{z}′ = \overline{x}+\overline{y}+\overline{z}′; S9 @ \overline{z}⊳\overline{x}+\overline{y}+0 = \overline{x}+\overline{y}+0⊳\overline{x}+\overline{y}+\overline{z} = \overline{x}+\overline{y}+\overline{z} ⇒ \overline{x}+\overline{y}+\overline{z}′ = \overline{x}+\overline{y}+\overline{z}′ ≫ \overline{x} + \overline{y} + \overline{z} = \overline{x} + \overline{y} + \overline{z}; Ded ⊳ \overline{x} + \overline{y} + \overline{z} = \overline{x} + \overline{y} + \overline{z} ≫ \underline{a} + \underline{b} + \underline{c} = \underline{a} + \underline{b} + \underline{c}⌉, p_{0}, c)]

[Prop 3.2k_{1} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} = \underline{b} ⊢ \underline{a} · 0 = \underline{b} · 0]

[Prop 3.2k_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: S7 ≫ \underline{a}·0 = 0; S7 ≫ \underline{b}·0 = 0; Prop 3.2a ≫ 0 = 0; Prop 3.2b⊳\underline{b}·0 = 0 ≫ 0 = \underline{b}·0; Prop 3.2c ≫ \underline{a}·0 = 0 ⇒ 0 = \underline{b}·0 ⇒ \underline{a}·0 = \underline{b} · 0; \underline{a} · 0 = 0 ⇒ 0 = \underline{b} · 0 ⇒ \underline{a} · 0 = \underline{b} · 0 ⊳ \underline{a} · 0 = 0 ⊳ 0 = \underline{b} · 0 ≫ \underline{a} · 0 = \underline{b} · 0⌉, p_{0}, c)]

[Prop 3.2k_{2} →^{stmt} S ⊢ ∀\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{c}′ = \underline{b} · \underline{c}′]

[Prop 3.2k_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\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{c} = \underline{b} · \underline{c} ⊳ \underline{a} = \underline{b} ≫ \underline{a} · \underline{c} = \underline{b} · \underline{c}; S8 ≫ \underline{a} · \underline{c}′ = \underline{a} · \underline{c} + \underline{a}; S8 ≫ \underline{b} · \underline{c}′ = \underline{b} · \underline{c} + \underline{b}; Prop 3.2e ≫ \underline{a} · \underline{c} = \underline{b} · \underline{c} ⇒ \underline{a} · \underline{c} + \underline{a} = \underline{b} · \underline{c} + \underline{a}; \underline{a} · \underline{c} = \underline{b} · \underline{c} ⇒ \underline{a} · \underline{c} + \underline{a} = \underline{b}·\underline{c}+\underline{a}⊳\underline{a}·\underline{c} = \underline{b}·\underline{c} ≫ \underline{a}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{a}; Prop 3.2i ≫ \underline{a} = \underline{b} ⇒ \underline{b}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{b}; \underline{a} = \underline{b} ⇒ \underline{b} · \underline{c} + \underline{a} = \underline{b} · \underline{c} + \underline{b} ⊳ \underline{a} · \underline{c} = \underline{b} · \underline{c} ≫ \underline{b} · \underline{c} + \underline{a} = \underline{b} · \underline{c} + \underline{b}; Prop 3.2c ≫ \underline{a} · \underline{c} + \underline{a} = \underline{b}·\underline{c}+\underline{a} ⇒ \underline{b}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{b} ⇒ \underline{a}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{b}; \underline{a}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{a} ⇒ \underline{b}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{b} ⇒ \underline{a}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{b}⊳\underline{a}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{a}⊳\underline{b}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{b} ≫ \underline{a}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{b}; \underline{a}·\underline{c}+\underline{a} = \underline{b}·\underline{c}+\underline{b}⊳\underline{a}·\underline{c}′ = \underline{a}·\underline{c}+\underline{a}⊳\underline{b}·\underline{c}′ = \underline{b}·\underline{c}+\underline{b} ≫ \underline{a}·\underline{c}′ = \underline{b}·\underline{c}′; Ded⊳∀\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{c}′ = \underline{b} · \underline{c}′ ≫ \underline{a} = \underline{b} ⇒ \underline{a} · \underline{c} = \underline{b} · \underline{c} ⊢ \underline{a} = \underline{b} ⇒ \underline{a} · \underline{c}′ = \underline{b} · \underline{c}′⌉, p_{0}, c)]

[Prop 3.2k →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: Prop 3.2k_{1} ≫ \overline{x} = \overline{y} ⇒ \overline{x} · 0 = \overline{y} · 0; Prop 3.2k_{2} ≫ \overline{x} = \overline{y} ⇒ \overline{x} · \overline{z} = \overline{y} · \overline{z} ⇒ \overline{x} = \overline{y} ⇒ \overline{x} · \overline{z}′ = \overline{y} · \overline{z}′; S9 @ \overline{z} ⊳ \overline{x} = \overline{y} ⇒ \overline{x} · 0 = \overline{y} · 0 ⊳ \overline{x} = \overline{y} ⇒ \overline{x} · \overline{z} = \overline{y} · \overline{z} ⇒ \overline{x} = \overline{y} ⇒ \overline{x} · \overline{z}′ = \overline{y} · \overline{z}′ ≫ \overline{x} = \overline{y} ⇒ \overline{x} · \overline{z} = \overline{y} · \overline{z}; Ded ⊳ \overline{x} = \overline{y} ⇒ \overline{x} · \overline{z} = \overline{y} · \overline{z} ≫ \underline{a} = \underline{b} ⊢ \underline{a} · \underline{c} = \underline{b} · \underline{c}⌉, p_{0}, c)]

[Prop 3.2l_{1} →^{stmt} S ⊢ ∀\underline{a}: 0 · 0 = 0]

[Prop 3.2l_{1} →^{proof} λc.λx.P(⌈S ⊢ S7 ≫ 0 · 0 = 0⌉, p_{0}, c)]

[Prop 3.2l_{2} →^{stmt} S ⊢ ∀\underline{a}: 0 · \underline{a} = 0 ⇒ 0 · \underline{a}′ = 0]

[Prop 3.2l_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{a}: 0 · \underline{a} = 0 ⊢ S8 ≫ 0 · \underline{a}′ = 0 · \underline{a} + 0; S5 ≫ 0 · \underline{a} + 0 = 0 · \underline{a}; Prop 3.2c ⊳ 0 · \underline{a} + 0 = 0 · \underline{a} ⊳ 0 · \underline{a}′ = 0 · \underline{a} + 0 ≫ 0 · \underline{a}′ = 0 · \underline{a}; Prop 3.2c ⊳ 0 · \underline{a}′ = 0 · \underline{a} ⊳ 0 · \underline{a} = 0 ≫ 0 · \underline{a}′ = 0; Ded ⊳ ∀\underline{a}: 0 · \underline{a} = 0 ⊢ 0 · \underline{a}′ = 0 ≫ 0 · \underline{a} = 0 ⇒ 0 · \underline{a}′ = 0⌉, p_{0}, c)]

[Prop 3.2l →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: Prop 3.2l_{1} ≫ 0 · 0 = 0; Prop 3.2l_{2} ≫ 0 · \overline{x} = 0 ⇒ 0 · \overline{x}′ = 0; S9 @ \overline{x} ⊳ 0 · 0 = 0 ⊳ 0 · \overline{x} = 0 ⇒ 0 · \overline{x}′ = 0 ≫ 0 · \overline{x} = 0; Ded ⊳ 0 · \overline{x} = 0 ≫ 0 · \underline{a} = 0⌉, p_{0}, c)]

[Prop 3.2m_{1} →^{stmt} S ⊢ ∀\underline{a}: \underline{a}′ · 0 = \underline{t} · 0 + 0]

[Prop 3.2m_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: S7 ≫ \underline{a}′ · 0 = 0; Prop 3.2f ≫ 0 = 0 + 0; S7 ≫ 0 = \underline{a} · 0; Prop 3.2e ≫ 0 = \underline{a} · 0 ⇒ 0 + 0 = \underline{a} · 0 + 0; 0 = \underline{a} · 0 ⇒ 0 + 0 = \underline{a} · 0 + 0 ⊳ 0 = \underline{a} · 0 ≫ 0 + 0 = \underline{a} · 0 + 0; Prop 3.2c ≫ 0 = 0 + 0 ⇒ 0 + 0 = \underline{a} · 0 + 0 ⇒ 0 = \underline{a} · 0 + 0; 0 = 0 + 0 ⇒ 0 + 0 = \underline{a} · 0 + 0 ⇒ 0 = \underline{a} · 0 + 0 ⊳ 0 = 0 + 0 ⊳ 0 + 0 = \underline{a} · 0 + 0 ≫ 0 = \underline{a} · 0 + 0; Prop 3.2c ≫ \underline{a}′ · 0 = 0 ⇒ 0 = \underline{a} · 0 + 0 ⇒ \underline{a}′ · 0 = \underline{a} · 0 + 0; \underline{a}′ · 0 = 0 ⇒ 0 = \underline{a} · 0 + 0 ⇒ \underline{a}′ · 0 = \underline{a} · 0 + 0 ⊳ \underline{a}′ · 0 = 0 ⊳ \underline{a}′ · 0 = 0 ⇒ 0 = \underline{a} · 0 + 0 ⇒ \underline{a}′ · 0 = \underline{a} · 0 + 0 ≫ \underline{a}′ · 0 = \underline{a} · 0 + 0⌉, p_{0}, c)]

[Prop 3.2m_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ⇒ \underline{a}′ · \underline{b}′ = \underline{a} · \underline{b}′ + \underline{b}′]

[Prop 3.2m_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ⊢ S8 ≫ \underline{a}′ · \underline{b}′ = \underline{a}′ ·\underline{b}′ +\underline{a}′; Prop 3.2e ≫ \underline{a}′ ·\underline{b} = \underline{a}·\underline{b}+\underline{b} ⇒ \underline{a}′ ·\underline{b}+\underline{a}′ = \underline{a}·\underline{b}+\underline{b}+\underline{a}′; \underline{a}′ ·\underline{b} = \underline{a}·\underline{b}+\underline{b} ⇒ \underline{a}′ · \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{b} + \underline{a}′ ⊳ \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ≫ \underline{a}′ · \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{b} + \underline{a}′; S6 ≫ \underline{b} + \underline{a}′ = \underline{b} + \underline{a}′; Prop 3.2g ≫ \underline{b}′ + \underline{a} = \underline{b} + \underline{a}′; Prop 3.2d ⊳ \underline{b} + \underline{a}′ = \underline{b} + \underline{a}′ ⊳ \underline{b}′ + \underline{a} = \underline{b} + \underline{a}′ ≫ \underline{b} + \underline{a}′ = \underline{b}′ + \underline{a}; Prop 3.2h ≫ \underline{b}′ + \underline{a} = \underline{a} + \underline{b}′; Prop 3.2c ⊳ \underline{b} + \underline{a}′ = \underline{b}′ + \underline{a} ⊳ \underline{b}′ + \underline{a} = \underline{a} + \underline{b}′ ≫ \underline{b} + \underline{a}′ = \underline{a} + \underline{b}′; Prop 3.2i ⊳ \underline{b} + \underline{a}′ = \underline{a} + \underline{b}′ ≫ \underline{a} · \underline{b} + \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{a} + \underline{b}′; S8 ≫ \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a}; Prop 3.2e ⊳ \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a} ≫ \underline{a} · \underline{b}′ + \underline{b}′ = \underline{a} · \underline{b} + \underline{a} + \underline{b}′; Prop 3.2d ⊳ \underline{a} · \underline{b}′ + \underline{b}′ = \underline{a} · \underline{b} + \underline{a} + \underline{b}′ ⊳ \underline{a} · \underline{b} + \underline{b} + \underline{a}′ = \underline{a} · \underline{b} + \underline{a} + \underline{b}′ ≫ \underline{a} · \underline{b} + \underline{b} + \underline{a}′ = \underline{a} · \underline{b}′ + \underline{b}′; Prop 3.2c ⊳ \underline{a}′ · \underline{b} + \underline{a}′ = \underline{a}·\underline{b}+\underline{b}+\underline{a}′ ⊳\underline{a}·\underline{b}+\underline{b}+\underline{a}′ = \underline{a}·\underline{b}′ +\underline{b}′ ≫ \underline{a}′ ·\underline{b}+\underline{a}′ = \underline{a}·\underline{b}′ +\underline{b}′; Prop 3.2c⊳\underline{a}′ ·\underline{b}′ = \underline{a}′ · \underline{b}′ + \underline{a}′ ⊳ \underline{a}′ · \underline{b} + \underline{a}′ = \underline{a} · \underline{b}′ + \underline{b}′ ≫ \underline{a}′ · \underline{b}′ = \underline{a} · \underline{b}′ + \underline{b}′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ⊢ \underline{a}′ · \underline{b}′ = \underline{a} · \underline{b}′ + \underline{b}′ ≫ \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b} ⇒ \underline{a}′ · \underline{b}′ = \underline{a} · \underline{b}′ + \underline{b}′⌉, p_{0}, c)]

[Prop 3.2m →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: Prop 3.2m_{1} ≫ \overline{x}′ · 0 = \overline{x} · 0 + 0; Prop 3.2m_{2} ≫ \overline{x}′ · \overline{y} = \overline{x} · \overline{y} + \overline{y} ⇒ \overline{x}′ · \overline{y}′ = \overline{x} · \overline{y}′ + \overline{y}; S9 @ \overline{y} ⊳ \overline{x}′ · 0 = \overline{x} · 0 + 0 ⊳ \overline{x}′ · \overline{y} = \overline{x} · \overline{y} + \overline{y} ⇒ \overline{x}′ · \overline{y}′ = \overline{x} · \overline{y}′ + \overline{y} ≫ \overline{x}′ · \overline{y} = \overline{x} · \overline{y} + \overline{y}; Ded ⊳ \overline{x}′ · \overline{y} = \overline{x} · \overline{y} + \overline{y} ≫ \underline{a}′ · \underline{b} = \underline{a} · \underline{b} + \underline{b}⌉, p_{0}, c)]

[Prop 3.2n_{1} →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0 = 0 · \underline{a}]

[Prop 3.2n_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: S7 ≫ \underline{a} · 0 = 0; Prop 3.2l ≫ 0 · \underline{a} = 0; Prop 3.2c ⊳ \underline{a} · 0 = 0 ⊳ 0 · \underline{a} = 0 ≫ \underline{a} · 0 = 0 · \underline{a}⌉, p_{0}, c)]

[Prop 3.2n_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = \underline{b} · \underline{a} ⇒ \underline{a} · \underline{b}′ = \underline{b}′ · \underline{a}]

[Prop 3.2n_{2} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = \underline{b} · \underline{a} ⊢ S8 ≫ \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a}; Prop 3.2e ⊳ \underline{a} · \underline{b} = \underline{b} · \underline{a} ≫ \underline{a} · \underline{b} + \underline{a} = \underline{b} · \underline{a} + \underline{a}; Prop 3.2b ⊳ Prop 3.2m ≫ \underline{b} · \underline{a} + \underline{a} = \underline{b}′ · \underline{a}; Prop 3.2c ⊳ L_{e} ⊳ \underline{b} · \underline{a} + \underline{a} = \underline{b}′ · \underline{a} ≫ \underline{a} · \underline{b} + \underline{a} = \underline{b}′ · \underline{a}; Prop 3.2c ⊳ \underline{a} · \underline{b}′ = \underline{a} · \underline{b} + \underline{a} ⊳ \underline{a} · \underline{b} + \underline{a} = \underline{b}′ · \underline{a} ≫ \underline{a} · \underline{b}′ = \underline{b}′ · \underline{a}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = \underline{b} · \underline{a} ⊢ \underline{a} · \underline{b}′ = \underline{b}′ · \underline{a} ≫ \underline{a} · \underline{b} = \underline{b} · \underline{a} ⇒ \underline{a} · \underline{b}′ = \underline{b}′ · \underline{s}⌉, p_{0}, c)]

[Prop 3.2n →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: Prop 3.2n_{1} ≫ \overline{x} · 0 = 0 · \overline{x}; Prop 3.2n_{2} ≫ \overline{x} · \overline{y} = \overline{y} · \overline{x} ⇒ \overline{x} · \overline{y}′ = \overline{y}′ · \overline{x}; S9 @ \overline{y} ⊳ \overline{x} · 0 = 0 · \overline{x} ⊳ \overline{x} · \overline{y} = \overline{y} · \overline{x} ⇒ \overline{x} · \overline{y}′ = \overline{y}′ · \overline{x} ≫ \overline{x} · \overline{y} = \overline{y} = \overline{x}; Ded ⊳ \overline{x} · \overline{y} = \overline{y} = \overline{x} ≫ \underline{a} · \underline{b} = \underline{b} · \underline{a}⌉, p_{0}, c)]

[Prop 3.2o →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ Prop 3.2k ≫ \underline{a} = \underline{b} ⇒ \underline{a} · \underline{c} = \underline{b} · \underline{c}; \underline{a} = \underline{b} ⇒ \underline{a} · \underline{c} = \underline{b} · \underline{c} ⊳ \underline{a} = \underline{b} ≫ \underline{a} · \underline{c} = \underline{b} · \underline{c}; Prop 3.2n ≫ \underline{a} · \underline{c} = \underline{c}·\underline{a}; Prop 3.2n ≫ \underline{b}·\underline{c} = \underline{c}·\underline{b}; Prop 3.2c ≫ \underline{a}·\underline{c} = \underline{b}·\underline{c} ⇒ \underline{b}·\underline{c} = \underline{c}·\underline{b} ⇒ \underline{a}·\underline{c} = \underline{c}·\underline{b}; \underline{a}·\underline{c} = \underline{b}·\underline{c} ⇒ \underline{b}·\underline{c} = \underline{c}·\underline{b} ⇒ \underline{a}·\underline{c} = \underline{c}·\underline{b}⊳\underline{a}·\underline{c} = \underline{b}·\underline{c}⊳\underline{b}·\underline{c} = \underline{c}·\underline{b} ≫ \underline{a}·\underline{c} = \underline{c}·\underline{b}; S1 ≫ \underline{a}·\underline{c} = \underline{c}·\underline{b} ⇒ \underline{a}·\underline{c} = \underline{c}·\underline{a} ⇒ \underline{c}·\underline{a} = \underline{c}·\underline{b}; \underline{a}·\underline{c} = \underline{c}·\underline{b} ⇒ \underline{a}·\underline{c} = \underline{c}·\underline{a} ⇒ \underline{c}·\underline{a} = \underline{c}·\underline{b}⊳\underline{a}·\underline{c} = \underline{c}·\underline{b}⊳\underline{a}·\underline{c} = \underline{c}·\underline{a} ≫ \underline{c}·\underline{a} = \underline{c}·\underline{b}; Ded⊳∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} = \underline{b} ⊢ \underline{c}·\underline{a} = \underline{c}·\underline{b} ≫ \underline{a} = \underline{b} ⇒ \underline{c}·\underline{a} = \underline{c}·\underline{b}⌉, p_{0}, c)]

[Prop 3.4a →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} + \underline{c} = \underline{a} · \underline{b} + \underline{a} · \underline{c}]

[Prop 3.4b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{b} + \underline{c} · \underline{a} = \underline{b} · \underline{a} + \underline{c} · \underline{b}]

[Prop 3.4c →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c}]

[Prop 3.4d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} = \underline{b}]

Litteratur

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