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 5 4 Numerals 7 5 Lemma Prop 3.7 8

5.1 Definitions of ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \overline{x} = \overline{y} . . . . . . . . . . . . 8 5.2 proof of Prop 3.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

6 Lemma Prop 3.10 10 7 Lemma Prop 3.11 11 A Helping lemmas 11

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 ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \overline{x} = \overline{y} needed to prove Prop 3.7 . after that we will define ¬∀_{obj}z: ¬\overline{y} = \overline{x} · z 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: [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]

Mendelson [Men97] defines a set of lemma’s [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}] These Lemma’s are proved in [Gru06], and we will continue to prove the following lemma’s, from Mendelson [Men97].

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

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

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]

[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{a}]

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

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

[Prop 3.4a_{1} →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: S5 ≫ \underline{b} + 0 = \underline{b}; Prop 3.2o ⊳ \underline{b} + 0 = \underline{b} ≫ \underline{a}·\underline{b}+0 = \underline{a}·\underline{b}; S5 ≫ \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; S7 ≫ \underline{a} · 0 = 0; Prop 3.2i ⊳ \underline{a} · 0 = 0 ≫ \underline{a} · \underline{b} + \underline{a} · 0 = \underline{a} · \underline{b} + 0; Prop 3.2d⊳\underline{a}·\underline{b}+0 = \underline{a}·\underline{b}+0⊳\underline{a}·\underline{b}+\underline{a}·0 = \underline{a}·\underline{b}+0 ≫ \underline{a}·\underline{b}+0 = \underline{a}·\underline{b}+\underline{a}·0⌉, p_{0}, c)]

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

[Prop 3.4a_{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{a} · \underline{c} ⊢ S6 ≫ \underline{b}+\underline{c}′ = \underline{b}+\underline{c}′; Prop 3.2o⊳\underline{b}+\underline{c}′ = \underline{b}+\underline{c}′ ≫ \underline{a}·\underline{b}+\underline{c}′ = \underline{a}·\underline{b}+\underline{c}′; S8 ≫ \underline{a}·\underline{b}+\underline{c}′ = \underline{a}·\underline{b}+\underline{c}+\underline{a}; Prop 3.2e⊳\underline{a}·\underline{b}+\underline{c} = \underline{a}·\underline{b}+\underline{a}·\underline{c} ≫ \underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}; Prop 3.2j ≫ \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}; Prop 3.2c⊳\underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}⊳\underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a} ≫ \underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}; S8 ≫ \underline{a}·\underline{c}′ = \underline{a}·\underline{c}+\underline{a}; Prop 3.2i⊳\underline{a}·\underline{c}′ = \underline{a}·\underline{c}+\underline{a} ≫ \underline{a}·\underline{b}+\underline{a}·\underline{c}′ = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}; Prop 3.2d⊳\underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a}⊳\underline{a}·\underline{b}+\underline{a}·\underline{c}′ = \underline{a}·\underline{b}+\underline{a}·\underline{c}+\underline{a} ≫ \underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a}·\underline{b}+\underline{a}·\underline{c}′; Prop 3.2c⊳\underline{a}·\underline{b}+\underline{c}′ = \underline{a}·\underline{b}+\underline{c}+\underline{a}⊳\underline{a}·\underline{b}+\underline{c}+\underline{a} = \underline{a} · \underline{b} + \underline{a} · \underline{c}′ ≫ \underline{a} · \underline{b} + \underline{c}′ = \underline{a} · \underline{b} + \underline{a} · \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{a} · \underline{c}′ ≫ \underline{a} · \underline{b} + \underline{c}′ = \underline{a} · \underline{b} + \underline{a} · \underline{c}′; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · \underline{b} + \underline{c} = \underline{a} · \underline{b} + \underline{a} · \underline{c} ⊢ \underline{a} · \underline{b} + \underline{c}′ = \underline{a} · \underline{b} + \underline{a} · \underline{c}′ ≫ \underline{a} · \underline{b} + \underline{c} = \underline{a} · \underline{b} + \underline{a} · \underline{c} ⇒ \underline{a} · \underline{b} + \underline{c}′ = \underline{a} · \underline{b} + \underline{a} · \underline{c}′⌉, p_{0}, c)]

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

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

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

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

