Peano arithmetic

Klaus Grue

GRD-2005-06-22.UTC:11:16:56.809226

Contents

1 Peano arithmetic 2 1.1 The constructs of Peano arithmetic . . . . . . . . . . . . . . . . . 2 1.2 Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 Mendelsons system S . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.4 A lemma and a proof . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.5 An alternative axiomatic system . . . . . . . . . . . . . . . . . . 7 1.6 Restatement of lemma and proof . . . . . . . . . . . . . . . . . . 9

2 Formal development 9

2.1 Propositional calculus . . . . . . . . . . . . . . . . . . . . . . . . 9 2.1.1 Modus ponens . . . . . . . . . . . . . . . . . . . . . . . . 9 2.1.2 Lemma M1.7 . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.1.3 Hypothetical modus ponens . . . . . . . . . . . . . . . . . 9 2.1.4 Turning lemmas to hypothetical lemmas . . . . . . . . . . 10

2.2 First order predicate calculus . . . . . . . . . . . . . . . . . . . . 10

2.2.1 Hypothetical generalization . . . . . . . . . . . . . . . . . 10 2.3 Peano arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

2.3.1 Lemma M3.2(a) . . . . . . . . . . . . . . . . . . . . . . . 10 2.3.2 Lemma M3.2(b) . . . . . . . . . . . . . . . . . . . . . . . 11 2.3.3 Lemma M3.1(S1) . . . . . . . . . . . . . . . . . . . . . . . 11 2.3.4 Lemma M3.2(c) . . . . . . . . . . . . . . . . . . . . . . . . 11 2.3.5 Lemma M3.1(S2) . . . . . . . . . . . . . . . . . . . . . . . 11 2.3.6 Lemma M3.1(S5) . . . . . . . . . . . . . . . . . . . . . . . 11 2.3.7 Lemma M3.1(S6) . . . . . . . . . . . . . . . . . . . . . . . 12 2.3.8 Lemma M3.2(f) . . . . . . . . . . . . . . . . . . . . . . . . 12

A Chores 12 A.1 The name of the page . . . . . . . . . . . . . . . . . . . . . . . . 12 A.2 Variables of Peano arithmetic . . . . . . . . . . . . . . . . . . . . 12 A.3 TEX definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 A.4 Test . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 A.5 Priority table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 B Index 17

C Bibliography 17

1 Peano arithmetic

This Logiweb page [1] defines Peano arithmetic.

1.1 The constructs of Peano arithmetic

Terms of Peano arithmetic are constructed from zero [˙0 →^{pyk} “peano

zero”][˙0 →^{tex} “

\dot{0}”], successor [x′ →^{pyk} “∗ peano succ”][x′ →^{tex} “#1.’”], plus [x ˙+ y →^{pyk} “∗ peano plus ∗”][x ˙+ y →^{tex} “#1. \mathop{\dot{+}} #2.”], and times [x ˙· y →^{pyk} “∗ peano times ∗”][x ˙· y →^{tex} “#1. \mathop{\dot{\cdot}} #2.”]. Formulas of Peano arithmeric are constructed from equality [x =^{p} y →^{pyk} “∗ peano is ∗”][x =^{p} y →^{tex} “#1. \stackrel{p}{=} #2.”], negation [ ˙¬ x →^{pyk} “peano not ∗”][ ˙¬ x →^{tex} “ \dot{\neg}\, {#1.}”], implication [x ˙⇒ y →^{pyk} “∗ peano imply

∗”][x ˙⇒ y →^{tex} “#1.

\mathrel{\dot{\Rightarrow}} #2.”], and universal quantification [ ˙∀x: y →^{pyk} “peano all ∗ indeed ∗”][ ˙∀x: y →^{tex} “ \dot{\forall} #1. \colon #2.”]. From these constructs we macro define one [˙1 →^{pyk} “peano one”][˙1 →^{tex} “ \dot{1}”], two [˙2 →^{pyk} “peano two”][˙2 →^{tex} “ \dot{2}”], conjunction [x ˙∧ y →^{pyk} “∗ peano and ∗”][x ˙∧ y →^{tex} “#1. \mathrel{\dot{\wedge}} #2.”], disjunction [x ˙∨ y →^{pyk} “∗ peano or

∗”][x ˙∨ y →^{tex} “#1.

\mathrel{\dot{\vee}} #2.”], biimplication [x ˙⇔ y →^{pyk} “∗ peano iff

∗”][x ˙⇔ y →^{tex} “#1.

\mathrel{\dot{\Leftrightarrow}} #2.”], and existential quantification [ ˙∃x: y →^{pyk} “peano exist ∗ indeed ∗”][ ˙∃x: y →^{tex} “ \dot{\exists} #1. \colon #2.”]:

[˙1 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[˙1 ¨= ˙0′]⌉)]
[˙2 →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[˙2 ¨= ˙1′]⌉)]

[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 ¨= ˙¬ x ˙⇒ y]⌉)]
[x ˙⇔ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ˙⇔ y ¨= (x ˙⇒ y) ˙∧ (y ˙⇒ x)]⌉)]
[ ˙∃x: y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ ˙∃x: y ¨= ˙¬ ˙∀x: ˙¬ y]⌉)]

1.2 Variables

We now introduce the unary operator [ẋ →^{pyk} “∗ peano var”][ẋ →^{tex} “ \dot{#1. }”] and define that a term is a Peano variable (i.e. a variable of Peano arithmetic) if it has the [ẋ] operator in its root. [x^{P} →^{pyk} “∗ is peano

var”][x^{P} →^{tex} “#1.

{} ˆ {\cal P}”] is true if [x] is a Peano variable:

[x^{P} →^{val} x =^{r} ⌈ẋ⌉]

We macro define [ȧ →^{pyk} “peano a”][ȧ →^{tex} “ \dot{\mathit{a}}”] to be a Peano variable:

[ȧ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ȧ ¨= ȧ]⌉)]

