Logic - Peano Arithmetic

˙∀ṫ: ˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ)

Kasper Frederiksen, tofu@diku.dk

GRD-2005-07-04.UTC:08:28:05.801232

Contents

1 Introduction 3 1.1 About LogiWeb . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 About the proof system . . . . . . . . . . . . . . . . . . . . . . . 3

2 The Deduction Algorithm 5

3 Supporting Lemmas 5 3.1 Corollary C1.10a . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.2 Corollary C1.10(b) . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.3 Lemma A1′^{∗} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.4 Lemma A2′^{∗} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.5 Lemma DoubleHypothesis . . . . . . . . . . . . . . . . . . . . . . 7 3.6 Lemma L1.8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8 3.7 Lemma Tautology1 . . . . . . . . . . . . . . . . . . . . . . . . . . 8

4 The Main Proofs 9 4.1 Lemma L3.2(b)′ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.2 Lemma L3.2(c)′ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.3 Lemma L3.2(d)′ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 4.4 Lemma L3.2(f)′ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

4.4.1 The base case of L3.2(f)′ . . . . . . . . . . . . . . . . . . . 10 4.4.2 The induction step of L3.2(f)′ . . . . . . . . . . . . . . . . 11

4.5 Lemma L3.2(g)′ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 4.5.1 Base case of L3.2(g)′ . . . . . . . . . . . . . . . . . . . . . 12 4.5.2 Induction step of L3.2(g)′ . . . . . . . . . . . . . . . . . . 13

4.6 Lemma L3.2(h)′ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 4.6.1 Base case of L3.2(h)′ . . . . . . . . . . . . . . . . . . . . . 15 4.6.2 Induction step of L3.2(h)′ . . . . . . . . . . . . . . . . . . 15 5 Conclusion 17 A The name of the page 18 B The Bibliography 18

1 Introduction

This report proves proposition L3.2(h)′ in [Mendelson, 2001], page 156. That is:

[S′ lemma L3.2(h)′: ˙∀ṫ: ˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ)]

The successful proof of this lemma can be seen in section 4.6.

The entire text has been verified as mathematically correct by the LogiWeb system. The source code can be obtained from the online version of this text:

      http://www.diku.dk/hjemmesider/studerende/tofu/Logik/

1.1 About LogiWeb

The LogiWeb system is being developed by Klaus Grue (DIKU) and is fully defined on the LogiWeb base page ^{1} written by Klaus Grue:

 http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/latest/

From a users point of view LogiWeb consists of two parts, a compiler and a (web)server. The user will write his text using latex syntax and whenever he wishes to express mathematics this will be written amongst the ordinary text, but using pyk syntax. When the source file is compiled two things happen. The pyk part of the file is translated into latex and given to the latex compiler along with the rest of the text, also the mathematics expressed by the pyk is checked for correctness.

The LogiWeb system allows the user to reference mathematical constructs defined on other pages. The task of managing requests for these pages falls to the LogiWeb server. The LogiWeb server on DIKU has a graphical front-end in the form of a webserver, that can be accessed through the links given above.

1.2 About the proof system

All proofs in this text have been completed in the axiomatic arithmetic system called S′. This system is a Peano Arithmetic system and is fully defined on the peano page ^{2} written by Klaus Grue:

    http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano/

It should be noted that the peano page redefines all the arithmetic and logical operators from base page in special “peano versions”. These new operators are identical to their classical counterparts. To avoid any confusion figure (1) gives an overview of the new operators.

1This report uses the version of base page that has the time stamp GRD-2005-06-22-UTC-06-58-05-413682

2This report uses the version of peano page that has the time stamp GRD-2005-06-22-UTC-07-23-31-271829

False ⇒ True  →  F ˙⇒ T
arbitraryvariable : A, B, C, ... →  A, B, C,…
specificterms : a, b, c, ... → ȧ, ḃ, ċ,…
∀a : a + 0 = a  → ˙∀ȧ: (ȧ ˙+ ˙0 =^{p} ȧ)
¬(1 · 0 = 1)  → ˙¬ (˙1 ˙· ˙0 =^{p} ˙1)

Figure 1: The new version of the operators

Peano arithmetic is only defined on natural numbers, and the successor operation is written like this: ˙0′ =^{p} ˙1.

This peano page also defines the axioms and rules of the S′ system. These are identical to those defined in [Mendelson, 2001], chapters two and three. Below I repeat the theory as it is defined on the peano page. Since the pyk syntax is not always obvious I have included some comments.

System [S′] is defined thus:

[Theory S′]
[S′ rule A1′: ∀A: ∀B: A ˙⇒ B ˙⇒ A]
[S′ rule A2′: ∀A: ∀B: ∀C: (A ˙⇒ B ˙⇒ C) ˙⇒ (A ˙⇒ B) ˙⇒ A ˙⇒ C]
[S′ rule A3′: ∀A: ∀B: ( ˙¬ B ˙⇒ ˙¬ A) ˙⇒ ( ˙¬ B ˙⇒ A) ˙⇒ B]
[S′ rule A4′: ∀C: ∀A: ∀X: ∀B: ⌈A⌉≡⟨⌈B⌉|⌈X ⌉ := ⌈C⌉⟩ ⊢⊢ ˙∀X: B ˙⇒ A]

This axiom allows us to remove a universal kvantor and replace the quantified variable with a specific term, as long as this does not cause a variable clash. When using the axiom, you must state which term you wish to substitute into the place of the quantified variable. The axiom is used like this: A4′ @ ṫ → ˙∀q̇: q̇ =^{p} q̇ ˙⇒ ṫ =^{p} ṫ