[Prop 3.4c_{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.4c_{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} ⊢ S8 ≫ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b}; Prop 3.2e ⊳ \underline{a} · \underline{b} · \underline{c} = \underline{a} · \underline{b} · \underline{c} ≫ \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b}; Prop 3.2c ⊳ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} ⊳ \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} ≫ \underline{a}·\underline{b}·\underline{c}′ = \underline{a}·\underline{b}·\underline{c}+\underline{a}·\underline{b}; Prop 3.4a ≫ \underline{a}·\underline{b}·\underline{c}+\underline{b} = \underline{a}·\underline{b}·\underline{c}+\underline{a}·\underline{b}; Prop 3.2d⊳\underline{a}·\underline{b}·\underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} ⊳ \underline{a} · \underline{b} · \underline{c} + \underline{b} = \underline{a} · \underline{b} · \underline{c} + \underline{a} · \underline{b} ≫ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{b}; S8 ≫ \underline{b} · \underline{c}′ = \underline{b} · \underline{c} + \underline{b}; Prop 3.2o ⊳ \underline{b} · \underline{c}′ = \underline{b} · \underline{c} + \underline{b} ≫ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{b}; Prop 3.2d ⊳ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{b} ⊳ \underline{a} · \underline{b} · \underline{c}′ = \underline{a} · \underline{b} · \underline{c} + \underline{b} ≫ \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.4c →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: Prop 3.4c_{1} ≫ \overline{x} · \overline{y} · 0 = \overline{x}·\overline{y}·0; Prop 3.4c_{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.4d_{1} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + 0 = \underline{b} + 0 ⇒ \underline{a} = \underline{b}]

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

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

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

[Prop 3.4d →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: Prop 3.4d_{1} ≫ \overline{x} + 0 = \overline{y} + 0 ⇒ \overline{x} = \overline{y}; Prop 3.4d_{2} ≫ \overline{x}+\overline{z} = \overline{y} +\overline{z} ⇒ \overline{x} = \overline{y} ⇒ \overline{x}+\overline{z}′ = \overline{y} +\overline{z}′ ⇒ \overline{x} = \overline{y}; S9 @ \overline{z}⊳\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} ⇒ \overline{x} = \overline{y}; Ded ⊳ \overline{x} + \overline{z} = \overline{y} + \overline{z} ⇒ \overline{x} = \overline{y} ≫ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} = \underline{b}⌉, p_{0}, c)]

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 0, 0′, 0′′ … With these definitions we will now continue to prove Prop 3.5 that states different things about numerals.

[Prop 3.5a →^{stmt} S ⊢ ∀\underline{a}: \underline{a} + 0′ = \underline{a}′]

[Prop 3.5b →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0′ = \underline{a}]

[Prop 3.5c →^{stmt} S ⊢ ∀\underline{a}: \underline{a} · 0′′ = \underline{a} + \underline{a}] [Prop 3.5d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ \underline{b} = 0]

[Prop 3.5e →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} = 0 ⇒ \underline{b} · \underline{a} = 0 ⇒ \underline{b} = 0]

[Prop 3.5f →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0′ ⇒ ¬¬\underline{a} = 0 ⇒ \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ \underline{b} = 0]

[Prop 3.5g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} · \underline{b} = 0′ ⇒ ¬\underline{a} = 0′ ⇒ \underline{b} = 0′]

[Prop 3.5h →^{stmt} S ⊢ ∀\underline{a}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}\underline{b}: ¬\underline{a} = \underline{b}′]

[Prop 3.5i →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{c} = 0 ⇒ \underline{a} · \underline{c} = \underline{b} · \underline{c} ⇒ \underline{a} = \underline{b}]

[Prop 3.5j →^{stmt} S ⊢ ∀\underline{a}: ¬\underline{a} = 0 ⇒ ¬\underline{a} = 0′ ⇒ ¬∀_{obj}\underline{b}: ¬\underline{a} = \underline{b}′′]

[Prop 3.5a →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: S6 ≫ \underline{a} + 0′ = \underline{a} + 0′; S5 ≫ \underline{a} + 0 = \underline{a}; S2⊳\underline{a}+0 = \underline{a} ≫ \underline{a}+0′ = \underline{a}′; Prop 3.2c⊳\underline{a}+0′ = \underline{a}+0′ ⊳\underline{a}+0′ = \underline{a}′ ≫ \underline{a}+0′ = \underline{a}′; Prop 3.2a ≫ \underline{a}+0′ = \underline{a}+0′; S1⊳\underline{a}+0′ = \underline{a}+0′⊳\underline{a}+0′ = \underline{a}′ ≫ \underline{a}+0′ = \underline{a}′⌉, p_{0}, c)]

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

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