Appendix A.2 defines Peano variables for the other letters of the English alphabet. [ṅonfree(x, y) →^{pyk} “peano nonfree ∗ in ∗ end nonfree”][ṅonfree(x, y) →^{tex} “ \dot{nonfree}(#1. , #2. )”] is true if the Peano variable [x] does not occur free in the Peano term/formula [y]. [ṅonfree^{∗}(x, y) →^{pyk} “peano nonfree star ∗ in ∗ end nonfree”][ṅonfree^{∗}(x, y) →^{tex} “ \dot{nonfree}ˆ ∗(#1. , #2. )”] is true if the Peano variable [x] does not occur free in the list [y] of Peano terms/formulas.

[ṅonfree(x, y) →^{val}

If(y^{P}, ¬x =^{t} y,

If(¬y =^{r} ⌈ ˙∀x: y⌉, ṅonfree^{∗}(x, y^{t}), If(x =^{t} y^{1}, T, ṅonfree(x, y^{2}))))]

[ṅonfree^{∗}(x, y) →^{val} x!If(y, T, If(ṅonfree(x, y^{h}), ṅonfree^{∗}(x, y^{t}), F))] [ḟree⟨a|x := b⟩ →^{pyk} “peano free ∗ set ∗ to ∗ end free”][ḟree⟨a|x := b⟩ →^{tex} “ \dot{free}\langle #1. | #2. := #3. \rangle”] is true if the substitution [⟨a |x:= b⟩] is free. [ḟree^{∗}⟨a|x := b⟩ →^{pyk} “peano free star ∗ set ∗ to ∗ end free”][ḟree^{∗}⟨a|x := b⟩ →^{tex} “ \dot{free}{}ˆ ∗\langle #1. | #2. := #3. \rangle”] is the version where [a] is a list of terms.

[ḟree⟨a|x := b⟩ →^{val} x!b!

If(a^{P}, T,

If(¬a =^{r} ⌈ ˙∀u: v⌉, ḟree^{∗}⟨a^{t}|x := b⟩,

If(a^{1} =^{t} x, T,

If(ṅonfree(x, a^{2}), T, If(¬ṅonfree(a^{1}, b), F, ḟree⟨a^{2}|x := b⟩)))))]

[ḟree^{∗}⟨a|x := b⟩ →^{val} x!b!If(a, T, If(ḟree⟨a^{h}|x := b⟩, ḟree^{∗}⟨a^{t}|x := b⟩, F))]

[a≡⟨b|x := c⟩ →^{pyk} “peano sub ∗ is ∗ where ∗ is ∗ end sub”][a≡⟨b|x := c⟩ →^{tex} “#1. {\equiv}\langle #2. |#3. :=#4. \rangle”] is true if [a] equals [⟨b |x:= c⟩]. [a≡⟨^{∗}b|x := c⟩ →^{pyk} “peano sub star ∗ is ∗ where ∗ is ∗ end sub”][a≡⟨^{∗}b|x := c⟩ →^{tex} “#1. {\equiv}\langleˆ ∗ #2. |#3. :=#4. \rangle”] is the version where [a] and [b] are lists.

[a≡⟨b|x := c⟩ →^{val} a!x!c!
If(If(b =^{r} ⌈ ˙∀u: v⌉, b^{1} =^{t} x, F), a =^{t} b,
If(b^{P} ∧ b =^{t} x, a =^{t} c, If(
a =^{r} b, a^{t}≡⟨^{∗}b^{t}|x := c⟩, F)))]
[a≡⟨^{∗}b|x := c⟩ →^{val} b!x!c!If(a, T, If(a^{h}≡⟨b^{h}|x := c⟩, a^{t}≡⟨^{∗}b^{t}|x := c⟩, F))]

1.3 Mendelsons system S

System [S →^{pyk} “system s”][S →^{tex} “ S”] of Mendelson [2] expresses Peano arithmetic. It comprises the axioms [A1 →^{pyk} “axiom a one”][A1 →^{tex} “ A1”], [A2 →^{pyk} “axiom a two”][A2 →^{tex} “ A2”], [A3 →^{pyk} “axiom a three”][A3 →^{tex} “ A3”], [A4 →^{pyk} “axiom a four”][A4 →^{tex} “ A4”], and [A5 →^{pyk} “axiom a five”][A5 →^{tex} “ A5”] and inference rules [MP →^{pyk} “rule mp”][MP →^{tex} “ MP”] and [Gen →^{pyk} “rule gen”][Gen →^{tex} “ Gen”] of first order predicate calculus. Furthermore, it comprises the proper axioms [S1 →^{pyk} “axiom s one”][S1 →^{tex} “ S1”], [S2 →^{pyk} “axiom s two”][S2 →^{tex} “ S2”], [S3 →^{pyk} “axiom s three”][S3 →^{tex} “ S3”], [S4 →^{pyk} “axiom s four”][S4 →^{tex} “ S4”], [S5 →^{pyk} “axiom s five”][S5 →^{tex} “ S5”], [S6 →^{pyk} “axiom s six”][S6 →^{tex} “ S6”], [S7 →^{pyk} “axiom s seven”][S7 →^{tex} “ S7”], [S8 →^{pyk} “axiom s eight”][S8 →^{tex} “ S8”], and [S9 →^{pyk} “axiom s nine”][S9 →^{tex} “ S9”]. System [S] is defined thus:

[S →^{stmt} ȧ ˙+ ḃ′ =^{p} ȧ ˙+ ḃ′ ⊕ ∀\underline{a}: ∀\underline{b}: ˙¬ \underline{b} ˙⇒ ˙¬ \underline{a} ˙⇒ ˙¬ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b} ⊕ ȧ =^{p} ḃ ˙⇒ ȧ′ =^{p} ḃ′ ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙⇒ \underline{b} ⊢ \underline{a} ⊢ \underline{b} ⊕ ȧ′ =^{p} ḃ′ ˙⇒ ȧ =^{p} ḃ ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ⊕ ∀\underline{x}: ∀\underline{a}: ∀\underline{b}: ṅonfree(\underline{x}, \underline{a}) ⊢⊢ ˙∀\underline{x}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ ˙∀\underline{x}: \underline{b} ⊕ ȧ ˙· ḃ′ =^{p} ȧ ˙· ḃ ˙+ ȧ ⊕ ȧ ˙+ ˙0 =^{p} ȧ ⊕ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c} ⊕ ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ċ ˙⇒ ḃ =^{p} ċ ⊕ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{x}: \underline{b}≡⟨\underline{a}|\underline{x} := ˙0⟩ ⊢⊢ \underline{c}≡⟨\underline{a}|\underline{x} := \underline{x}′⟩ ⊢⊢ \underline{b} ˙⇒ ˙∀\underline{x}: \underline{a} ˙⇒ \underline{c} ˙⇒

˙∀\underline{x}: \underline{a} ⊕ ¬˙0 =^{p} ȧ′ ⊕ ∀\underline{x}: ∀\underline{a}: \underline{a} ⊢ ˙∀\underline{x}: \underline{a} ⊕ ∀\underline{c}: ∀\underline{a}: ∀\underline{x}: ∀\underline{b}: ⌈\underline{a}⌉≡⟨⌈\underline{b}⌉|⌈\underline{x}⌉ := ⌈\underline{c}⌉⟩ ⊢⊢

˙∀\underline{x}: \underline{b} ˙⇒ \underline{a} ⊕ ȧ ˙· ˙0 =^{p} ˙0]

[A1 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a}][A1 →^{proof} Rule tactic]

[A2 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c}][A2 →^{proof} Rule tactic]

[A3 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ \underline{b} ˙⇒ ˙¬ \underline{a} ˙⇒ ˙¬ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b}][A3 →^{proof} Rule tactic]

The order of quantifiers in the following axiom is such that [\underline{c}] which the current conclusion tactic cannot guess comes first. This allows to supply a value for [\underline{c}] without having to supply values for the other meta-variables.

[A4 →^{stmt} S ⊢ ∀\underline{c}: ∀\underline{a}: ∀\underline{x}: ∀\underline{b}: ⌈\underline{a}⌉≡⟨⌈\underline{b}⌉|⌈\underline{x}⌉ := ⌈\underline{c}⌉⟩ ⊢⊢ ˙∀\underline{x}: \underline{b} ˙⇒ \underline{a}][A4 →^{proof} Rule tactic]

[A5 →^{stmt} S ⊢ ∀\underline{x}: ∀\underline{a}: ∀\underline{b}: ṅonfree(\underline{x}, \underline{a}) ⊢⊢ ˙∀\underline{x}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ ˙∀\underline{x}: \underline{b}][A5 →^{proof} Rule tactic]

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

Axiom [S1] to [S8] are stated as Mendelson [2] does. This is done here to test certain parts of the Logiweb system. Serious users of Peano arithmetic are advised to take Mendelson’s Lemma 3.1 as axioms instead.

[S1 →^{stmt} S ⊢ ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ċ ˙⇒ ḃ =^{p} ċ][S1 →^{proof} Rule tactic]
[S2 →^{stmt} S ⊢ ȧ =^{p} ḃ ˙⇒ ȧ′ =^{p} ḃ′][S2 →^{proof} Rule tactic]
[S3 →^{stmt} S ⊢ ¬˙0 =^{p} ȧ′][S3 →^{proof} Rule tactic]
[S4 →^{stmt} S ⊢ ȧ′ =^{p} ḃ′ ˙⇒ ȧ =^{p} ḃ][S4 →^{proof} Rule tactic]
[S5 →^{stmt} S ⊢ ȧ ˙+ ˙0 =^{p} ȧ][S5 →^{proof} Rule tactic]
[S6 →^{stmt} S ⊢ ȧ ˙+ ḃ′ =^{p} ȧ ˙+ ḃ′][S6 →^{proof} Rule tactic]
[S7 →^{stmt} S ⊢ ȧ ˙· ˙0 =^{p} ˙0][S7 →^{proof} Rule tactic]
[S8 →^{stmt} S ⊢ ȧ ˙· ḃ′ =^{p} ȧ ˙· ḃ ˙+ ȧ][S8 →^{proof} Rule tactic]