[S′ rule A5′: ∀X: ∀A: ∀B: ṅonfree(⌈X ⌉, ⌈A⌉) ⊢⊢ ˙∀X: (A ˙⇒ B) ˙⇒ A ˙⇒

˙∀X: B]

This axiom is not used in this report.

[S′ rule MP′: ∀A: ∀B: A ˙⇒ B ⊢ A ⊢ B]
[S′ rule Gen′: ∀X: ∀A: A ⊢ ˙∀X: A]

This is the generalization rule, that allows us to add a universal kvantor in front of a proof line.

[S′ rule S1′: ∀A: ∀B: ∀C: A =^{p} B ˙⇒ A =^{p} C ˙⇒ B =^{p} C]

[S′ rule S2′: ∀A: ∀B: A =^{p} B ˙⇒ A′ =^{p} B′]

[S′ rule S3′: ∀A: ¬˙0 =^{p} A′]

[S′ rule S4′: ∀A: ∀B: A′ =^{p} B′ ˙⇒ A =^{p} B]

[S′ rule S5′: ∀A: A ˙+ ˙0 =^{p} A]

[S′ rule S6′: ∀A: ∀B: A ˙+ B′ =^{p} (A ˙+ B)′]

[S′ rule S7′: ∀A: A ˙· ˙0 =^{p} ˙0]

[S′ rule S8′: ∀A: ∀B: A ˙·(B′) =^{p} (A ˙· B) ˙+ A]

[S′ rule S9′: ∀A: ∀B: ∀C: ∀X:

B≡⟨A|X := ˙0⟩ ⊢⊢ C≡⟨A|X := X′⟩ ⊢⊢

B ˙⇒ ˙∀X: (A ˙⇒ C) ˙⇒ ˙∀X: A]

This is the induction axiom. What it basically says is “base case” ⇒ “induction step” ⇒ “conclusion”.

2 The Deduction Algorithm

Mendelson introduces the Deduction Theorem for first-order theories in [Mendelson, 2001] page 74. The proof is stated in the form of an algorithm that will turn a proof of the the lemma S′ ⊢ (B ⊢ C), in to a proof of the lemma S′ ⊢ B ˙⇒ C.

While it would be possible to implement this automatic proof converter in pyk, as a part of this text, Klaus has advised that we do not attempt this. We are going to follow this advise. Instead we run the algorithm by hand and type in the converted proofs.

A god description of the deduction algorithm can be found at:

     http://www.diku.dk/undervisning/2005s/235/deduction.html

3 Supporting Lemmas

Before we start proving the lemmas in section 4. Let us first prove a number of lemmas that will help make the following proofs shorter.

Pleas note that many of the lemmas in this section were included on a whenneeded basis. If, in section 4, you notice a situation where one of the following lemmas could have been used to shorten the proof, then that is an “older” proof from before the supporting lemma was included.

3.1 Corollary C1.10a

The lemma [C1.10a]^{3} is taken from [Mendelson, 2001] page 38.

[S′ lemma C1.10a: ∀B: ∀C: ∀D: (B ˙⇒ C ⊢ C ˙⇒ D ⊢ B ˙⇒ D)] S′ proof of C1.10a:

L01: Arbitrary ≫  B  ;
L02: Arbitrary ≫  C  ;
L03: Arbitrary ≫  D  ;
L04: Premise ≫  B ˙⇒ C  ;
L05: Premise ≫  C ˙⇒ D  ;
L06: A1′ ≫  (C ˙⇒ D) ˙⇒ (B ˙⇒ (C ˙⇒ D))  ;
L07: MP′ ⊳ L06 ⊳ L05 ≫  B ˙⇒ (C ˙⇒ D)  ;
L08: A2′ ≫  {(B ˙⇒ (C ˙⇒ D)) ˙⇒ ((B ˙⇒ C) ˙⇒ \atop (B ˙⇒ D))  ;}
L09: MP′ ⊳ L08 ⊳ L07 ≫  (B ˙⇒ C) ˙⇒ (B ˙⇒ D)  ;
L10: MP′ ⊳ L09 ⊳ L04 ≫  B ˙⇒ D  □

3.2 Corollary C1.10(b)

The lemma [C1.10(b)]^{4} is taken from [Mendelson, 2001] page 38.

[S′ lemma C1.10(b): ∀B: ∀C: ∀D: (B ˙⇒ (C ˙⇒ D) ⊢ C ⊢ B ˙⇒ D)] S′ proof of C1.10(b):

L01: Arbitrary ≫  B  ;
L02: Arbitrary ≫  C  ;
L03: Arbitrary ≫  D  ;
L04: Premise ≫  B ˙⇒ (C ˙⇒ D)  ;
L05: Premise ≫  C  ;
L06: A1′ ≫  C ˙⇒ (B ˙⇒ C)  ;
L07: MP′ ⊳ L06 ⊳ L05 ≫  B ˙⇒ C  ;
L08: A2′ ≫  {(B ˙⇒ (C ˙⇒ D)) ˙⇒ ((B ˙⇒ C) ˙⇒ \atop (B ˙⇒ D))  ;}
L09: MP′ ⊳ L08 ⊳ L04 ≫  (B ˙⇒ C) ˙⇒ (B ˙⇒ D)  ;
L10: MP′ ⊳ L09 ⊳ L07 ≫  B ˙⇒ D  □

3.3 Lemma A1′^{∗}

The lemma [A1′^{∗}]^{5} is used during the deduction algorithm, when one wishes to add a hypothesis, H, to a line of a proof. This will shorten the proof by one line.