[Prop 3.5d_{1} →^{stmt} S ⊢ ∀\underline{a}: \underline{a} + 0 ⇒ \underline{a} = 0 ∧ 0 = 0]

[Prop 3.5d_{2} →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} + \underline{b} = 0 ⇒ ¬\underline{a} = 0 ⇒ \underline{b} = 0 ⇒ \underline{a} + \underline{b}′ = 0 ⇒ ¬\underline{a} = 0 ⇒ \underline{b}′ = 0]

5 Lemma Prop 3.7

5.1 Definitions of ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \overline{x} = \overline{y}

in the folowing we need some definitions, we will macro define them as: [x < y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x < y ¨= ∃z: (z ≠ 0 ∧ z + x = y)]⌉)] [x ≤ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ≤ y ¨= x < y ∨ x = y]⌉)] [x > y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x > y ¨= y < x]⌉)] [x ≥ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ≥ y ¨= y ≤ x]⌉)] [x ≮ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ≮ y ¨= ¬(x < y)]⌉)] [x ≯ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ≯ y ¨= y ≮ x]⌉)] [x | y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x | y ¨= ∃z: y = x · z]⌉)] with these definitions, we will continue to prove the following statements: [Prop 3.7a →^{stmt} S ⊢ ∀\underline{a}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{a}] [Prop 3.7b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} = \underline{c} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{c}] [Prop 3.7c →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} = \underline{a}] [Prop 3.7d →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} + \underline{c} = \underline{b} + \underline{c}] [Prop 3.7e →^{stmt} S ⊢ ∀\underline{a}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{a} ⇒ \underline{a} = \underline{a}] [Prop 3.7f →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} = \underline{c} ⇒ \underline{b} = \underline{c} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{c} ⇒ \underline{a} = \underline{c}] [Prop 3.7g →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c}] [Prop 3.7g′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ \underline{a} + \underline{c} = \underline{b} + \underline{c} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b}] [Prop 3.7h →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} = \underline{c} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{c}] [Prop 3.7i →^{stmt} S ⊢ ∀\underline{a}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + 0 = \underline{a} ⇒ 0 = \underline{a}] [Prop 3.7j →^{stmt} S ⊢ ∀\underline{a}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + 0 = \underline{a}′] [Prop 3.7k →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a}′ = \underline{b} ⇒ \underline{a}′ = \underline{b}] [Prop 3.7k′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a}′ = \underline{b} ⇒ \underline{a}′ = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b}] [Prop 3.7l →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b}′] [Prop 3.7l′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b}′ ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b}] [Prop 3.7m →^{stmt} S ⊢ ∀\underline{a}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{a}′] [Prop 3.7o →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} = \underline{a}] [Prop 3.7p →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬\underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} = \underline{a}] [Prop 3.7q →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} = \underline{a} ⇒ \underline{b} = \underline{a}] [Prop 3.7r →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{a} + \underline{b} ⇒ \underline{a} = \underline{a} + \underline{b}] [Prop 3.7s →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{a} + \underline{b}] [Prop 3.7t →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{b} = 0 ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{a} · \underline{b} ⇒ \underline{a} = \underline{a} · \underline{b}] [Prop 3.7u →^{stmt} S ⊢ ∀\underline{a}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + 0 = \underline{a}] [Prop 3.7u′ →^{stmt} S ⊢ ∀\underline{a}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + 0 = \underline{a} ⇒ ¬\underline{a} = 0] [Prop 3.7v →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + 0 = \underline{a} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + 0 = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + 0 = \underline{a} · \underline{b}] [Prop 3.7w →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + 0′ = \underline{b} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} · \underline{a}] [Prop 3.7x →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} = \underline{c} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} · \underline{a} = \underline{c} · \underline{a}] [Prop 3.7x′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} · \underline{a} = \underline{c} · \underline{a} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} = \underline{c}] [Prop 3.7y →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} = 0 ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} = \underline{c} ⇒ \underline{b} = \underline{c} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} · \underline{a} = \underline{c} · \underline{a} ⇒ \underline{b} · \underline{a} = \underline{c} · \underline{a}] [Prop 3.7y′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ¬\underline{a} = 0 ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} · \underline{a} = \underline{c} · \underline{a} ⇒ \underline{b} · \underline{a} = \underline{c} · \underline{a} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} = \underline{c} ⇒ \underline{b} = \underline{c}] [Prop 3.7z →^{stmt} S ⊢ ∀\underline{a}: ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = 0] [Prop 3.7z′ →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{b} ⇒ \underline{a} = \underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{b} = \underline{a} ⇒ \underline{b} = \underline{a} ⇒ \underline{a} = \underline{b}]

