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

projekt i logik

Maja Hanne Tønnesen, Rune Kildetoft Andresen & Niels Peter Meyn Milthers

21. juni 2006

Indhold

1 Introduction 2

2  2

Resumé

1 Introduction

In this paper we will prove the propositions regarding S starting with proposition Prop 3.2i. continuing to 3.4, bevise 3.5, aksiomer, der definerer x—y, bevise 3.10, og bevise 3.11. We chose to prove chapter 3 from mendelson, starting with Lemma 3.2, since the first ten wfs’ are proved in Mendelson, we will start with Lemma 3.2.i.

2

A modified version of Mendelsons system S (Peano arithmetic) [Men97] may be formulated thus:

[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{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{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}: Ded(\underline{a}, \underline{b}) ⊢⊢ \underline{a} ⊢ \underline{b} ⊕ Π\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{x}, \underline{a}: \underline{a} ⊢ ∀\underline{x}: \underline{a} ⊕ Π\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.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 ⊢

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

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

L_{g}: Block ≫ End ; Ded⊳ L_{g} ≫ \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 ⊢ L_{?}: Arbitrary ≫ \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 ⊢

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

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

L_{j}: Block ≫ End ; Ded⊳ L_{j} ≫ \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 ⊢

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

L_{c}: Block ≫ End ; Ded⊳ L_{c} ≫ \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 ⊢ L_{?}: Arbitrary ≫ \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 ⊢

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

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

L_{i}: Block ≫ End ; Ded⊳ L_{i} ≫ \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 ⊢

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

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

L_{c}: Block ≫ End ; Ded⊳ L_{c} ≫ \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 ⊢

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

L_{?}: Prop 3.2c⊳0 · \underline{a}′ =

0 · \underline{a}⊳0 · \underline{a} = 0 ≫ 0 · \underline{a}′ = 0 ;

L_{e}: Block ≫ End ; Ded⊳ L_{e} ≫ 0 · \underline{a} = 0 ⇒ 0 · \underline{a}′ = 0⌉, p_{0}, c)]

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

L_{?}:  Arbitrary ≫  \underline{a}  ;
L_{?}:  Block ≫  Begin  ; Prop 3.2l_{1} ≫0·

0 = 0; Prop 3.2l_{2} ≫0 · \overline{x} = 0 ⇒ 0 · \overline{x}′ = 0;

{L_{?}:  S9 @ \overline{x}⊳0 · 0 = 0⊳0 · \overline{x} = 0 ⇒ \atop 0 · \overline{x}′ = 0 ≫}  0 · \overline{x} = 0  ;
L_{c}:  Block ≫  End  ; Ded⊳

L_{c} ≫ 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 ⊢ L_{?}: Arbitrary ≫ \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 ⊢

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

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

L_{o}: Block ≫ End ; Ded⊳ L_{o} ≫ \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 ⊢

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

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

L_{c}: Block ≫ End ; Ded⊳ L_{c} ≫ \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 ⊢ L_{?}: Arbitrary ≫ \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 ⊢

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

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

L_{f}: Block ≫ End ; Ded⊳ L_{f} ≫ \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 ⊢

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

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

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

[Prop 3.2o →^{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.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};

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

L_{i}: Block ≫ End ; Ded⊳ L_{i} ≫ \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.