3[C1.10a =^{pyk} “corollary one point ten a”]

4[C1.10(b) =^{pyk} “corollary one point ten b”]

5[A1′^{∗} =^{pyk} “lemma prime a one star”]

[S′ lemma A1′^{∗}: ∀A: ∀H: (A ⊢ H ˙⇒ A)]

S′ proof of A1′^{∗}:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  H  ;
L03: Premise ≫  A  ;
L04: A1′ ≫  A ˙⇒ (H ˙⇒ A)  ;
L05: MP′ ⊳ L04 ⊳ L03 ≫  H ˙⇒ A  □

3.4 Lemma A2′^{∗}

Use of the axiom A2′ is often followed by a use of the modus ponens rule. If we instead use lemma [A2′^{∗}]^{6} , then the modus ponens is not necessary.

[S′ lemma A2′^{∗}: ∀H: ∀A: ∀B: (H ˙⇒ (A ˙⇒ B)) ⊢ ((H ˙⇒ A) ˙⇒ (H ˙⇒ B))]

S′ proof of A2′^{∗}:

L01: Arbitrary ≫  H  ;
L02: Arbitrary ≫  A  ;
L03: Arbitrary ≫  B  ;
L04: Premise ≫  H ˙⇒ (A ˙⇒ B)  ;
L05: A2′ ≫  {(H ˙⇒ (A ˙⇒ B)) ˙⇒ ((H ˙⇒ \atop A) ˙⇒ (H ˙⇒ B))  ;}
L06: MP′ ⊳ L05 ⊳ L04 ≫  (H ˙⇒ A) ˙⇒ (H ˙⇒ B)  □

3.5 Lemma DoubleHypothesis

The lemma [DoubleHypothesis]^{7} is used during the deduction algorithm, when one wishes to add a hypothesis, H, to a proof line of the form A ˙⇒ B. This will shorten the proof by one line.

[S′ lemma DoubleHypothesis: ∀A: ∀B: ∀H: (A ˙⇒ B ⊢ ((H ˙⇒ A) ˙⇒ (H ˙⇒

B)))]

S′ proof of DoubleHypothesis:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  H  ;
L04: Premise ≫  A ˙⇒ B  ;
L05: A1′^{∗} ⊳ L04 ≫  H ˙⇒ (A ˙⇒ B)  ;
L06: A2′^{∗} ⊳ L05 ≫  (H ˙⇒ A) ˙⇒ (H ˙⇒ B)  □

6[A2′^{∗} =^{pyk} “lemma prime a two star”]

7[DoubleHypothesis =^{pyk} “lemma double hyp”]

3.6 Lemma L1.8

Lemma [L1.8]^{8} from [Mendelson, 2001] page 36, is used to introduce the premise at the start of the deduction algorithm.

[S′ lemma L1.8: ∀B: (B ˙⇒ B)] S′ proof of L1.8:

L01: Arbitrary ≫  B  ;
L02: A2′ ≫  {(B ˙⇒ ((B ˙⇒ B) ˙⇒ B)) ˙⇒ \atop ((B ˙⇒ (B ˙⇒ B)) ˙⇒ (B ˙⇒ B))  ;}
L03: A1′ ≫  B ˙⇒ ((B ˙⇒ B) ˙⇒ B)  ;
L04: MP′ ⊳ L02 ⊳ L03 ≫  (B ˙⇒ (B ˙⇒ B)) ˙⇒ (B ˙⇒ B)  ;
L05: A1′ ≫  B ˙⇒ (B ˙⇒ B)  ;
L06: MP′ ⊳ L04 ⊳ L05 ≫  B ˙⇒ B  □

3.7 Lemma Tautology1

The lemma that I call [Tautology1]^{9} is an all-round useful lemma.

[S′ lemma Tautology1: ∀A: ∀B: ∀C: ((A ˙⇒ (B ˙⇒ C)) ⊢ (B ˙⇒ (A ˙⇒ C)))] S′ proof of Tautology1:

L01: Arbitrary ≫  A  ;
L02: Arbitrary ≫  B  ;
L03: Arbitrary ≫  C  ;
L04: Premise ≫  A ˙⇒ (B ˙⇒ C)  ;
L05: A2′ ≫  {(A ˙⇒ (B ˙⇒ C)) ˙⇒ ((A ˙⇒ B) ˙⇒ \atop (A ˙⇒ C))  ;}
L06: MP′ ⊳ L05 ⊳ L04 ≫  (A ˙⇒ B) ˙⇒ (A ˙⇒ C)  ;
L07: A1′ ≫  {((A ˙⇒ B) ˙⇒ (A ˙⇒ C)) ˙⇒ (B ˙⇒ \atop ((A ˙⇒ B) ˙⇒ (A ˙⇒ C)))  ;}
L08: MP′ ⊳ L07 ⊳ L06 ≫  B ˙⇒ ((A ˙⇒ B) ˙⇒ (A ˙⇒ C))  ;
L09: A2′ ≫  (B ˙⇒ ((A ˙⇒ B) ˙⇒ (A ˙⇒ ; C))) ˙⇒ ((B ˙⇒ (A ˙⇒ B)) ˙⇒ ; (B ˙⇒ (A ˙⇒ C)))  ;
L10: MP′ ⊳ L09 ⊳ L08 ≫  {(B ˙⇒ (A ˙⇒ B)) ˙⇒ (B ˙⇒ (A ˙⇒ \atop C))  ;}
L11: A1′ ≫  B ˙⇒ (A ˙⇒ B)  ;
L12: MP′ ⊳ L10 ⊳ L11 ≫  B ˙⇒ (A ˙⇒ C)  □