5.2 proof of Prop 3.7

6 Lemma Prop 3.10

[Prop 3.10a →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{a} = ∀\underline{a}: \underline{a} · z] [Prop 3.10b →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{a} = ∀\underline{a}: 0′ · z] [Prop 3.10c →^{stmt} S ⊢ ¬∀_{obj}z: ¬0 = ∀\underline{a}: \underline{a} · z] [Prop 3.10d →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{c} = ¬∀_{obj}z: ¬\underline{c} ⇒ \underline{a} = ¬∀_{obj}z: ¬\underline{b} ∧ \underline{b} = ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · z · z · z] [Prop 3.10e →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{b} ⇒ ¬¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{a} = \underline{a} ⇒ \underline{a} = \underline{a} = ∀\underline{a}: ∀\underline{b}: ¬¬\underline{a} = 0 ⇒ \underline{b} · z] [Prop 3.10f →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{a} ⇒ \underline{a} = \underline{b} = ¬∀_{obj}z: ¬¬\underline{b} ⇒ \underline{b} = ∀\underline{a}: ∀\underline{b}: \underline{a} · z · z] [Prop 3.10g →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{b} · \underline{c} = ¬∀_{obj}z: ¬\underline{b} ⇒ \underline{a} = ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · z · z] [Prop 3.10h →^{stmt} S ⊢ ¬∀_{obj}z: ¬\underline{b} + \underline{c} = ¬∀_{obj}z: ¬\underline{c} ⇒ \underline{a} = ¬∀_{obj}z: ¬\underline{b} ∧ \underline{a} = ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} · z · z · z]

7 Lemma Prop 3.11

[Prop 3.11 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} = 0 ⇒ ¬∀_{obj}\underline{c}: ∀_{obj}\underline{d}: ¬¬¬\underline{b} = \underline{a} · \underline{c} + \underline{d} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{d} = \underline{a} ⇒ ∀_{obj}\underline{e}: ∀_{obj}\underline{f} : ¬\underline{b} = \underline{a} · \underline{e} + \underline{f} ⇒ ¬∀_{obj}z: ¬¬¬z = 0 ⇒ z + \underline{f} = \underline{a} ⇒ ¬\underline{c} = \underline{e} ⇒ \underline{d} = \underline{f}]

A Helping lemmas

for some of our proofs we need to prove some lemmas concerning ∧ and ∨ these will be proved here. [T0 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{b} ⇒ \underline{a} ⇒ \underline{b}] [T1 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⇒ \underline{a} ⇒ \underline{b}] [H0a →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⊢ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⇒ \underline{c}] [H0b →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{b} ⊢ \underline{a} ⇒ \underline{c}] [H1 →^{stmt} S ⊢ ∀\underline{a}: ¬¬\underline{a} ⇒ \underline{a}] [H2 →^{stmt} S ⊢ ∀\underline{a}: \underline{a} ⇒ ¬¬\underline{a}] [Con1 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⇒ \underline{b} ⊢ \underline{a}] [Con2 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⇒ \underline{b} ⊢ \underline{b}] [Con →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ \underline{b} ⊢ ¬\underline{a} ⇒ \underline{b}] [Dis1 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ ¬\underline{a} ⇒ \underline{b}] [Dis2 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{b} ⊢ ¬\underline{a} ⇒ \underline{b}]

[T0 →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: \underline{b} ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ Repetition ⊳ \underline{b} ≫ \underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ \underline{b} ≫ \underline{a} ⇒ \underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: \underline{b} ⊢ \underline{a} ⇒ \underline{b} ≫ \underline{b} ⇒ \underline{a} ⇒ \underline{b}⌉, p_{0}, c)]

[T1 →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ Repetition ⊳ ¬\underline{a} ≫ ¬\underline{a}; T0 ≫ \underline{a} ⇒ ¬\underline{b} ⇒ \underline{a}; MP ⊳ \underline{a} ⇒ ¬\underline{b} ⇒ \underline{a} ⊳ \underline{a} ≫ ¬\underline{b} ⇒ \underline{a}; T0 ≫ ¬\underline{a} ⇒ ¬\underline{b} ⇒ ¬\underline{a}; MP⊳¬\underline{a} ⇒ ¬\underline{b} ⇒ ¬\underline{a}⊳¬\underline{a} ≫ ¬\underline{b} ⇒ ¬\underline{a}; Neg⊳¬\underline{b} ⇒ ¬\underline{a}⊳¬\underline{b} ⇒ \underline{a} ≫ \underline{b}; Ded⊳ ∀\underline{a}: ∀\underline{b}: \underline{a} ⊢ \underline{b} ≫ \underline{a} ⇒ \underline{b}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ¬\underline{a} ⊢ \underline{a} ⇒ \underline{b} ≫ ¬\underline{a} ⇒ \underline{a} ⇒ \underline{b}⌉, p_{0}, c)]