[S9 →^{stmt} S ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{x}: \underline{b}≡⟨\underline{a}|\underline{x} := ˙0⟩ ⊢⊢ \underline{c}≡⟨\underline{a}|\underline{x} := \underline{x}′⟩ ⊢⊢ \underline{b} ˙⇒ ˙∀\underline{x}: \underline{a} ˙⇒

\underline{c} ˙⇒ ˙∀\underline{x}: \underline{a}][S9 →^{proof} Rule tactic]

1.4 A lemma and a proof

We now prove Lemma [L3.2(a) →^{pyk} “lemma l three two a”][L3.2(a) →^{tex} “ L3.2(a)”] which is an instance of the corresponding proposition in Mendelson [2]:

[L3.2(a) →^{stmt} S ⊢ ẋ =^{p} ẋ]

[L3.2(a) →^{proof} λc.λx.P(⌈S ⊢ S5 ≫ ȧ ˙+ ˙0 =^{p} ȧ; Gen ⊳ ȧ ˙+ ˙0 =^{p} ȧ ≫ ˙∀ȧ: ȧ ˙+ ˙0 =^{p} ȧ; A4 @ ẋ ≫ ˙∀ȧ: ȧ ˙+ ˙0 =^{p} ȧ ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ; MP ⊳ ˙∀ȧ: ȧ ˙+ ˙0 =^{p} ȧ ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ ⊳ ˙∀ȧ: ȧ ˙+ ˙0 =^{p} ȧ ≫ ẋ ˙+ ˙0 =^{p} ẋ; S1 ≫ ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ċ ˙⇒ ḃ =^{p} ċ; Gen ⊳ ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ċ ˙⇒ ḃ =^{p} ċ ≫ ˙∀ċ: ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ċ ˙⇒ ḃ =^{p} ċ; A4 @ ẋ ≫ ˙∀ċ: ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ċ ˙⇒ ḃ =^{p} ċ ˙⇒ ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ẋ ˙⇒ ḃ =^{p} ẋ; MP ⊳ ˙∀ċ: ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ċ ˙⇒ ḃ =^{p} ċ ˙⇒ ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ẋ ˙⇒ ḃ =^{p} ẋ ⊳ ˙∀ċ: ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ċ ˙⇒ ḃ =^{p} ċ ≫ ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ẋ ˙⇒ ḃ =^{p} ẋ; Gen ⊳ ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ẋ ˙⇒ ḃ =^{p} ẋ ≫ ˙∀ḃ: ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ẋ ˙⇒ ḃ =^{p} ẋ; A4 @ ẋ ≫ ˙∀ḃ: ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ẋ ˙⇒ ḃ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ẋ =^{p} ẋ; MP ⊳ ˙∀ḃ: ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ẋ ˙⇒ ḃ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ẋ =^{p} ẋ ⊳ ˙∀ḃ: ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ẋ ˙⇒ ḃ =^{p} ẋ ≫ ȧ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ẋ =^{p} ẋ; Gen ⊳ ȧ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ẋ =^{p} ẋ ≫ ˙∀ȧ: ȧ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ẋ =^{p} ẋ; A4 @ ẋ ˙+ ˙0 ≫ ˙∀ȧ: ȧ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ẋ =^{p} ẋ ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ =^{p} ẋ; MP ⊳ ˙∀ȧ: ȧ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ẋ =^{p} ẋ ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ =^{p} ẋ ⊳ ˙∀ȧ: ȧ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ẋ =^{p} ẋ ≫ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ =^{p} ẋ; MP ⊳ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ =^{p} ẋ ⊳ ẋ ˙+ ˙0 =^{p} ẋ ≫ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ =^{p} ẋ; MP ⊳ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ =^{p} ẋ ⊳ ẋ ˙+ ˙0 =^{p} ẋ ≫ ẋ =^{p} ẋ⌉, p_{0}, c)]

1.5 An alternative axiomatic system

System [S′ →^{pyk} “system prime s”][S′ →^{tex} “ S’”] is system [S] in which the proper axioms are taken from Lemma 3.1 in Mendelson [2]. It comprises the axioms [A1′ →^{pyk} “axiom prime a one”][A1′ →^{tex} “ A1’”], [A2′ →^{pyk} “axiom prime a two”][A2′ →^{tex} “ A2’”], [A3′ →^{pyk} “axiom prime a three”][A3′ →^{tex} “ A3’”], [A4′ →^{pyk} “axiom prime a four”][A4′ →^{tex} “ A4’”], and [A5′ →^{pyk} “axiom prime a five”][A5′ →^{tex} “ A5’”] and inference rules [MP′ →^{pyk} “rule prime mp”][MP′ →^{tex} “ MP’”] and [Gen′ →^{pyk} “rule prime gen”][Gen′ →^{tex} “ Gen’”] of first order predicate calculus. Furthermore, it comprises the proper axioms [S1′ →^{pyk} “axiom prime s one”][S1′ →^{tex} “ S1’”], [S2′ →^{pyk} “axiom prime s two”][S2′ →^{tex} “ S2’”], [S3′ →^{pyk} “axiom prime s three”][S3′ →^{tex} “ S3’”], [S4′ →^{pyk} “axiom prime s four”][S4′ →^{tex} “ S4’”], [S5′ →^{pyk} “axiom prime s five”][S5′ →^{tex} “ S5’”], [S6′ →^{pyk} “axiom prime s six”][S6′ →^{tex} “ S6’”], [S7′ →^{pyk} “axiom prime s seven”][S7′ →^{tex} “ S7’”], [S8′ →^{pyk} “axiom prime s eight”][S8′ →^{tex} “ S8’”], and [S9′ →^{pyk} “axiom prime s nine”][S9′ →^{tex} “ S9’”]. System [S′] is defined thus:

[S′ →^{stmt} ∀\underline{a}: ∀\underline{b}: \underline{a}′ =^{p} \underline{b}′ ˙⇒ \underline{a} =^{p} \underline{b} ⊕ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{t} =^{p} \underline{s} ⊢

\underline{h} ˙⇒ \underline{r} =^{p} \underline{s} ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ⊕ ∀\underline{x}: ∀\underline{a}: ∀\underline{b}: ṅonfree(⌈\underline{x}⌉, ⌈\underline{a}⌉) ⊢⊢ ˙∀\underline{x}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ ˙∀\underline{x}: \underline{b} ⊕ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: \underline{h} ˙⇒ \underline{t} ˙+ \underline{r}′ =^{p} \underline{t} ˙+ \underline{r}′ ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙· \underline{b}′ =^{p} \underline{a} ˙· \underline{b} ˙+ \underline{a} ⊕

∀\underline{a}: ∀\underline{b}: \underline{a} =^{p} \underline{b} ˙⇒ \underline{a}′ =^{p} \underline{b}′ ⊕ ∀\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{h}: ∀\underline{t}: ∀\underline{r}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{t}′ =^{p} \underline{r}′ ⊕ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙+ \underline{b}′ =^{p}

\underline{a} ˙+ \underline{b}′ ⊕ ∀\underline{a}: ¬˙0 =^{p} \underline{a}′ ⊕ ∀\underline{x}: ∀\underline{a}: \underline{a} ⊢ ˙∀\underline{x}: \underline{a} ⊕ ∀\underline{c}: ∀\underline{a}: ∀\underline{x}: ∀\underline{b}: ⌈\underline{a}⌉≡⟨⌈\underline{b}⌉|⌈\underline{x}⌉ := ⌈\underline{c}⌉⟩ ⊢⊢ ˙∀\underline{x}: \underline{b} ˙⇒ \underline{a} ⊕ ∀\underline{h}: ∀\underline{t}: \underline{h} ˙⇒ \underline{t} ˙+ ˙0 =^{p} \underline{t} ⊕ ∀\underline{a}: \underline{a} ˙· ˙0 =^{p} ˙0 ⊕ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} =^{p} \underline{b} ˙⇒ \underline{a} =^{p} \underline{c} ˙⇒ \underline{b} =^{p} \underline{c} ⊕ ∀\underline{t}: \underline{t} =^{p} \underline{t} ⊕ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{x}: \underline{b}≡⟨\underline{a}|\underline{x} := ˙0⟩ ⊢⊢ \underline{c}≡⟨\underline{a}|\underline{x} := \underline{x}′⟩ ⊢⊢ \underline{b} ˙⇒ ˙∀\underline{x}: \underline{a} ˙⇒ \underline{c} ˙⇒ ˙∀\underline{x}: \underline{a} ⊕ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c} ⊕