8[L1.8 =^{pyk} “lemma one point eight”]

9[Tautology1 =^{pyk} “tautology one”]

4 The Main Proofs

The purpose of this report is the proof of L3.2(h)′ in section 4.6. In order to get that far we must first prove a number of the lemmas that precede it in [Mendelson, 2001]. Of these lemma L3.2(a)′ has been proved by Klaus on the peano page and lemma L3.2(e)’ is not needed. Taking into account the support lemmas proved in section 3, this leaves parts (b), (c), (d), (f), (g) and of course (h), still to be proven.

Of these lemmas (f), (g) and (h) are proved using induction, which means that we will need the Deduction Algorithm.

All of these lemmas are proved in [Mendelson, 2001], so the task of this report has been to rewrite Mendelson’s proofs in explicit form and use the deduction algorithm where necessary.

4.1 Lemma L3.2(b)′

[L3.2(b)′]^{10}

[S′ lemma L3.2(b)′: ∀T : ∀R: T =^{p} R ˙⇒ R =^{p} T ]

S′ proof of L3.2(b)′:

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: S1′ ≫  T =^{p} R ˙⇒ (T =^{p} T ˙⇒ R =^{p} T )  ;
L04: L3.2(a)′ ≫  T =^{p} T  ;
L05: C1.10(b) ⊳ L03 ⊳ L04 ≫  T =^{p} R ˙⇒ R =^{p} T  □

4.2 Lemma L3.2(c)′

[L3.2(c)′]^{11}

[S′ lemma L3.2(c)′: ∀T : ∀R: ∀S: T =^{p} R ˙⇒ (R =^{p} S ˙⇒ T =^{p} S)]

S′ proof of L3.2(c)′:

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: Arbitrary ≫  S  ;
L04: S1′ ≫  R =^{p} T ˙⇒ (R =^{p} S ˙⇒ T =^{p} S)  ;
L05: L3.2(b)′ ≫  T =^{p} R ˙⇒ R =^{p} T  ;
L06: C1.10a ⊳ L05 ⊳ L04 ≫  T =^{p} R ˙⇒ (R =^{p} S ˙⇒ T =^{p} S) □

10[L3.2(b)′ =^{pyk} “lemma prime l three two b”]

11[L3.2(c)′ =^{pyk} “lemma prime l three two c”]

4.3 Lemma L3.2(d)′

[L3.2(d)′]^{12}

[S′ lemma L3.2(d)′: ∀T : ∀R: ∀S: R =^{p} T ˙⇒ (S =^{p} T ˙⇒ R =^{p} S)]

S′ proof of L3.2(d)′:

L01: Arbitrary ≫  T  ;
L02: Arbitrary ≫  R  ;
L03: Arbitrary ≫  S  ;
L04: L3.2(c)′ ≫  R =^{p} T ˙⇒ (T =^{p} S ˙⇒ R =^{p} S)  ;
L05: Tautology1 ⊳ L04 ≫  T =^{p} S ˙⇒ (R =^{p} T ˙⇒ R =^{p} S)  ;
L06: L3.2(b)′ ≫  S =^{p} T ˙⇒ T =^{p} S  ;
L07: C1.10a ⊳ L06 ⊳ L05 ≫  S =^{p} T ˙⇒ (R =^{p} T ˙⇒ R =^{p} S)  ;
L08: Tautology1 ⊳ L07 ≫  R =^{p} T ˙⇒ (S =^{p} T ˙⇒ R =^{p} S) □

4.4 Lemma L3.2(f)′

To prove [L3.2(f)′]^{13} using induction, we will need to prove the base case [L3.2(f)′_{BASE}]^{14} (section 4.4.1) and the induction step [L3.2(f)′_{HYP}]^{15} (section 4.4.2).

[S′ lemma L3.2(f)′: ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ)]

S′ proof of L3.2(f)′:

L01: L3.2(f)′_{BASE} ≫  ˙0 =^{p} ˙0 ˙+ ˙0  ;
L02: L3.2(f)′_{HYP} ≫  ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′)  ;

L03: S9′ ≫ (˙0 =^{p} ˙0 ˙+ ˙0) ˙⇒ (( ˙∀ṫ: (ṫ =^{p}

˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′)) ˙⇒

( ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ))) ;

L04: MP′ ⊳ L03 ⊳ L01 ≫ ( ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p}

˙0 ˙+ ṫ′)) ˙⇒ ( ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ)) ;

L05: MP′ ⊳ L04 ⊳ L02 ≫  ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ)  □

4.4.1 The base case of L3.2(f)′

[S′ lemma L3.2(f)′_{BASE}: ˙0 =^{p} ˙0 ˙+ ˙0]

S′ proof of L3.2(f)′_{BASE}:

L01: S5′ ≫  ˙0 ˙+ ˙0 =^{p} ˙0  ;

12[L3.2(d)′ =^{pyk} “lemma prime l three two d”]

13[L3.2(f)′ =^{pyk} “lemma prime l three two f”]

14[L3.2(f)′_{BASE} =^{pyk} “lemma prime l three two f base”]

15[L3.2(f)′_{HYP} =^{pyk} “lemma prime l three two f hyp”]

L02: L3.2(b)′ ≫  ˙0 ˙+ ˙0 =^{p} ˙0 ˙⇒ ˙0 =^{p} ˙0 ˙+ ˙0  ;
L03: MP′ ⊳ L02 ⊳ L01 ≫  ˙0 =^{p} ˙0 ˙+ ˙0  □