[H0a →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⊢ \underline{b} ⇒ \underline{c} ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⊢ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⊢ MP ⊳ \underline{a} ⇒ \underline{b} ⊳ \underline{a} ≫ \underline{b}; MP ⊳ \underline{b} ⇒ \underline{c} ⊳ \underline{b} ≫ \underline{c}; Ded ⊳ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⊢ \underline{b} ⇒ \underline{c} ⊢ \underline{a} ⊢ \underline{c} ≫ \underline{a} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{a} ⇒ \underline{c}; MP ⊳ \underline{a} ⇒ \underline{b} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{a} ⇒ \underline{c} ⊳ \underline{a} ⇒ \underline{b} ≫ \underline{b} ⇒ \underline{c} ⇒ \underline{a} ⇒ \underline{c}; MP ⊳ \underline{b} ⇒ \underline{c} ⇒ \underline{a} ⇒ \underline{c} ⊳ \underline{b} ⇒ \underline{c} ≫ \underline{a} ⇒ \underline{c}⌉, p_{0}, c)]

[H0b →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⊢ \underline{b} ⊢ A2′ ≫ \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{a} ⇒ \underline{b} ⇒ \underline{a} ⇒ \underline{c}; MP ⊳ \underline{a} ⇒ \underline{b} ⇒ \underline{c} ⇒ \underline{a} ⇒ \underline{b} ⇒ \underline{a} ⇒ \underline{c} ⊳ \underline{a} ⇒ \underline{b} ⇒ \underline{c} ≫ \underline{a} ⇒ \underline{b} ⇒ \underline{a} ⇒ \underline{c}; T0 ≫ \underline{b} ⇒ \underline{a} ⇒ \underline{b}; MP ⊳ \underline{b} ⇒ \underline{a} ⇒ \underline{b} ⊳ \underline{b} ≫ \underline{a} ⇒ \underline{b}; MP ⊳ \underline{a} ⇒ \underline{b} ⇒ \underline{a} ⇒ \underline{c} ⊳ \underline{a} ⇒ \underline{b} ≫ \underline{a} ⇒ \underline{c}⌉, p_{0}, c)]

[H1 →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: Neg ≫ ¬\underline{a} ⇒ ¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬\underline{a} ⇒ \underline{a}; Repetition ≫ ¬\underline{a} ⇒ ¬\underline{a}; H0b ⊳ ¬\underline{a} ⇒ ¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬\underline{a} ⇒ \underline{a} ⊳ ¬\underline{a} ⇒ ¬\underline{a} ≫ ¬\underline{a} ⇒ ¬¬\underline{a} ⇒ \underline{a}; A1′ ≫ ¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬¬\underline{a}; H0a ⊳ ¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬¬\underline{a} ⊳ ¬\underline{a} ⇒ ¬¬\underline{a} ⇒ \underline{a} ≫ ¬¬\underline{a} ⇒ \underline{a}⌉, p_{0}, c)]

[H2 →^{proof} λc.λx.P(⌈S ⊢ ∀\underline{a}: Neg ≫ ¬¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬¬¬\underline{a} ⇒ \underline{a} ⇒ ¬¬\underline{a}; H1 ≫ ¬¬¬\underline{a} ⇒ ¬\underline{a}; MP ⊳ ¬¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬¬¬\underline{a} ⇒ \underline{a} ⇒ ¬¬\underline{a} ⊳ ¬¬¬\underline{a} ⇒ ¬\underline{a} ≫ ¬¬¬\underline{a} ⇒ \underline{a} ⇒ ¬¬\underline{a}; A1′ ≫ \underline{a} ⇒ ¬¬¬\underline{a} ⇒ \underline{a}; H1 ⊳ ¬¬¬\underline{a} ⇒ \underline{a} ⇒ ¬¬\underline{a} ⊳ \underline{a} ⇒ ¬¬¬\underline{a} ⇒ \underline{a} ≫ \underline{a} ⇒ ¬¬\underline{a}⌉, p_{0}, c)]

Litteratur

[Gru06] K. Grue. A logiweb base page. Technical report, Logiweb, 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.