∀\underline{h}: ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{r} =^{p} \underline{s} ⊢ \underline{h} ˙⇒ \underline{t} =^{p} \underline{s} ⊕ ∀\underline{a}: \underline{a} ˙+ ˙0 =^{p} \underline{a}]

[A1′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a}][A1′ →^{proof} Rule tactic] [A2′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{c} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{c}][A2′ →^{proof} Rule tactic] [A3′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ˙¬ \underline{b} ˙⇒ ˙¬ \underline{a} ˙⇒ ˙¬ \underline{b} ˙⇒ \underline{a} ˙⇒ \underline{b}][A3′ →^{proof} Rule tactic] [A4′ →^{stmt} S′ ⊢ ∀\underline{c}: ∀\underline{a}: ∀\underline{x}: ∀\underline{b}: ⌈\underline{a}⌉≡⟨⌈\underline{b}⌉|⌈\underline{x}⌉ := ⌈\underline{c}⌉⟩ ⊢⊢ ˙∀\underline{x}: \underline{b} ˙⇒ \underline{a}][A4′ →^{proof} Rule tactic] [A5′ →^{stmt} S′ ⊢ ∀\underline{x}: ∀\underline{a}: ∀\underline{b}: ṅonfree(⌈\underline{x}⌉, ⌈\underline{a}⌉) ⊢⊢ ˙∀\underline{x}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a} ˙⇒ ˙∀\underline{x}: \underline{b}][A5′ →^{proof} Rule tactic] [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] [S1′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: \underline{a} =^{p} \underline{b} ˙⇒ \underline{a} =^{p} \underline{c} ˙⇒ \underline{b} =^{p} \underline{c}][S1′ →^{proof} Rule tactic] [S2′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} =^{p} \underline{b} ˙⇒ \underline{a}′ =^{p} \underline{b}′][S2′ →^{proof} Rule tactic] [S3′ →^{stmt} S′ ⊢ ∀\underline{a}: ¬˙0 =^{p} \underline{a}′][S3′ →^{proof} Rule tactic] [S4′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a}′ =^{p} \underline{b}′ ˙⇒ \underline{a} =^{p} \underline{b}][S4′ →^{proof} Rule tactic] [S5′ →^{stmt} S′ ⊢ ∀\underline{a}: \underline{a} ˙+ ˙0 =^{p} \underline{a}][S5′ →^{proof} Rule tactic] [S6′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙+ \underline{b}′ =^{p} \underline{a} ˙+ \underline{b}′][S6′ →^{proof} Rule tactic] [S7′ →^{stmt} S′ ⊢ ∀\underline{a}: \underline{a} ˙· ˙0 =^{p} ˙0][S7′ →^{proof} Rule tactic] [S8′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙· \underline{b}′ =^{p} \underline{a} ˙· \underline{b} ˙+ \underline{a}][S8′ →^{proof} Rule tactic] [S9′ →^{stmt} S′ ⊢ ∀\underline{a}: ∀\underline{b}: ∀\underline{c}: ∀\underline{x}: \underline{b}≡⟨\underline{a}|\underline{x} := ˙0⟩ ⊢⊢ \underline{c}≡⟨\underline{a}|\underline{x} := \underline{x}′⟩ ⊢⊢ \underline{b} ˙⇒ ˙∀\underline{x}: \underline{a} ˙⇒ \underline{c} ˙⇒ ˙∀\underline{x}: \underline{a}][S9′ →^{proof} Rule tactic]

Note that [A1] and [A1′] are distinct. The former says [S ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a}] and the latter says [S′ ⊢ ∀\underline{a}: ∀\underline{b}: \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{a}].

1.6 Restatement of lemma and proof

We now prove Lemma [L3.2(a)] once again under the name of [L3.2(a)′ →^{pyk} “lemma prime l three two a”][L3.2(a)′ →^{tex} “ L3.2(a)’”]:

[L3.2(a)′ →^{stmt} S′ ⊢ ∀\underline{a}: \underline{a} =^{p} \underline{a}]

[L3.2(a)′ →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{a}: S5′ ≫ \underline{a} ˙+ ˙0 =^{p} \underline{a}; S1′ ≫ \underline{a} ˙+ ˙0 =^{p} \underline{a} ˙⇒ \underline{a} ˙+ ˙0 =^{p} \underline{a} ˙⇒ \underline{a} =^{p} \underline{a}; MP′ ⊳ \underline{a} ˙+ ˙0 =^{p} \underline{a} ˙⇒ \underline{a} ˙+ ˙0 =^{p} \underline{a} ˙⇒ \underline{a} =^{p} \underline{a} ⊳ \underline{a} ˙+ ˙0 =^{p} \underline{a} ≫ \underline{a} ˙+ ˙0 =^{p} \underline{a} ˙⇒ \underline{a} =^{p} \underline{a}; MP′ ⊳ \underline{a} ˙+ ˙0 =^{p} \underline{a} ˙⇒ \underline{a} =^{p} \underline{a} ⊳ \underline{a} ˙+ ˙0 =^{p} \underline{a} ≫ \underline{a} =^{p} \underline{a}⌉, p_{0}, c)]

2 Formal development

2.1 Propositional calculus

2.1.1 Modus ponens

We use [x ⊵ y →^{pyk} “∗ macro modus ponens ∗”][x ⊵ y →^{tex} “#1. \unrhd #2.”] as shorthand for modus ponens:

[x ⊵ y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ⊵ y ¨= MP′ ⊳ x ⊳ y]⌉)]

2.1.2 Lemma M1.7

Lemma [M1.7 →^{pyk} “mendelson one seven”][M1.7 →^{tex} “ M1.7”] (i.e. Lemma 1.7 in Mendelson [2]) reads:

[M1.7 →^{stmt} S′ ⊢ ∀\underline{b}: \underline{b} ˙⇒ \underline{b}]

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

2.1.3 Hypothetical modus ponens

The hypothetical version [MP′_{h} →^{pyk} “hypothetical rule prime mp”][MP′_{h} →^{tex} “ MP’ h”] of modus ponens MP′ has a hypothesis \underline{h} on each premise and on the conclusion:

[MP′_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: \underline{h} ˙⇒ \underline{a} ˙⇒ \underline{b} ⊢ \underline{h} ˙⇒ \underline{a} ⊢ \underline{h} ˙⇒ \underline{b}]

[MP′_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{a}: ∀\underline{b}: \underline{h} ˙⇒ \underline{a} ˙⇒ \underline{b} ⊢ \underline{h} ˙⇒ \underline{a} ⊢ A2′ ≫ \underline{h} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{h} ˙⇒ \underline{a} ˙⇒ \underline{h} ˙⇒ \underline{b}; MP′ ⊳ \underline{h} ˙⇒ \underline{a} ˙⇒ \underline{b} ˙⇒ \underline{h} ˙⇒ \underline{a} ˙⇒ \underline{h} ˙⇒ \underline{b} ⊳ \underline{h} ˙⇒ \underline{a} ˙⇒ \underline{b} ≫ \underline{h} ˙⇒ \underline{a} ˙⇒ \underline{h} ˙⇒ \underline{b}; MP′ ⊳ \underline{h} ˙⇒ \underline{a} ˙⇒ \underline{h} ˙⇒ \underline{b} ⊳ \underline{h} ˙⇒ \underline{a} ≫ \underline{h} ˙⇒ \underline{b}⌉, p_{0}, c)] We use [x ⊵_{h} y →^{pyk} “∗ hypothetical modus ponens ∗”][x ⊵_{h} y →^{tex} “#1. \unrhd h #2.”] as shorthand for hypothetical modus ponens:

[x ⊵_{h} y →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[x ⊵_{h} y ¨= MP′_{h} ⊳ x ⊳ y]⌉)]

2.1.4 Turning lemmas to hypothetical lemmas

Lemma [Hypothesize →^{pyk} “hypothesize”][Hypothesize →^{tex} “ Hypothesize”] turns a lemma with no premises into one that assumes the hypothesis [\underline{h}] to hold:

[Hypothesize →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{a}: \underline{a} ⊢ \underline{h} ˙⇒ \underline{a}]

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

2.2 First order predicate calculus

2.2.1 Hypothetical generalization

The hypothetical version [Gen′_{h} →^{pyk} “hypothetical rule prime gen”][Gen′_{h} →^{tex} “ Gen’ h”] of generalisation Gen′ has a hypothesis \underline{h} on premise and conclusion:

[Gen′_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{x}: ∀\underline{a}: ṅonfree(⌈\underline{x}⌉, ⌈\underline{h}⌉) ⊢⊢ \underline{h} ˙⇒ \underline{a} ⊢ \underline{h} ˙⇒ ˙∀\underline{x}: \underline{a}]

[Gen′_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{x}: ∀\underline{a}: ṅonfree(⌈\underline{x}⌉, ⌈\underline{h}⌉) ⊢⊢ \underline{h} ˙⇒ \underline{a} ⊢ A5′ ⊳ ⊳ ṅonfree(⌈\underline{x}⌉, ⌈\underline{h}⌉) ≫ ˙∀\underline{x}: \underline{h} ˙⇒ \underline{a} ˙⇒ \underline{h} ˙⇒ ˙∀\underline{x}: \underline{a}; Gen′ ⊳ \underline{h} ˙⇒ \underline{a} ≫ ˙∀\underline{x}: \underline{h} ˙⇒ \underline{a}; MP′ ⊳ ˙∀\underline{x}: \underline{h} ˙⇒ \underline{a} ˙⇒ \underline{h} ˙⇒ ˙∀\underline{x}: \underline{a} ⊳ ˙∀\underline{x}: \underline{h} ˙⇒ \underline{a} ≫ \underline{h} ˙⇒ ˙∀\underline{x}: \underline{a}⌉, p_{0}, c)]

2.3 Peano arithmetic

2.3.1 Lemma M3.2(a)

Lemma [M3.2(a) →^{pyk} “mendelson three two a”][M3.2(a) →^{tex} “ M3.2(a)”] and the associated hypothetical lemma [M3.2(a)_{h} →^{pyk} “hypothetical three two a”][M3.2(a)_{h} →^{tex} “ M3.2(a) h”] read:

[M3.2(a) →^{stmt} S′ ⊢ ∀\underline{t}: \underline{t} =^{p} \underline{t}][M3.2(a) →^{proof} Rule tactic]

[M3.2(a)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{t}]

Above we cheat in stating M3.2(a) as a rule and not as a lemma. A reasonable way to construct a large proof is to start stating everything as rules and then changing the rules to lemmas one at a time until only the rules of the theory are left.

[M3.2(a)_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{t}: M3.2(a) ≫ \underline{t} =^{p} \underline{t}; Hypothesize ⊳ \underline{t} =^{p} \underline{t} ≫

\underline{h} ˙⇒ \underline{t} =^{p} \underline{t}⌉, p_{0}, c)]

2.3.2 Lemma M3.2(b)

Lemma [M3.2(b)_{h} →^{pyk} “hypothetical three two b”][M3.2(b)_{h} →^{tex} “ M3.2(b) h”] reads:

[M3.2(b)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{r} =^{p} \underline{t}][M3.2(b)_{h} →^{proof} Rule tactic]

[M3.2(b)_{h} →^{proof} λc.λx.P(⌈S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ S1′ ≫ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t}; Hypothesize⊳\underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ≫ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t}; MP′_{h} ⊳\underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ≫ \underline{h} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t}; M3.2(a)_{h} ≫ \underline{h} ˙⇒ \underline{t} =^{p} \underline{t}; MP′_{h} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{t} ˙⇒ \underline{r} =^{p} \underline{t} ⊳ \underline{h} ˙⇒ \underline{t} =^{p} \underline{t} ≫ \underline{h} ˙⇒ \underline{r} =^{p} \underline{t}⌉, p_{0}, c)]

2.3.3 Lemma M3.1(S1)

Lemma [M3.1(S1′)_{h} →^{pyk} “hypothetical three one s one”][M3.1(S1′)_{h} →^{tex} “ M3.1(S1’) h”] is the hypothetical version of Mendelson Lemma 3.1(S1′):

[M3.1(S1′)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{t} =^{p} \underline{s} ⊢ \underline{h} ˙⇒ \underline{r} =^{p} \underline{s}][M3.1(S1′)_{h} →^{proof} Rule tactic]

2.3.4 Lemma M3.2(c)

Lemma [M3.2(c)_{h} →^{pyk} “hypothetical three two c”][M3.2(c)_{h} →^{tex} “ M3.2(c) h”] is the hypothetical version of Mendelson Lemma 3.2(c) which expresses ordinary transitivity:

[M3.2(c)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: ∀\underline{s}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{r} =^{p} \underline{s} ⊢ \underline{h} ˙⇒ \underline{t} =^{p} \underline{s}][M3.2(c)_{h} →^{proof} Rule tactic]

2.3.5 Lemma M3.1(S2)

Lemma [M3.1(S2′)_{h} →^{pyk} “hypothetical three one s two”][M3.1(S2′)_{h} →^{tex} “ M3.1(S2’) h”] is the hypothetical version of Mendelson Lemma 3.1(S2′):

[M3.1(S2′)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: \underline{h} ˙⇒ \underline{t} =^{p} \underline{r} ⊢ \underline{h} ˙⇒ \underline{t}′ =^{p} \underline{r}′][M3.1(S2′)_{h} →^{proof} Rule tactic]

2.3.6 Lemma M3.1(S5)

Lemma [M3.1(S5′)_{h} →^{pyk} “hypothetical three one s five”][M3.1(S5′)_{h} →^{tex} “ M3.1(S5’) h”] is the hypothetical version of Mendelson Lemma 3.1(S5′):

[M3.1(S5′)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: \underline{h} ˙⇒ \underline{t} ˙+ ˙0 =^{p} \underline{t}][M3.1(S5′)_{h} →^{proof} Rule tactic] 2.3.7 Lemma M3.1(S6)

Lemma [M3.1(S6′)_{h} →^{pyk} “hypothetical three one s six”][M3.1(S6′)_{h} →^{tex} “ M3.1(S6’) h”] is the hypothetical version of Mendelson Lemma 3.1(S6′):

[M3.1(S6′)_{h} →^{stmt} S′ ⊢ ∀\underline{h}: ∀\underline{t}: ∀\underline{r}: \underline{h} ˙⇒ \underline{t} ˙+ \underline{r}′ =^{p} \underline{t} ˙+ \underline{r}′][M3.1(S6′)_{h} →^{proof} Rule tactic]

2.3.8 Lemma M3.2(f)

Lemma [M3.2(f) →^{pyk} “mendelson three two f”][M3.2(f) →^{tex} “ M3.2(f)”] is the closure of Mendelson Lemma 3.2(f) for the concrete variable [ṫ]:

[M3.2(f) →^{stmt} S′ ⊢ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ]

The proof below uses local macro definitions.

[M3.2(f) →^{proof} λc.λx.P(⌈S′ ⊢ A1′ ≫ x ˙⇒ x ˙⇒ x; M3.1(S5′)_{h} ≫ x ˙⇒ x ˙⇒ x ˙⇒ ˙0 ˙+ ˙0 =^{p} ˙0; M3.2(b)_{h} ⊳ x ˙⇒ x ˙⇒ x ˙⇒ ˙0 ˙+ ˙0 =^{p} ˙0 ≫ x ˙⇒ x ˙⇒ x ˙⇒ ˙0 =^{p} ˙0 ˙+ ˙0; MP′ ⊳ x ˙⇒ x ˙⇒ x ˙⇒ ˙0 =^{p} ˙0 ˙+ ˙0 ⊳ x ˙⇒ x ˙⇒ x ≫ ˙0 =^{p} ˙0 ˙+ ˙0; M1.7 ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ; M3.1(S2′)_{h} ⊳ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′; M3.1(S6′)_{h} ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p} ˙0 ˙+ ṫ′; M3.2(b)_{h} ⊳ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p} ˙0 ˙+ ṫ′ ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p} ˙0 ˙+ ṫ′; M3.2(c)_{h} ⊳ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ⊳ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ˙0 ˙+ ṫ′ =^{p} ˙0 ˙+ ṫ′ ≫ ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′; Gen′⊳ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ≫ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′; S9′ ≫ ˙0 =^{p} ˙0 ˙+ ˙0 ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ; MP′ ⊳ ˙0 =^{p} ˙0 ˙+ ˙0 ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ⊳ ˙0 =^{p} ˙0 ˙+ ˙0 ≫ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ; MP′ ⊳ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ˙⇒ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ⊳ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′ ≫ ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ⌉, p_{0}, c)]