4.4.2 The induction step of L3.2(f)′

[S′ lemma L3.2(f)′_{HYP}: ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′)]

S′ proof of L3.2(f)′_{HYP}:

L01: L1.8 ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ  ;
L02: S6′ ≫  ˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′  ;

L03: A1′ ≫ (˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′) ˙⇒ (ṫ =^{p}

˙0 ˙+ ṫ ˙⇒ (˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′)) ;

L04: MP′ ⊳ L03 ⊳ L02 ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ (˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′) ;
L05: S2′ ≫  ṫ =^{p} (˙0 ˙+ ṫ) ˙⇒ ṫ′ =^{p} (˙0 ˙+ ṫ)′  ;

L06: A1′ ≫ (ṫ =^{p} (˙0 ˙+ ṫ) ˙⇒ ṫ′ =^{p} (˙0 ˙+ ṫ)′) ˙⇒

(ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ (ṫ =^{p} (˙0 ˙+ ṫ) ˙⇒

ṫ′ =^{p} (˙0 ˙+ ṫ)′)) ;

L07: MP′ ⊳ L06 ⊳ L05 ≫

ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ (ṫ =^{p} (˙0 ˙+ ṫ) ˙⇒ ṫ′ =^{p}
(˙0 ˙+ ṫ)′) ;

L08: A2′^{∗} ⊳ L07 ≫ (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ) ˙⇒ (ṫ =^{p}

˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} (˙0 ˙+ ṫ)′) ;

L09: MP′ ⊳ L08 ⊳ L01 ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} (˙0 ˙+ ṫ)′ ;

L10: L3.2(d)′ ≫ ṫ′ =^{p} (˙0 ˙+ ṫ)′ ˙⇒ (˙0 ˙+ ṫ′ =^{p}

(˙0 ˙+ ṫ)′ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′) ;

L11: Hypothesize ⊳ L10 ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ (ṫ′ =^{p} (˙0 ˙+ ṫ)′ ˙⇒

(˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′ ˙⇒ ṫ′ =^{p}

˙0 ˙+ ṫ′)) ;

L12: A2′^{∗} ⊳ L11 ≫ (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} (˙0 ˙+ ṫ)′) ˙⇒

(ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ (˙0 ˙+ ṫ′ =^{p}

(˙0 ˙+ ṫ)′ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′)) ;

L13: MP′ ⊳ L12 ⊳ L09 ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ (˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′ ˙⇒

ṫ′ =^{p} ˙0 ˙+ ṫ′) ;

L14: A2′^{∗} ⊳ L13 ≫ (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p}

(˙0 ˙+ ṫ)′) ˙⇒ (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p}

˙0 ˙+ ṫ′) ;

L15: MP′ ⊳ L14 ⊳ L04 ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′  ;
L16: Gen′ ⊳ L15 ≫  ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′)  □

4.5 Lemma L3.2(g)′

To prove [L3.2(g)′]^{16} using induction, we will need to prove the base case [L3.2(g)′_{BASE}]^{17}(section 4.5.1) and the induction step [L3.2(g)′_{HYP}]^{18}(section 4.5.2).

[S′ lemma L3.2(g)′: ˙∀ṫ: ˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′)]

S′ proof of L3.2(g)′:

L01: L3.2(g)′_{BASE} ≫ ˙∀ṫ: (ṫ′ ˙+ ˙0 =^{p} (ṫ ˙+ ˙0)′) ;

L02: L3.2(g)′_{HYP} ≫ ˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′ ˙⇒

ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′) ;

L03: S9′ ≫ ˙∀ṫ: (ṫ′ ˙+ ˙0 =^{p} (ṫ ˙+ ˙0)′) ˙⇒

( ˙∀ṙ: ((ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ˙⇒

(ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′)) ˙⇒

( ˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′))) ;

L04: MP′ ⊳ L03 ⊳ L01 ≫ ˙∀ṙ: ((ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ˙⇒

(ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′)) ˙⇒

( ˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′)) ;

L05: MP′ ⊳ L04 ⊳ L02 ≫  ˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′)  ;
L06: Gen′ ⊳ L05 ≫  ˙∀ṫ: ˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′)  □

4.5.1 Base case of L3.2(g)′

[S′ lemma L3.2(g)′_{BASE}: ˙∀ṫ: (ṫ′ ˙+ ˙0 =^{p} (ṫ ˙+ ˙0)′)]

S′ proof of L3.2(g)′_{BASE}:

L01: S5′ ≫  ṫ′ ˙+ ˙0 =^{p} ṫ′  ;
L02: S5′ ≫  ṫ ˙+ ˙0 =^{p} ṫ  ;
L03: S2′ ≫  ṫ ˙+ ˙0 =^{p} ṫ ˙⇒ (ṫ ˙+ ˙0)′ =^{p} ṫ′  ;
L04: MP′ ⊳ L03 ⊳ L02 ≫  (ṫ ˙+ ˙0)′ =^{p} ṫ′  ;

L05: L3.2(d)′ ≫ (ṫ′ ˙+ ˙0) =^{p} ṫ′ ˙⇒ ((ṫ ˙+ ˙0)′ =^{p} ṫ′ ˙⇒

(ṫ′ ˙+ ˙0) =^{p} (ṫ ˙+ ˙0)′) ;

L06: MP′ ⊳ L05 ⊳ L01 ≫  {(ṫ ˙+ ˙0)′ =^{p} ṫ′ ˙⇒ (ṫ′ ˙+ ˙0) =^{p} \atop (ṫ ˙+ ˙0)′  ;}
L07: MP′ ⊳ L06 ⊳ L04 ≫  ṫ′ ˙+ ˙0 =^{p} (ṫ ˙+ ˙0)′  ;
L08: Gen′ ⊳ L07 ≫  ˙∀ṫ: (ṫ′ ˙+ ˙0 =^{p} (ṫ ˙+ ˙0)′)  □

16[L3.2(g)′ =^{pyk} “lemma prime l three two g”]

17[L3.2(g)′_{BASE} =^{pyk} “lemma prime l three two g”]

18[L3.2(g)′_{HYP} =^{pyk} “lemma prime l three two g hyp”]

4.5.2 Induction step of L3.2(g)′

[S′ lemma L3.2(g)′_{HYP}: ˙∀ṙ: ((ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ˙⇒ (ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′))]

S′ proof of L3.2(g)′_{HYP}:

L01: Local ≫  H = ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′  ;
L02: L1.8 ≫  H ˙⇒ H  ;
L03: S6′ ≫  ṫ′ ˙+ ṙ′ =^{p} (ṫ′ ˙+ ṙ)′  ;
L04: A1′^{∗} ⊳ L03 ≫  H ˙⇒ ṫ′ ˙+ ṙ′ =^{p} (ṫ′ ˙+ ṙ)′  ;

L05: S2′ ≫

ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′ ˙⇒ (ṫ′ ˙+ ṙ)′ =^{p}
((ṫ ˙+ ṙ)′)′ ;

L06: A1′^{∗} ⊳ L05 ≫ H ˙⇒ (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′ ˙⇒

(ṫ′ ˙+ ṙ)′ =^{p} ((ṫ ˙+ ṙ)′)′) ;

L07: A2′^{∗} ⊳ L06 ≫ (H ˙⇒ ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ˙⇒

(H ˙⇒ (ṫ′ ˙+ ṙ)′ =^{p} ((ṫ ˙+ ṙ)′)′) ;

L08: MP′ ⊳ L07 ⊳ L02 ≫ H ˙⇒ (ṫ′ ˙+ ṙ)′ =^{p} ((ṫ ˙+ ṙ)′)′ ;

L09: L3.2(c)′ ≫ ṫ′ ˙+ ṙ′ =^{p} (ṫ′ ˙+ ṙ)′ ˙⇒ ((ṫ′ ˙+ ṙ)′ =^{p}

((ṫ ˙+ ṙ)′)′ ˙⇒ ṫ′ ˙+ ṙ′ =^{p}

((ṫ ˙+ ṙ)′)′) ;

L10: A1′^{∗} ⊳ L09 ≫ H ˙⇒ (ṫ′ ˙+ ṙ′ =^{p} (ṫ′ ˙+ ṙ)′ ˙⇒

((ṫ′ ˙+ ṙ)′ =^{p} ((ṫ ˙+ ṙ)′)′ ˙⇒

ṫ′ ˙+ ṙ′ =^{p} ((ṫ ˙+ ṙ)′)′)) ;

L11: A2′^{∗} ⊳ L10 ≫ (H ˙⇒ ṫ′ ˙+ ṙ′ =^{p} (ṫ′ ˙+ ṙ)′) ˙⇒

(H ˙⇒ ((ṫ′ ˙+ ṙ)′ =^{p} ((ṫ ˙+ ṙ)′)′ ˙⇒

ṫ′ ˙+ ṙ′ =^{p} ((ṫ ˙+ ṙ)′)′)) ;

L12: MP′ ⊳ L11 ⊳ L04 ≫ H ˙⇒ ((ṫ′ ˙+ ṙ)′ =^{p} ((ṫ ˙+ ṙ)′)′ ˙⇒

ṫ′ ˙+ ṙ′ =^{p} ((ṫ ˙+ ṙ)′)′) ;

L13: A2′^{∗} ⊳ L12 ≫ (H ˙⇒ (ṫ′ ˙+ ṙ)′ =^{p} ((ṫ ˙+ ṙ)′)′) ˙⇒

(H ˙⇒ ṫ′ ˙+ ṙ′ =^{p} ((ṫ ˙+ ṙ)′)′) ;

L14: MP′ ⊳ L13 ⊳ L08 ≫  H ˙⇒ ṫ′ ˙+ ṙ′ =^{p} ((ṫ ˙+ ṙ)′)′  ;
L15: S6′ ≫  ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′  ;
L16: A1′^{∗} ⊳ L15 ≫  H ˙⇒ ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′  ;

L17: S2′ ≫

ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′ ˙⇒ (ṫ ˙+ ṙ′)′ =^{p}
((ṫ ˙+ ṙ)′)′ ;

L18: A1′^{∗} ⊳ L17 ≫ H ˙⇒ (ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′ ˙⇒

(ṫ ˙+ ṙ′)′ =^{p} ((ṫ ˙+ ṙ)′)′) ;

L19: A2′^{∗} ≫ (H ˙⇒ ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′) ˙⇒

(H ˙⇒ (ṫ ˙+ ṙ′)′ =^{p} ((ṫ ˙+ ṙ)′)′) ;

L20: MP′ ⊳ L19 ⊳ L16 ≫  H ˙⇒ (ṫ ˙+ ṙ′)′ =^{p} ((ṫ ˙+ ṙ)′)′  ;

L21: L3.2(d)′ ≫

ṫ′ ˙+ ṙ′  =^{p} ((ṫ ˙+ ṙ)′)′  ˙⇒

((ṫ ˙+ ṙ′)′ =^{p} ((ṫ ˙+ ṙ)′)′ ˙⇒

ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′) ;

L22: A1′^{∗} ⊳ L21 ≫ H ˙⇒ (ṫ′ ˙+ ṙ′ =^{p} ((ṫ ˙+ ṙ)′)′ ˙⇒

((ṫ ˙+ ṙ′)′ =^{p} ((ṫ ˙+ ṙ)′)′ ˙⇒

ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′)) ;

L23: A2′^{∗} ⊳ L22 ≫ (H ˙⇒ ṫ′ ˙+ ṙ′ =^{p} ((ṫ ˙+ ṙ)′)′) ˙⇒

(H ˙⇒ ((ṫ ˙+ ṙ′)′ =^{p} ((ṫ ˙+ ṙ)′)′ ˙⇒

ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′)) ;

L24: MP′ ⊳ L23 ⊳ L14 ≫ H ˙⇒ ((ṫ ˙+ ṙ′)′ =^{p} ((ṫ ˙+ ṙ)′)′ ˙⇒

ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′) ;

L25: A2′^{∗} ⊳ L24 ≫ (H ˙⇒ (ṫ ˙+ ṙ′)′ =^{p} ((ṫ ˙+ ṙ)′)′) ˙⇒

(H ˙⇒ ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′) ;

L26: MP′ ⊳ L25 ⊳ L20 ≫  H ˙⇒ ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′  ;
L27: Gen′ ⊳ L26 ≫  ˙∀ṙ: (H ˙⇒ ṫ′ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ′)′)  □

4.6 Lemma L3.2(h)′

To prove [L3.2(h)′]^{19} using induction, we will need to prove the base case [L3.2(h)′_{BASE}]^{20}(section 4.6.1) and the induction step [L3.2(h)′_{HYP}]^{21}(section 4.6.2).

[S′ lemma L3.2(h)′: ˙∀ṫ: ˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ)]