A Chores

A.1 The name of the page

This defines the name of the page:

[peano →^{pyk} “peano”]

A.2 Variables of Peano arithmetic

We use [ḃ →^{pyk} “peano b”][ḃ →^{tex} “ \dot{\mathit{b}}”], [ċ →^{pyk} “peano c”][ċ →^{tex} “ \dot{\mathit{c}}”], [ḋ →^{pyk} “peano d”][ḋ →^{tex} “ \dot{\mathit{d}}”], [ė →^{pyk} “peano e”][ė →^{tex} “ \dot{\mathit{e}}”], [ḟ →^{pyk} “peano f”][ḟ →^{tex} “ \dot{\mathit{f}}”], [ġ →^{pyk} “peano g”][ġ →^{tex} “ \dot{\mathit{g}}”], [ḣ →^{pyk} “peano h”][ḣ →^{tex} “ \dot{\mathit{h}}”], [i̇ →^{pyk} “peano i”][i̇ →^{tex} “ \dot{\mathit{i}}”], [j̇ →^{pyk} “peano j”][j̇ →^{tex} “ \dot{\mathit{j}}”], [k̇ →^{pyk} “peano k”][k̇ →^{tex} “ \dot{\mathit{k}}”], [l̇ →^{pyk} “peano l”][l̇ →^{tex} “ \dot{\mathit{l}}”], [ṁ →^{pyk} “peano m”][ṁ →^{tex} “ \dot{\mathit{m}}”], [ṅ →^{pyk} “peano n”][ṅ →^{tex} “ \dot{\mathit{n}}”], [ȯ →^{pyk} “peano o”][ȯ →^{tex} “ \dot{\mathit{o}}”], [ṗ →^{pyk} “peano p”][ṗ →^{tex} “ \dot{\mathit{p}}”], [q̇ →^{pyk} “peano q”][q̇ →^{tex} “ \dot{\mathit{q}}”], [ṙ →^{pyk} “peano r”][ṙ →^{tex} “ \dot{\mathit{r}}”], [ṡ →^{pyk} “peano s”][ṡ →^{tex} “ \dot{\mathit{s}}”], [ṫ →^{pyk} “peano t”][ṫ →^{tex} “ \dot{\mathit{t}}”], [u̇ →^{pyk} “peano u”][u̇ →^{tex} “ \dot{\mathit{u}}”], [v̇ →^{pyk} “peano v”][v̇ →^{tex} “ \dot{\mathit{v}}”], [ẇ →^{pyk} “peano w”][ẇ →^{tex} “ \dot{\mathit{w}}”], [ẋ →^{pyk} “peano x”][ẋ →^{tex} “ \dot{\mathit{x}}”], [ẏ →^{pyk} “peano y”][ẏ →^{tex} “ \dot{\mathit{y}}”], and [ż →^{pyk} “peano z”][ż →^{tex} “ \dot{\mathit{z}}”] to denote variables of Peano arithmetic: [ḃ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ḃ ¨= ḃ]⌉)], [ċ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ċ ¨= ċ]⌉)], [ḋ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ḋ ¨= ḋ]⌉)], [ė →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ė ¨= ė]⌉)], [ḟ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ḟ ¨= ḟ]⌉)], [ġ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ġ ¨= ġ]⌉)], [ḣ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ḣ ¨= ḣ]⌉)], [i̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[i̇ ¨= i̇]⌉)], [j̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[j̇ ¨= j̇]⌉)], [k̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[k̇ ¨= k̇]⌉)], [l̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[l̇ ¨= l̇]⌉)], [ṁ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṁ ¨= ṁ]⌉)], [ṅ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṅ ¨= ṅ]⌉)], [ȯ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ȯ ¨= ȯ]⌉)], [ṗ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṗ ¨= ṗ]⌉)], [q̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[q̇ ¨= q̇]⌉)], [ṙ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṙ ¨= ṙ]⌉)], [ṡ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṡ ¨= ṡ]⌉)], [ṫ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ṫ ¨= ṫ]⌉)], [u̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[u̇ ¨= u̇]⌉)], [v̇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[v̇ ¨= v̇]⌉)], [ẇ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ẇ ¨= ẇ]⌉)], [ẋ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ẋ ¨= ẋ]⌉)], [ẏ →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ẏ ¨= ẏ]⌉)], and [ż →^{macro} λt.λs.λc.M̃_{4}(t, s, c, ⌈[ż ¨= ż]⌉)].

A.3 TEX definitions A.4 Test

[⌈ȧ⌉^{P}]^{·} [⌈a⌉^{P}]^{−} [ṅonfree(⌈ẋ⌉, ⌈ẏ =^{p} ż ˙⇒ ˙∀ẋ: ẋ =^{p} ẏ⌉)]^{·} [ṅonfree(⌈ẋ⌉, ⌈ẋ =^{p} ż ˙⇒ ˙∀ẋ: ẋ =^{p} ẏ⌉)]^{−} [ṅonfree(⌈ẋ⌉, ⌈ẏ =^{p} ẋ ˙⇒ ˙∀ẋ: ẋ =^{p} ẏ⌉)]^{−} [ṅonfree(⌈ẋ⌉, ⌈ẏ =^{p} ż ˙⇒ ˙∀ẏ: ẋ =^{p} ẏ⌉)]^{−} [ḟree⟨⌈ ˙∀ẋ: b : : ẋ : : c⌉|⌈ẋ⌉ := ⌈x : : ẏ : : z⌉⟩]^{·} [ḟree⟨⌈ ˙∀ẏ: b : : ẋ : : c⌉|⌈ẋ⌉ := ⌈x : : ẏ : : z⌉⟩]^{−} [ḟree⟨⌈ ˙∀ẋ: b : : ẋ : : c⌉|⌈ẏ⌉ := ⌈x : : ẏ : : z⌉⟩]^{·} [ḟree⟨⌈ ˙∀ẏ: b : : ẋ : : c⌉|⌈ẏ⌉ := ⌈x : : ẏ : : z⌉⟩]^{·} [ȧ≡⟨ȧ|ḃ := ċ⟩]^{·} [ċ≡⟨ḃ|ḃ := ċ⟩]^{·} [∀ȧ: ȧ =^{p} ḃ≡⟨∀ȧ: ȧ =^{p} ḃ|ȧ := ċ⟩]^{·} [∀ȧ: ȧ =^{p} ċ≡⟨∀ȧ: ȧ =^{p} ḃ|ḃ := ċ⟩]^{·} [ ˙∀ȧ: ȧ =^{p} ˙0 ˙+ ȧ ˙⇒ ċ ˙· ḋ =^{p} ˙0 ˙+ ċ ˙· ḋ≡⟨ ˙∀ȧ: ȧ =^{p} ˙0 ˙+ ȧ ˙⇒ ḃ =^{p} ˙0 ˙+ ḃ|ḃ := ċ ˙· ḋ⟩]^{·} [ ˙∀ȧ: ȧ =^{p} ˙0 ˙+ ȧ ˙⇒ ḃ =^{p} ˙0 ˙+ ḃ≡⟨ ˙∀ȧ: ȧ =^{p} ˙0 ˙+ ȧ ˙⇒ ḃ =^{p} ˙0 ˙+ ḃ|ȧ := ċ⟩]^{·}

A.5 Priority table