S′ proof of L3.2(h)′:

L01: L3.2(h)′_{BASE} ≫ ˙∀ṫ: (ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ) ;

L02: L3.2(h)′_{HYP} ≫

˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p}
ṙ′ ˙+ ṫ) ;

L03: S9′ ≫ ˙∀ṫ: (ṫ ˙+ ˙0 =^{p}  ˙0 ˙+ ṫ) ˙⇒

(( ˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p}
ṙ′ ˙+ ṫ)) ˙⇒ ˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ)) ;

L04: MP′ ⊳ L03 ⊳ L01 ≫

˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p}
ṙ′ ˙+ ṫ) ˙⇒ ˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ) ;
L05: MP′ ⊳ L04 ⊳ L02 ≫  ˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ)  ;
L06: Gen′ ⊳ L05 ≫  ˙∀ṫ: ˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ)  □

19[L3.2(h)′ =^{pyk} “lemma prime l three two h”]

20[L3.2(h)′_{BASE} =^{pyk} “lemma prime l three two h base”]

21[L3.2(h)′_{HYP} =^{pyk} “lemma prime l three two h hyp”]

4.6.1 Base case of L3.2(h)′

[S′ lemma L3.2(h)′_{BASE}: ˙∀ṫ: (ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ)] S′ proof of L3.2(h)′_{BASE}:

L01: S5′ ≫  ṫ ˙+ ˙0 =^{p} ṫ  ;
L02: L3.2(f)′ ≫  ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ)  ;
L03: A4′ @ ṫ ≫  ( ˙∀ṫ: (ṫ =^{p} ˙0 ˙+ ṫ)) ˙⇒ (ṫ =^{p} ˙0 ˙+ ṫ) ;
L04: MP′ ⊳ L03 ⊳ L02 ≫ ṫ =^{p} ˙0 ˙+ ṫ ;

L05: L3.2(c)′ ≫ ṫ ˙+ ˙0 =^{p} ṫ ˙⇒ (ṫ =^{p} ˙0 ˙+ ṫ ˙⇒

ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ) ;

L06: MP′ ⊳ L05 ⊳ L01 ≫  ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ  ;
L07: MP′ ⊳ L06 ⊳ L04 ≫  ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ  ;
L08: Gen′ ⊳ L07 ≫  ˙∀ṫ: (ṫ ˙+ ˙0 =^{p} ˙0 ˙+ ṫ)  □

4.6.2 Induction step of L3.2(h)′ For proving the induction step, we will need the lemma [L3.2h_{SWAP}]^{22}.

[S′ lemma L3.2h_{SWAP}: ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′ ⊢ ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′] S′ proof of L3.2h_{SWAP}:

L01: Premise ≫  ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′  ;
L02: Gen′ ⊳ L01 ≫  ˙∀ṫ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′)  ;

L03: A4′ @ q̇ ≫ ˙∀ṫ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ˙⇒

q̇′ ˙+ ṙ =^{p} (q̇ ˙+ ṙ)′ ;

L04: MP′ ⊳ L03 ⊳ L02 ≫  q̇′ ˙+ ṙ =^{p} (q̇ ˙+ ṙ)′  ;
L05: Gen′ ⊳ L04 ≫  ˙∀ṙ: (q̇′ ˙+ ṙ =^{p} (q̇ ˙+ ṙ)′)  ;

L06: A4′ @ ṫ ≫ ˙∀ṙ: (q̇′ ˙+ ṙ =^{p} (q̇ ˙+ ṙ)′) ˙⇒

q̇′ ˙+ ṫ =^{p} (q̇ ˙+ ṫ)′ ;

L07: MP′ ⊳ L06 ⊳ L05 ≫  q̇′ ˙+ ṫ =^{p} (q̇ ˙+ ṫ)′  ;
L08: Gen′ ⊳ L07 ≫  ˙∀q̇: (q̇′ ˙+ ṫ =^{p} (q̇ ˙+ ṫ)′)  ;

L09: A4′ @ ṙ ≫ ˙∀q̇: (q̇′ ˙+ ṫ =^{p} (q̇ ˙+ ṫ)′) ˙⇒

ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ;

L10: MP′ ⊳ L09 ⊳ L08 ≫ ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ □

Now we are ready to prove the induction step.

[S′ lemma L3.2(h)′_{HYP}: ˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ)] S′ proof of L3.2(h)′_{HYP}:

22[L3.2h_{SWAP} =^{pyk} “lemma prime l three two h hyp”]

L01: Local ≫  H = ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ  ;
L02: L1.8 ≫  H ˙⇒ H  ;
L03: S6′ ≫  ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′  ;
L04: A1′^{∗} ⊳ L03 ≫  H ˙⇒ ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′  ;

L05: S2′ ≫

ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ ˙⇒ (ṫ ˙+ ṙ)′ =^{p}
(ṙ ˙+ ṫ)′ ;

L06: DoubleHypothesis ⊳ L05 ≫ (H ˙⇒ ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ) ˙⇒ (H ˙⇒

((ṫ ˙+ ṙ)′ =^{p} (ṙ ˙+ ṫ)′)) ;

L06: MP′ ⊳ L06 ⊳ L02 ≫ H ˙⇒ ((ṫ ˙+ ṙ)′ =^{p} (ṙ ˙+ ṫ)′) ;

L07: L3.2(c)′ ≫ ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′ ˙⇒ ((ṫ ˙+ ṙ)′ =^{p}

(ṙ ˙+ ṫ)′ ˙⇒ ṫ ˙+ ṙ′ =^{p} (ṙ ˙+ ṫ)′) ;

L08: DoubleHypothesis ⊳ L07 ≫ (H ˙⇒ ṫ ˙+ ṙ′ =^{p} (ṫ ˙+ ṙ)′) ˙⇒

(H ˙⇒ ((ṫ ˙+ ṙ)′ =^{p} (ṙ ˙+ ṫ)′ ˙⇒

ṫ ˙+ ṙ′ =^{p} (ṙ ˙+ ṫ)′)) ;

L09: MP′ ⊳ L08 ⊳ L04 ≫ H ˙⇒ ((ṫ ˙+ ṙ)′ =^{p} (ṙ ˙+ ṫ)′ ˙⇒

ṫ ˙+ ṙ′ =^{p} (ṙ ˙+ ṫ)′) ;

L10: A2′^{∗} ⊳ L09 ≫ (H ˙⇒ (ṫ ˙+ ṙ)′ =^{p} (ṙ ˙+ ṫ)′) ˙⇒

(H ˙⇒ ṫ ˙+ ṙ′ =^{p} (ṙ ˙+ ṫ)′) ;

L11: MP′ ⊳ L10 ⊳ L06 ≫ H ˙⇒ ṫ ˙+ ṙ′ =^{p} (ṙ ˙+ ṫ)′ ;

L12: L3.2(d)′ ≫ ṫ ˙+ ṙ′ =^{p} (ṙ ˙+ ṫ)′ ˙⇒ (ṙ′ ˙+ ṫ =^{p}

(ṙ ˙+ ṫ)′ ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ) ;

L13: DoubleHypothesis ⊳ L12 ≫ (H ˙⇒ ṫ ˙+ ṙ′ =^{p} (ṙ ˙+ ṫ)′) ˙⇒

(H ˙⇒ (ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒

ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ)) ;

L14: MP′ ⊳ L13 ⊳ L11 ≫ H ˙⇒ (ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′ ˙⇒

ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ) ;

L15: L3.2(g)′ ≫ ˙∀ṫ: ˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ;

L16: A4′ @ ṫ ≫ ˙∀ṫ: ˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ˙⇒

˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ;

L16: A4′ @ ṫ ≫ ˙∀ṫ: ˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ˙⇒

˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ;

L17: MP′ ⊳ L16 ⊳ L15 ≫ ˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ;

L18: A4′ @ ṙ ≫ ˙∀ṙ: (ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ˙⇒

(ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′) ;

L19: MP′ ⊳ L18 ⊳ L17 ≫  ṫ′ ˙+ ṙ =^{p} (ṫ ˙+ ṙ)′  ;
L20: L3.2h_{SWAP} ⊳ L19 ≫  ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′  ;
L21: A1′^{∗} ⊳ L20 ≫  H ˙⇒ ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′  ;

L22: A2′^{∗} ⊳ L14 ≫ (H ˙⇒ ṙ′ ˙+ ṫ =^{p} (ṙ ˙+ ṫ)′) ˙⇒

(H ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ) ;

L23: MP′ ⊳ L22 ⊳ L21 ≫  H ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ  ;
L24: Gen′ ⊳ L23 ≫  ˙∀ṙ: (H ˙⇒ ṫ ˙+ ṙ′ =^{p} ṙ′ ˙+ ṫ)  □

5 Conclusion

We have now successfully proved the lemma:

[S′ lemma L3.2(h)′: ˙∀ṫ: ˙∀ṙ: (ṫ ˙+ ṙ =^{p} ṙ ˙+ ṫ)]

In retrospect some of the proofs could have been made shorter/simpler, but this does not alter the fact that the LogiWeb system has verified that this text is correct.

A The name of the page

This defines the name of the page:

[logik rapport =^{pyk} “logik rapport”]

B The Bibliography References

[Mendelson, 2001] E. Mendelson, Introduction to Mathematical Logic, fourth edition. Chapman and Hall 2001.