[peano →^{prio} Preassociative [peano], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [math ∗ end math], [flush left [∗]], [x], [y], [z], [[∗ ▷◁ ∗]], [[∗ →^{∗} ∗]], [pyk], [tex], [name], [prio], [∗], [T], [if(∗, ∗, ∗)], [[∗ ⇒^{∗} ∗]], [val], [claim], [⊥], [f(∗)], [(∗)^{I}], [F], [\underline{0}], [\underline{1}], [\underline{2}], [\underline{3}], [\underline{4}], [\underline{5}], [\underline{6}], [\underline{7}], [\underline{8}], [\underline{9}], [0], [1], [2], [3], [4], [5], [6], [7], [8], [9], [a], [b], [c], [d], [e], [f], [g], [h], [i], [j], [k], [l], [m], [n], [o], [p], [q], [r], [s], [t], [u], [v], [w], [(∗)^{M}], [If(∗, ∗, ∗)], [array{∗} ∗ end array], [l], [c], [r], [empty], [⟨∗ | ∗:= ∗⟩], [M(∗)], [Ũ(∗)], [U(∗)], [U^{M}(∗)], [apply(∗, ∗)], [apply_{1}(∗, ∗)], [identifier(∗)], [identifier_{1}(∗, ∗)], [arrayplus(∗, ∗)], [array-remove(∗, ∗, ∗)], [array-put(∗, ∗, ∗, ∗)], [array-add(∗, ∗, ∗, ∗, ∗)], [bit(∗, ∗)], [bit_{1}(∗, ∗)], [rack], ["vector"], ["bibliography"], ["dictionary"], ["body"], ["codex"], ["expansion"], ["code"], ["cache"], ["diagnose"], ["pyk"], ["tex"], ["texname"], ["value"], ["message"], ["macro"], ["definition"], ["unpack"], ["claim"], ["priority"], ["lambda"], ["apply"], ["true"], ["if"], ["quote"], ["proclaim"], ["define"], ["introduce"], ["hide"], ["pre"], ["post"], [E(∗, ∗, ∗)], [E_{2}(∗, ∗, ∗, ∗, ∗)], [E_{3}(∗, ∗, ∗, ∗)], [E_{4}(∗, ∗, ∗, ∗)], [lookup(∗, ∗, ∗)], [abstract(∗, ∗, ∗, ∗)], [⌈∗⌉], [M(∗, ∗, ∗)], [M_{2}(∗, ∗, ∗, ∗)], [M^{∗}(∗, ∗, ∗)], [macro], [s_{0}], [zip(∗, ∗)], [assoc_{1}(∗, ∗, ∗)], [(∗)^{p}], [self], [[∗ ¨= ∗]], [[∗ ˙= ∗]], [[∗ ´= ∗]], [[∗ =^{pyk} ∗]], [[∗ =^{tex} ∗]], [[∗ =^{name} ∗]], [Priority table[∗]], [M̃_{1}], [M̃_{2}(∗)], [M̃_{3}(∗)], [M̃_{4}(∗, ∗, ∗, ∗)], [M̃(∗, ∗, ∗)], [Q̃(∗, ∗, ∗)], [Q̃_{2}(∗, ∗, ∗)], [Q̃_{3}(∗, ∗, ∗, ∗)], [Q̃^{∗}(∗, ∗, ∗)], [(∗)], [aspect(∗, ∗)], [aspect(∗, ∗, ∗)], [⟨∗⟩], [tuple_{1}(∗)], [tuple_{2}(∗)], [let_{2}(∗, ∗)], [let_{1}(∗, ∗)], [[∗ =^{claim} ∗]], [checker], [check(∗, ∗)], [check_{2}(∗, ∗, ∗)], [check_{3}(∗, ∗, ∗)], [check^{∗}(∗, ∗)], [check_{2}^{∗}(∗, ∗, ∗)], [[∗]^{·}], [[∗]^{−}], [[∗]^{∘}], [msg], [[∗ =^{msg} ∗]], [<stmt>], [stmt], [[∗ =^{stmt} ∗]], [HeadNil′], [HeadPair′], [Transitivity′], [⊥ ⊥], [Contra′], [T′_{E}], [L_{1}], [\underline{∗}], [A], [B], [C], [D], [E], [F], [G], [H], [I], [J], [K], [L], [M], [N], [O], [P], [Q], [R], [S], [T ], [U], [V], [W], [X], [Y], [Z], [⟨∗ | ∗:= ∗⟩], [⟨^{∗}∗ | ∗:= ∗⟩], [∅], [Remainder], [(∗)^{v}], [intro(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗)], [error(∗, ∗)], [error_{2}(∗, ∗)], [proof(∗, ∗, ∗)], [proof_{2}(∗, ∗)], [S(∗, ∗)], [S^{I}(∗, ∗)], [S^{⊳} (∗, ∗)], [S_{1}^{⊳} (∗, ∗, ∗)], [S^{E}(∗, ∗)], [S_{1}^{E}(∗, ∗, ∗)], [S^{+}(∗, ∗)], [S_{1}^{+}(∗, ∗, ∗)], [S^{−}(∗, ∗)], [S_{1}^{−}(∗, ∗, ∗)], [S^{∗}(∗, ∗)], [S_{1}^{∗}(∗, ∗, ∗)], [S_{2}^{∗}(∗, ∗, ∗, ∗)], [S^{@}(∗, ∗)], [S_{1}^{@}(∗, ∗, ∗)], [S^{⊢}(∗, ∗)], [S_{1}^{⊢}(∗, ∗, ∗, ∗)], [S⊢ ⊢(∗, ∗)],

[S⊢ ⊢ ; 1(∗, ∗, ∗, ∗)], [S^{i.e.}(∗, ∗)], [S_{1}^{i.e.}(∗, ∗, ∗, ∗)], [S_{2}^{i.e.}(∗, ∗, ∗, ∗, ∗)], [S^{∀}(∗, ∗)],

[S_{1}^{∀}(∗, ∗, ∗, ∗)], [S^{;}(∗, ∗)], [S_{1}^{;}(∗, ∗, ∗)], [S_{2}^{;}(∗, ∗, ∗, ∗)], [T (∗)], [claims(∗, ∗, ∗)], [claims_{2}(∗, ∗, ∗)], [<proof>], [proof], [[Lemma ∗: ∗]], [[Proof of ∗: ∗]], [[∗ lemma ∗: ∗]], [[∗ antilemma ∗: ∗]], [[∗ rule ∗: ∗]], [[∗ antirule ∗: ∗]], [verifier], [V_{1}(∗)], [V_{2}(∗, ∗)], [V_{3}(∗, ∗, ∗, ∗)], [V_{4}(∗, ∗)], [V_{5}(∗, ∗, ∗, ∗)], [V_{6}(∗, ∗, ∗, ∗)], [V_{7}(∗, ∗, ∗, ∗)], [Cut(∗, ∗)], [Head_{⊕}(∗)], [Tail_{⊕}(∗)], [rule_{1}(∗, ∗)], [rule(∗, ∗)], [Rule tactic], [Plus(∗, ∗)], [[Theory ∗]], [theory_{2}(∗, ∗)], [theory_{3}(∗, ∗)], [theory_{4}(∗, ∗, ∗)], [HeadNil′′], [HeadPair′′], [Transitivity′′], [Contra′′], [HeadNil], [HeadPair], [Transitivity], [Contra], [T_{E}], [ragged right], [ragged right expansion ], [parm(∗, ∗, ∗)], [parm^{∗}(∗, ∗, ∗)], [inst(∗, ∗)], [inst^{∗}(∗, ∗)], [occur(∗, ∗, ∗)], [occur^{∗}(∗, ∗, ∗)], [unify(∗ = ∗, ∗)], [unify^{∗}(∗ = ∗, ∗)], [unify_{2}(∗ = ∗, ∗)], [L_{a}], [L_{b}], [L_{c}], [L_{d}], [L_{e}], [L_{f}], [L_{g}], [L_{h}], [L_{i}], [L_{j}], [L_{k}], [L_{l}], [L_{m}], [L_{n}], [L_{o}], [L_{p}], [L_{q}], [L_{r}], [L_{s}], [L_{t}], [L_{u}], [L_{v}], [L_{w}], [L_{x}], [L_{y}], [L_{z}], [L_{A}], [L_{B}], [L_{C}], [L_{D}], [L_{E}], [L_{F}], [L_{G}], [L_{H}], [L_{I}], [L_{J}], [L_{K}], [L_{L}], [L_{M}], [L_{N}], [L_{O}], [L_{P}], [L_{Q}], [L_{R}], [L_{S}], [L_{T}], [L_{U}], [L_{V}], [L_{W}], [L_{X}], [L_{Y}], [L_{Z}], [L_{?}], [Reflexivity], [Reflexivity_{1}], [Commutativity], [Commutativity_{1}], [<tactic>], [tactic], [[∗ =^{tactic} ∗]], [P(∗, ∗, ∗)], [P^{∗}(∗, ∗, ∗)], [p_{0}], [conclude_{1}(∗, ∗)], [conclude_{2}(∗, ∗, ∗)], [conclude_{3}(∗, ∗, ∗, ∗)], [conclude_{4}(∗, ∗)], [˙0], [˙1], [˙2], [ȧ], [ḃ], [ċ], [ḋ], [ė], [ḟ], [ġ], [ḣ], [i̇], [j̇], [k̇], [l̇], [ṁ], [ṅ], [ȯ], [ṗ], [q̇], [ṙ], [ṡ], [ṫ], [u̇], [v̇], [ẇ], [ẋ], [ẏ], [ż], [ṅonfree(∗, ∗)], [ṅonfree^{∗}(∗, ∗)], [ḟree⟨∗|∗ := ∗⟩], [ḟree^{∗}⟨∗|∗ := ∗⟩], [∗≡⟨∗|∗ := ∗⟩], [∗≡⟨^{∗}∗|∗ := ∗⟩], [S], [A1], [A2], [A3], [A4], [A5], [S1], [S2], [S3], [S4], [S5], [S6], [S7], [S8], [S9], [MP], [Gen], [L3.2(a)], [S′], [A1′], [A2′], [A3′], [A4′], [A5′], [S1′], [S2′], [S3′], [S4′], [S5′], [S6′], [S7′], [S8′], [S9′], [MP′], [Gen′], [L3.2(a)′], [M1.7], [MP′_{h}], [Hypothesize], [Gen′_{h}], [M3.2(a)], [M3.2(a)_{h}], [M3.2(b)_{h}], [M3.1(S1′)_{h}], [M3.2(c)_{h}], [M3.1(S2′)_{h}], [M3.1(S5′)_{h}], [M3.1(S6′)_{h}], [M3.2(f)]; Preassociative [∗ {∗}], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [˙∗]; Preassociative [“ ∗ ”], [], [(∗)^{t}], [string(∗) + ∗], [string(∗) ++ ∗], [ ∗], [ ∗], [!∗], [”∗], [#∗], [$∗], [%∗], [&∗], [’∗], [(∗], [)∗], [∗∗], [+∗], [, ∗], [-∗], [.∗], [/∗], [0∗], [1∗], [2∗], [3∗], [4∗], [5∗], [6∗], [7∗], [8∗], [9∗], [:∗], [; ∗], [<∗], [=∗], [>∗], [?∗], [@∗], [A∗], [B∗], [C∗], [D∗], [E∗], [F∗], [G∗], [H∗], [I∗], [J∗], [K∗], [L∗], [M∗], [N∗], [O∗], [P∗], [Q∗], [R∗], [S∗], [T∗], [U∗], [V∗], [W∗], [X∗], [Y∗], [Z∗], [[∗], [\∗], []∗], [ˆ ∗], [ ∗], [‘∗], [a∗], [b∗], [c∗], [d∗], [e∗], [f∗], [g∗], [h∗], [i∗], [j∗], [k∗], [l∗], [m∗], [n∗], [o∗], [p∗], [q∗], [r∗], [s∗], [t∗], [u∗], [v∗], [w∗], [x∗], [y∗], [z∗], [{∗], [|∗], [}∗], [˜ ∗], [Preassociative ∗; ∗], [Postassociative ∗; ∗], [[∗], ∗], [priority ∗ end], [newline ∗], [macro newline ∗]; Preassociative [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗^{H}], [∗^{T}], [∗^{U}], [∗^{h}], [∗^{t}], [∗^{s}], [∗^{c}], [∗^{d}], [∗^{a}], [∗^{C}], [∗^{M}], [∗^{B}], [∗^{r}], [∗^{i}], [∗^{d}], [∗^{R}], [∗^{0}], [∗^{1}], [∗^{2}], [∗^{3}], [∗^{4}], [∗^{5}], [∗^{6}], [∗^{7}], [∗^{8}], [∗^{9}], [∗^{E}], [∗^{V}], [∗^{C}], [∗^{C^{∗}}], [∗′]; Preassociative [∗ · ∗], [∗ ·_{0} ∗], [∗ ˙· ∗]; Preassociative [∗ + ∗], [∗ +_{0} ∗], [∗ +_{1} ∗], [∗ − ∗], [∗ −_{0} ∗], [∗ −_{1} ∗], [∗ ˙+ ∗]; Preassociative [∗ ∪ {∗}], [∗ ∪ ∗], [∗\{∗}]; Postassociative [∗ ˙. . ∗], [∗ \underline{˙. .} ∗], [∗ \underline{: :} ∗], [∗ \underline{+2∗} ∗], [∗ : : ∗], [∗ +2∗ ∗]; Postassociative [∗, ∗]; Preassociative

[∗ ≈^{B} ∗], [∗ ≈^{D} ∗], [∗ ≈^{C} ∗], [∗ ≈^{P} ∗], [∗ ≈ ∗], [∗ = ∗], [∗ →^{+} ∗], [∗ =^{t} ∗], [∗ =^{t^{∗}} ∗], [∗ =^{r} ∗],

[∗ ∈_{t} ∗], [∗ ⊆_{T} ∗], [∗ =^{T} ∗], [∗ =^{s} ∗], [∗ free in ∗], [∗ free in^{∗} ∗], [∗ free for ∗ in ∗],

[∗ free for^{∗} ∗ in ∗], [∗ ∈_{c} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗], [∗ =^{p} ∗], [∗^{P}];

Preassociative [¬∗], [ ˙¬ ∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗], [∗ ˙∧ ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗], [∗ ˙∨ ∗]; Preassociative [ ˙∀∗: ∗], [ ˙∃∗: ∗]; Postassociative [∗ ¨⇒ ∗], [∗ ˙⇒ ∗], [∗ ˙⇔ ∗]; Postassociative [∗ : ∗], [∗!∗]; Preassociative

[∗ \{ \begin{matrix}∗ \\ ∗ \end{matrix} ];

Preassociative [λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗^{I}], [∗^{⊳} ], [∗^{V}], [∗^{+}], [∗^{−}], [∗^{∗}]; Preassociative [∗ @ ∗], [∗ ⊳ ∗], [∗ ⊳ ⊳ ∗], [∗ ≫ ∗], [∗ ⊵ ∗], [∗ ⊵_{h} ∗]; Postassociative [∗ ⊢ ∗], [∗ ⊢⊢ ∗], [∗ i.e. ∗]; Preassociative [∀∗: ∗]; Postassociative [∗ ⊕ ∗]; Postassociative [∗; ∗]; Preassociative [∗ proves ∗]; Preassociative [∗ proof of ∗ : ∗], [Line ∗ : ∗ ≫ ∗; ∗], [Last line ∗ ≫ ∗ □], [Line ∗ : Premise ≫ ∗; ∗], [Line ∗ : Side-condition ≫ ∗; ∗], [Arbitrary ≫ ∗; ∗], [Local ≫ ∗ = ∗; ∗]; Postassociative [∗ then ∗], [∗[ ∗]∗]; Preassociative [∗&∗]; Preassociative [∗\\∗]; ]

B Index

Peano variable, 3

variable, Peano, 3

C Bibliography

[1] K. Grue. Logiweb. In Fairouz Kamareddine, editor, Mathematical Knowledge Management Symposium 2003, volume 93 of Electronic Notes in Theoretical Computer Science, pages 70–101. Elsevier, 2004.

[2] E. Mendelson. Introduction to Mathematical Logic. Wadsworth and Brooks, 3. edition, 1987.