Peano arithmetic

Klaus Grue

GRD-2005-06-22.UTC:07:23:31.271829

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 . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.5 An alternative axiomatic system . . . . . . . . . . . . . . . . . . 6 1.6 Restatement of lemma and proof . . . . . . . . . . . . . . . . . . 8

2 Formal development 8

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

2.2 First order predicate calculus . . . . . . . . . . . . . . . . . . . . 9

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

2.3.1 Lemma M3.2(a) . . . . . . . . . . . . . . . . . . . . . . . 10 2.3.2 Lemma M3.2(b) . . . . . . . . . . . . . . . . . . . . . . . 10 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) . . . . . . . . . . . . . . . . . . . . . . . 11 2.3.8 Lemma M3.2(f) . . . . . . . . . . . . . . . . . . . . . . . . 11

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

C Bibliography 29

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]^{1}, successor [x′]^{2}, plus [x ˙+ y]^{3}, and times [x ˙· y]^{4}.

Formulas of Peano arithmeric are constructed from equality [x =^{p} y]^{5}, negation [ ˙¬ x]^{6}, implication [x ˙⇒ y]^{7}, and universal quantification [ ˙∀x: y]^{8}.

From these constructs we macro define one [˙1]^{9}, two [˙2]^{10}, conjunction [x ˙∧ y]^{11}, disjunction [x ˙∨ y]^{12}, biimplication [x ˙⇔ y]^{13}, and existential quantification [ ˙∃x: y]^{14}:

[˙1 ¨= ˙0′]

[˙2 ¨= ˙1′]

[x ˙∧ y ¨= ˙¬ (x ˙⇒ ˙¬ y)]

[x ˙∨ y ¨= ˙¬ x ˙⇒ y]

[x ˙⇔ y ¨= (x ˙⇒ y) ˙∧ (y ˙⇒ x)]

[ ˙∃x: y ¨= ˙¬ ˙∀x: ˙¬ y]

1[˙0 =^{pyk} “peano zero”]

2[x′ =^{pyk} “∗ peano succ”]

3[x ˙+ y =^{pyk} “∗ peano plus ∗”]

4[x ˙· y =^{pyk} “∗ peano times ∗”]

5[x =^{p} y =^{pyk} “∗ peano is ∗”]

6[ ˙¬ x =^{pyk} “peano not ∗”]

7[x ˙⇒ y =^{pyk} “∗ peano imply ∗”]

8[ ˙∀x: y =^{pyk} “peano all ∗ indeed ∗”]

9[˙1 =^{pyk} “peano one”]

10[˙2 =^{pyk} “peano two”]

11[x ˙∧ y =^{pyk} “∗ peano and ∗”]

12[x ˙∨ y =^{pyk} “∗ peano or ∗”]

13[x ˙⇔ y =^{pyk} “∗ peano iff ∗”]

14[ ˙∃x: y =^{pyk} “peano exist ∗ indeed ∗”]

1.2 Variables

We now introduce the unary operator [ẋ]^{15} 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}]^{16} is true if [x] is a Peano variable:

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

We macro define [ȧ]^{17} to be a Peano variable:

[ȧ ¨= ȧ]

Appendix A.2 defines Peano variables for the other letters of the English alphabet.

[ṅonfree(x, y)]^{18} is true if the Peano variable [x] does not occur free in the Peano term/formula [y]. [ṅonfree^{∗}(x, y)]^{19} is true if the Peano variable [x] does not occur free in the list [y] of Peano terms/formulas.

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

[ṅonfree^{∗}(x, y) ˙= x!If(y, T, ṅonfree(x, y^{h}) ¨∧ ṅonfree^{∗}(x, y^{t}))]

[ḟree⟨a|x := b⟩]^{20} is true if the substitution [⟨a |x:= b⟩] is free. [ḟree^{∗}⟨a|x := b⟩]^{21} is the version where [a] is a list of terms.

[ḟree⟨a|x := b⟩ ˙= x!b! if a^{P} then T else if ¬a =^{r} ⌈ ˙∀u: v⌉ then ḟree^{∗}⟨a^{t}|x := b⟩ else if a^{1} =^{t} x then T else if ṅonfree(x, a^{2}) then T else if ¬ṅonfree(a^{1}, b) then F else ḟree⟨a^{2}|x := b⟩]

[ḟree^{∗}⟨a|x := b⟩ ˙= x!b!If(a, T, ḟree⟨a^{h}|x := b⟩ ¨∧ ḟree^{∗}⟨a^{t}|x := b⟩)] [a≡⟨b|x := c⟩]^{22} is true if [a] equals [⟨b |x:= c⟩]. [a≡⟨^{∗}b|x := c⟩]^{23} is the version where [a] and [b] are lists.

15[ẋ =^{pyk} “∗ peano var”] 16[x^{P} =^{pyk} “∗ is peano var”] 17[ȧ =^{pyk} “peano a”] 18[ṅonfree(x, y) =^{pyk} “peano nonfree ∗ in ∗ end nonfree”] 19[ṅonfree^{∗}(x, y) =^{pyk} “peano nonfree star ∗ in ∗ end nonfree”] 20[ḟree⟨a|x := b⟩ =^{pyk} “peano free ∗ set ∗ to ∗ end free”] 21[ḟree^{∗}⟨a|x := b⟩ =^{pyk} “peano free star ∗ set ∗ to ∗ end free”]

[a≡⟨b|x := c⟩ ˙= a!x!c! if b =^{r} ⌈ ˙∀u: v⌉ ¨∧ b^{1} =^{t} x then a =^{t} b else if b^{P} ∧ b =^{t} x then a =^{t} c else a =^{r} b ¨∧ a^{t}≡⟨^{∗}b^{t}|x := c⟩]

[a≡⟨^{∗}b|x := c⟩ ˙= b!x!c!If(a, T, a^{h}≡⟨b^{h}|x := c⟩ ¨∧ a^{t}≡⟨^{∗}b^{t}|x := c⟩)]

1.3 Mendelsons system S

System [S]^{24} of Mendelson [2] expresses Peano arithmetic. It comprises the axioms [A1]^{25}, [A2]^{26}, [A3]^{27}, [A4]^{28}, and [A5]^{29} and inference rules [MP]^{30} and [Gen]^{31} of first order predicate calculus. Furthermore, it comprises the proper axioms [S1]^{32}, [S2]^{33}, [S3]^{34}, [S4]^{35}, [S5]^{36}, [S6]^{37}, [S7]^{38}, [S8]^{39}, and [S9]^{40}. 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] The order of quantifiers in the following axiom is such that [C] which the current conclusion tactic cannot guess comes first. This allows to supply a value for [C] without having to supply values for the other meta-variables.

22[a≡⟨b|x := c⟩ =^{pyk} “peano sub ∗ is ∗ where ∗ is ∗ end sub”] 23[a≡⟨^{∗}b|x := c⟩ =^{pyk} “peano sub star ∗ is ∗ where ∗ is ∗ end sub”] 24[S =^{pyk} “system s”] 25[A1 =^{pyk} “axiom a one”] 26[A2 =^{pyk} “axiom a two”] 27[A3 =^{pyk} “axiom a three”] 28[A4 =^{pyk} “axiom a four”] 29[A5 =^{pyk} “axiom a five”] 30[MP =^{pyk} “rule mp”] 31[Gen =^{pyk} “rule gen”] 32[S1 =^{pyk} “axiom s one”] 33[S2 =^{pyk} “axiom s two”] 34[S3 =^{pyk} “axiom s three”] 35[S4 =^{pyk} “axiom s four”] 36[S5 =^{pyk} “axiom s five”] 37[S6 =^{pyk} “axiom s six”] 38[S7 =^{pyk} “axiom s seven”] 39[S8 =^{pyk} “axiom s eight”] 40[S9 =^{pyk} “axiom s nine”]

[S rule A4: ∀C: ∀A: ∀X: ∀B: ⌈A⌉≡⟨⌈B⌉|⌈X ⌉ := ⌈C⌉⟩ ⊢⊢ ˙∀X: B ˙⇒ A]

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

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

[S rule Gen: ∀X: ∀A: A ⊢ ˙∀X: A]

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.

[S rule S1: ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ċ ˙⇒ ḃ =^{p} ċ]

[S rule S2: ȧ =^{p} ḃ ˙⇒ ȧ′ =^{p} ḃ′]

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

[S rule S4: ȧ′ =^{p} ḃ′ ˙⇒ ȧ =^{p} ḃ]

[S rule S5: ȧ ˙+ ˙0 =^{p} ȧ]

[S rule S6: ȧ ˙+ ḃ′ =^{p} (ȧ ˙+ ḃ)′]

[S rule S7: ȧ ˙· ˙0 =^{p} ˙0]

[S rule S8: ȧ ˙·(ḃ′) =^{p} (ȧ ˙· ḃ) ˙+ ȧ]

[S rule S9: ∀A: ∀B: ∀C: ∀X: B≡⟨A|X := ˙0⟩ ⊢⊢ C≡⟨A|X := X′⟩ ⊢⊢ B ˙⇒ ˙∀X: (A ˙⇒ C) ˙⇒ ˙∀X: A]

1.4 A lemma and a proof

We now prove Lemma [L3.2(a)]^{41} which is an instance of the corresponding proposition in Mendelson [2]:

[S lemma L3.2(a): ẋ =^{p} ẋ] S proof of L3.2(a):

41[L3.2(a) =^{pyk} “lemma l three two a”]

L01: S5 ≫  ȧ ˙+ ˙0 =^{p} ȧ  ;
L02: Gen ⊳ L01 ≫  ˙∀ȧ: ȧ ˙+ ˙0 =^{p} ȧ  ;
L03: A4 @ ẋ ≫  ˙∀ȧ: ȧ ˙+ ˙0 =^{p} ȧ ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ  ;
L04: MP ⊳ L03 ⊳ L02 ≫  ẋ ˙+ ˙0 =^{p} ẋ  ;
L05: S1 ≫  ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ċ ˙⇒ ḃ =^{p} ċ  ;
L06: Gen ⊳ L05 ≫  ˙∀ċ: (ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ċ ˙⇒ ḃ =^{p} ċ)  ;

L07: A4 @ ẋ ≫

˙∀ċ: (ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ċ ˙⇒ ḃ =^{p}
ċ) ˙⇒ ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ẋ ˙⇒ ḃ =^{p} ẋ ;
L08: MP ⊳ L07 ⊳ L06 ≫  ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ẋ ˙⇒ ḃ =^{p} ẋ  ;
L09: Gen ⊳ L08 ≫  ˙∀ḃ: (ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ẋ ˙⇒ ḃ =^{p} ẋ) ;

L10: A4 @ ẋ ≫

˙∀ḃ: (ȧ =^{p} ḃ ˙⇒ ȧ =^{p} ẋ ˙⇒ ḃ =^{p}
ẋ) ˙⇒ ȧ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ẋ =^{p} ẋ ;
L11: MP ⊳ L10 ⊳ L09 ≫  ȧ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ẋ =^{p} ẋ  ;
L12: Gen ⊳ L11 ≫  ˙∀ȧ: (ȧ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ẋ =^{p} ẋ) ;

L13: A4 @ ẋ ˙+ ˙0 ≫ ˙∀ȧ: (ȧ =^{p} ẋ ˙⇒ ȧ =^{p} ẋ ˙⇒ ẋ =^{p}

ẋ) ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒

ẋ =^{p} ẋ  ;

L14: MP ⊳ L13 ⊳ L12 ≫

ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ =^{p}
ẋ  ;
L15: MP ⊳ L14 ⊳ L04 ≫  ẋ ˙+ ˙0 =^{p} ẋ ˙⇒ ẋ =^{p} ẋ  ;
L16: MP ⊳ L15 ⊳ L04 ≫  ẋ =^{p} ẋ  □

1.5 An alternative axiomatic system

System [S′]^{42} is system [S] in which the proper axioms are taken from Lemma 3.1 in Mendelson [2]. It comprises the axioms [A1′]^{43}, [A2′]^{44}, [A3′]^{45}, [A4′]^{46}, and [A5′]^{47} and inference rules [MP′]^{48} and [Gen′]^{49} of first order predicate calculus. Furthermore, it comprises the proper axioms [S1′]^{50}, [S2′]^{51}, [S3′]^{52}, [S4′]^{53}, [S5′]^{54}, [S6′]^{55}, [S7′]^{56}, [S8′]^{57}, and [S9′]^{58}.

42[S′ =^{pyk} “system prime s”]

43[A1′ =^{pyk} “axiom prime a one”]

44[A2′ =^{pyk} “axiom prime a two”]

45[A3′ =^{pyk} “axiom prime a three”]

46[A4′ =^{pyk} “axiom prime a four”]

47[A5′ =^{pyk} “axiom prime a five”]

48[MP′ =^{pyk} “rule prime mp”]

49[Gen′ =^{pyk} “rule prime gen”]

50[S1′ =^{pyk} “axiom prime s one”]

51[S2′ =^{pyk} “axiom prime s two”]

52[S3′ =^{pyk} “axiom prime s three”]

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] [S′ rule A5′: ∀X: ∀A: ∀B: ṅonfree(⌈X ⌉, ⌈A⌉) ⊢⊢ ˙∀X: (A ˙⇒ B) ˙⇒ A ˙⇒ ˙∀X: B] [S′ rule MP′: ∀A: ∀B: A ˙⇒ B ⊢ A ⊢ B] [S′ rule Gen′: ∀X: ∀A: A ⊢ ˙∀X: A]

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

Note that [A1] and [A1′] are distinct. The former says [S ⊢ ∀A: ∀B: A ˙⇒ B ˙⇒ A] and the latter says [S′ ⊢ ∀A: ∀B: A ˙⇒ B ˙⇒ A].

53[S4′ =^{pyk} “axiom prime s four”] 54[S5′ =^{pyk} “axiom prime s five”] 55[S6′ =^{pyk} “axiom prime s six”] 56[S7′ =^{pyk} “axiom prime s seven”] 57[S8′ =^{pyk} “axiom prime s eight”] 58[S9′ =^{pyk} “axiom prime s nine”]

1.6 Restatement of lemma and proof

We now prove Lemma [L3.2(a)] once again under the name of [L3.2(a)′]^{59}: [S′ lemma L3.2(a)′: ∀A: A =^{p} A] S′ proof of L3.2(a)′:

L01: Arbitrary ≫  A  ;
L02: S5′ ≫  A ˙+ ˙0 =^{p} A  ;
L03: S1′ ≫  {A ˙+ ˙0 =^{p} A ˙⇒ \atop A ˙+ ˙0 =^{p} A ˙⇒ A =^{p} A  ;}
L04: MP′ ⊳ L03 ⊳ L02 ≫  A ˙+ ˙0 =^{p} A ˙⇒ A =^{p} A  ;
L05: MP′ ⊳ L04 ⊳ L02 ≫  A =^{p} A  □

2 Formal development

2.1 Propositional calculus

2.1.1 Modus ponens We use [x ⊵ y]^{60} as shorthand for modus ponens:

[x ⊵ y ¨= MP′ ⊳ x ⊳ y] 2.1.2 Lemma M1.7 Lemma [M1.7]^{61} (i.e. Lemma 1.7 in Mendelson [2]) reads: [S′ lemma M1.7: ∀B: B ˙⇒ B] S′ proof of M1.7:

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

2.1.3 Hypothetical modus ponens The hypothetical version [MP′_{h}]^{62} of modus ponens MP′ has a hypothesis H on each premise and on the conclusion:

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

60[x ⊵ y =^{pyk} “∗ macro modus ponens ∗”]

61[M1.7 =^{pyk} “mendelson one seven”]

62[MP′_{h} =^{pyk} “hypothetical rule prime mp”]

[S′ lemma MP′_{h}: ∀H: ∀A: ∀B: H ˙⇒ A ˙⇒ B ⊢ H ˙⇒ A ⊢ H ˙⇒ B] S′ proof of MP′_{h}:

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

We use [x ⊵_{h} y]^{63} as shorthand for hypothetical modus ponens:

[x ⊵_{h} y ¨= MP′_{h} ⊳ x ⊳ y] 2.1.4 Turning lemmas to hypothetical lemmas Lemma [Hypothesize]^{64} turns a lemma with no premises into one that assumes the hypothesis [H] to hold: [S′ lemma Hypothesize: ∀H: ∀A: A ⊢ H ˙⇒ A] S′ proof of Hypothesize:

L01: Arbitrary ≫  H  ;
L02: Arbitrary ≫  A  ;
L03: Premise ≫  A  ;
L04: A1′ ≫  A ˙⇒ H ˙⇒ A  ;
L05: L04 ⊵ L03 ≫  H ˙⇒ A  □

2.2 First order predicate calculus

2.2.1 Hypothetical generalization The hypothetical version [Gen′_{h}]^{65} of generalisation Gen′ has a hypothesis H on premise and conclusion: [S′ lemma Gen′_{h}: ∀H: ∀X: ∀A: ṅonfree(⌈X ⌉, ⌈H⌉) ⊢⊢ H ˙⇒ A ⊢ H ˙⇒ ˙∀X: A] S′ proof of Gen′_{h}:

L01: Arbitrary ≫  H  ;
L02: Arbitrary ≫  X  ;
L03: Arbitrary ≫  A  ;
L04: Side-condition ≫  ṅonfree(⌈X ⌉, ⌈H⌉)  ;

63[x ⊵_{h} y =^{pyk} “∗ hypothetical modus ponens ∗”]

64[Hypothesize =^{pyk} “hypothesize”]

65[Gen′_{h} =^{pyk} “hypothetical rule prime gen”]

L05: Premise ≫  H ˙⇒ A  ;
L06: A5′ ⊳ ⊳ L04 ≫  ˙∀X: (H ˙⇒ A) ˙⇒ H ˙⇒ ˙∀X: A  ;
L07: Gen′ ⊳ L05 ≫  ˙∀X: (H ˙⇒ A)  ;
L08: L06 ⊵ L07 ≫  H ˙⇒ ˙∀X: A  □

2.3 Peano arithmetic

2.3.1 Lemma M3.2(a) Lemma [M3.2(a)]^{66} and the associated hypothetical lemma [M3.2(a)_{h}]^{67} read: [S′ rule M3.2(a): ∀T : T =^{p} T ] [S′ lemma M3.2(a)_{h}: ∀H: ∀T : H ˙⇒ T =^{p} 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. S′ proof of M3.2(a)_{h}:

L01: Arbitrary ≫  H  ;
L02: Arbitrary ≫  T  ;
L03: M3.2(a) ≫  T =^{p} T  ;
L04: Hypothesize ⊳ L03 ≫  H ˙⇒ T =^{p} T  □

2.3.2 Lemma M3.2(b) Lemma [M3.2(b)_{h}]^{68} reads: [S′ rule M3.2(b)_{h}: ∀H: ∀T : ∀R: H ˙⇒ T =^{p} R ⊢ H ˙⇒ R =^{p} T ] S′ proof of M3.2(b)_{h}:

L01: Arbitrary ≫  H  ;
L02: Arbitrary ≫  T  ;
L03: Arbitrary ≫  R  ;
L04: Premise ≫  H ˙⇒ T =^{p} R  ;
L05: S1′ ≫  T =^{p} R ˙⇒ T =^{p} T ˙⇒ R =^{p} T  ;
L06: Hypothesize ⊳ L05 ≫  {H ˙⇒ T =^{p} R ˙⇒ T =^{p} T ˙⇒ R =^{p} \atop T  ;}
L07: L06 ⊵_{h} L04 ≫  H ˙⇒ T =^{p} T ˙⇒ R =^{p} T  ;
L08: M3.2(a)_{h} ≫  H ˙⇒ T =^{p} T  ;
L09: L07 ⊵_{h} L08 ≫  H ˙⇒ R =^{p} T  □

66[M3.2(a) =^{pyk} “mendelson three two a”]

67[M3.2(a)_{h} =^{pyk} “hypothetical three two a”]

68[M3.2(b)_{h} =^{pyk} “hypothetical three two b”]

2.3.3 Lemma M3.1(S1) Lemma [M3.1(S1′)_{h}]^{69} is the hypothetical version of Mendelson Lemma 3.1(S1′):

[S′ rule M3.1(S1′)_{h}: ∀H: ∀T : ∀R: ∀S: H ˙⇒ T =^{p} R ⊢ H ˙⇒ T =^{p} S ⊢ H ˙⇒ R =^{p}

S] 2.3.4 Lemma M3.2(c) Lemma [M3.2(c)_{h}]^{70} is the hypothetical version of Mendelson Lemma 3.2(c) which expresses ordinary transitivity:

[S′ rule M3.2(c)_{h}: ∀H: ∀T : ∀R: ∀S: H ˙⇒ T =^{p} R ⊢ H ˙⇒ R =^{p} S ⊢ H ˙⇒ T =^{p} S]

2.3.5 Lemma M3.1(S2) Lemma [M3.1(S2′)_{h}]^{71} is the hypothetical version of Mendelson Lemma 3.1(S2′): [S′ rule M3.1(S2′)_{h}: ∀H: ∀T : ∀R: H ˙⇒ T =^{p} R ⊢ H ˙⇒ T′ =^{p} R′] 2.3.6 Lemma M3.1(S5) Lemma [M3.1(S5′)_{h}]^{72} is the hypothetical version of Mendelson Lemma 3.1(S5′): [S′ rule M3.1(S5′)_{h}: ∀H: ∀T : H ˙⇒ T ˙+ ˙0 =^{p} T ] 2.3.7 Lemma M3.1(S6) Lemma [M3.1(S6′)_{h}]^{73} is the hypothetical version of Mendelson Lemma 3.1(S6′): [S′ rule M3.1(S6′)_{h}: ∀H: ∀T : ∀R: H ˙⇒ T ˙+ R′ =^{p} (T ˙+ R)′] 2.3.8 Lemma M3.2(f) Lemma [M3.2(f)]^{74} is the closure of Mendelson Lemma 3.2(f) for the concrete variable [ṫ]: [S′ lemma M3.2(f): ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ] The proof below uses local macro definitions.

69[M3.1(S1′)_{h} =^{pyk} “hypothetical three one s one”]

70[M3.2(c)_{h} =^{pyk} “hypothetical three two c”]

71[M3.1(S2′)_{h} =^{pyk} “hypothetical three one s two”]

72[M3.1(S5′)_{h} =^{pyk} “hypothetical three one s five”]

73[M3.1(S6′)_{h} =^{pyk} “hypothetical three one s six”]

74[M3.2(f) =^{pyk} “mendelson three two f”]

S′ proof of M3.2(f):

L01: Local ≫  Z = x ˙⇒ x ˙⇒ x  ;
L02: A1′ ≫  Z  ;
L03: M3.1(S5′)_{h} ≫  Z ˙⇒ ˙0 ˙+ ˙0 =^{p} ˙0  ;
L04: M3.2(b)_{h} ⊳ L03 ≫  Z ˙⇒ ˙0 =^{p} ˙0 ˙+ ˙0  ;
L05: L04 ⊵ L02 ≫  ˙0 =^{p} ˙0 ˙+ ˙0  ;
L06: Local ≫  H = ṫ =^{p} ˙0 ˙+ ṫ  ;
L07: M1.7 ≫  H ˙⇒ ṫ =^{p} ˙0 ˙+ ṫ  ;
L08: M3.1(S2′)_{h} ⊳ L07 ≫  H ˙⇒ ṫ′ =^{p} (˙0 ˙+ ṫ)′  ;
L09: M3.1(S6′)_{h} ≫  H ˙⇒ ˙0 ˙+ ṫ′ =^{p} (˙0 ˙+ ṫ)′  ;
L10: M3.2(b)_{h} ⊳ L09 ≫  H ˙⇒ (˙0 ˙+ ṫ)′ =^{p} ˙0 ˙+ ṫ′  ;
L11: M3.2(c)_{h} ⊳ L08 ⊳ L10 ≫  H ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′  ;
L12: Gen′ ⊳ L11 ≫  ˙∀ṫ: (H ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′)  ;

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

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

L14: L13 ⊵ L05 ≫

˙∀ṫ: (H ˙⇒ ṫ′ =^{p} ˙0 ˙+ ṫ′) ˙⇒ ˙∀ṫ: ṫ =^{p}
˙0 ˙+ ṫ  ;
L15: L14 ⊵ L12 ≫  ˙∀ṫ: ṫ =^{p} ˙0 ˙+ ṫ  □

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 [ḃ]^{75}, [ċ]^{76}, [ḋ]^{77}, [ė]^{78}, [ḟ]^{79}, [ġ]^{80}, [ḣ]^{81}, [i̇]^{82}, [j̇]^{83}, [k̇]^{84}, [l̇]^{85}, [ṁ]^{86}, [ṅ]^{87}, [ȯ]^{88}, [ṗ]^{89}, [q̇]^{90}, [ṙ]^{91}, [ṡ]^{92}, [ṫ]^{93}, [u̇]^{94}, [v̇]^{95}, [ẇ]^{96}, [ẋ]^{97}, [ẏ]^{98}, and [ż]^{99} to denote variables of Peano arithmetic:

[ḃ ¨= ḃ], [ċ ¨= ċ], [ḋ ¨= ḋ], [ė ¨= ė], [ḟ ¨= ḟ], [ġ ¨= ġ], [ḣ ¨= ḣ], [i̇ ¨= i̇], [j̇ ¨= j̇], [k̇ ¨= k̇], [l̇ ¨= l̇], [ṁ ¨= ṁ], [ṅ ¨= ṅ], [ȯ ¨= ȯ], [ṗ ¨= ṗ], [q̇ ¨= q̇], [ṙ ¨= ṙ], [ṡ ¨= ṡ], [ṫ ¨= ṫ], [u̇ ¨= u̇], [v̇ ¨= v̇], [ẇ ¨= ẇ], [ẋ ¨= ẋ], [ẏ ¨= ẏ], and [ż ¨= ż].

A.3 TEX definitions

[˙0 =^{tex} “

\dot{0}”]

[x′ =^{tex} “#1.

’”]

75[ḃ =^{pyk} “peano b”] 76[ċ =^{pyk} “peano c”] 77[ḋ =^{pyk} “peano d”] 78[ė =^{pyk} “peano e”] 79[ḟ =^{pyk} “peano f”] 80[ġ =^{pyk} “peano g”] 81[ḣ =^{pyk} “peano h”] 82[i̇ =^{pyk} “peano i”] 83[j̇ =^{pyk} “peano j”] 84[k̇ =^{pyk} “peano k”] 85[l̇ =^{pyk} “peano l”] 86[ṁ =^{pyk} “peano m”] 87[ṅ =^{pyk} “peano n”] 88[ȯ =^{pyk} “peano o”] 89[ṗ =^{pyk} “peano p”] 90[q̇ =^{pyk} “peano q”] 91[ṙ =^{pyk} “peano r”] 92[ṡ =^{pyk} “peano s”] 93[ṫ =^{pyk} “peano t”] 94[u̇ =^{pyk} “peano u”] 95[v̇ =^{pyk} “peano v”] 96[ẇ =^{pyk} “peano w”] 97[ẋ =^{pyk} “peano x”] 98[ẏ =^{pyk} “peano y”] 99[ż =^{pyk} “peano z”]

[x ˙+ y =^{tex} “#1.

\mathop{\dot{+}} #2.”]

[x ˙· y =^{tex} “#1.

\mathop{\dot{\cdot}} #2.”]

[x =^{p} y =^{tex} “#1.

\stackrel{p}{=} #2.”]

[ ˙¬ x =^{tex} “

\dot{\neg}\, #1.”]

[x ˙⇒ y =^{tex} “#1.

\mathrel{\dot{\Rightarrow}} #2.”]

[ ˙∀x: y =^{tex} “

\dot{\forall} #1. \colon #2.”]

[˙1 =^{tex} “

\dot{1}”]

[˙2 =^{tex} “

\dot{2}”]

[x ˙∧ y =^{tex} “#1.

\mathrel{\dot{\wedge}} #2.”]

[x ˙∨ y =^{tex} “#1.

\mathrel{\dot{\vee}} #2.”]

[x ˙⇔ y =^{tex} “#1.

\mathrel{\dot{\Leftrightarrow}} #2.”]

[ ˙∃x: y =^{tex} “

\dot{\exists} #1. \colon #2.”]

[ẋ =^{tex} “

\dot{#1. }”]

[x^{P} =^{tex} “#1.

{} ˆ {\cal P}”]

[ȧ =^{tex} “

\dot{\mathit{a}}”] [ṅonfree(x, y) =^{tex} “

\dot{nonfree}(#1. , #2. )”]

[ṅonfree^{∗}(x, y) =^{tex} “ \dot{nonfree}ˆ ∗(#1. , #2. )”]

[ḟree⟨a|x := b⟩ =^{tex} “ \dot{free}\langle #1. | #2. := #3. \rangle”]

[ḟree^{∗}⟨a|x := b⟩ =^{tex} “ \dot{free}{}ˆ ∗\langle #1. | #2. := #3. \rangle”]

[a≡⟨b|x := c⟩ =^{tex} “#1.

{\equiv}\langle #2. |#3. :=#4. \rangle”]

[a≡⟨^{∗}b|x := c⟩ =^{tex} “#1.

{\equiv}\langleˆ ∗ #2. |#3. :=#4. \rangle”]

[S =^{tex} “

S”]

[A1 =^{tex} “

A1”]

[A2 =^{tex} “

A2”]

[A3 =^{tex} “

A3”]

[A4 =^{tex} “

A4”]

[A5 =^{tex} “

A5”]

[MP =^{tex} “

MP”]

[Gen =^{tex} “

Gen”]

[S1 =^{tex} “

S1”]

[S2 =^{tex} “

S2”]

[S3 =^{tex} “

S3”]

[S4 =^{tex} “

S4”]

[S5 =^{tex} “

S5”]

[S6 =^{tex} “

S6”]

[S7 =^{tex} “

S7”]

[S8 =^{tex} “

S8”]

[S9 =^{tex} “

S9”]

[L3.2(a) =^{tex} “

L3.2(a)”]

[S′ =^{tex} “

S’”]

[A1′ =^{tex} “

A1’”]

[A2′ =^{tex} “

A2’”]

[A3′ =^{tex} “

A3’”]

[A4′ =^{tex} “

A4’”]

[A5′ =^{tex} “

A5’”]

[MP′ =^{tex} “

MP’”]

[Gen′ =^{tex} “

Gen’”]

[S1′ =^{tex} “

S1’”]

[S2′ =^{tex} “

S2’”]

[S3′ =^{tex} “

S3’”]

[S4′ =^{tex} “

S4’”]

[S5′ =^{tex} “

S5’”]

[S6′ =^{tex} “

S6’”]

[S7′ =^{tex} “

S7’”]

[S8′ =^{tex} “

S8’”]

[S9′ =^{tex} “

S9’”]

[L3.2(a)′ =^{tex} “

L3.2(a)’”]

[x ⊵ y =^{tex} “#1.

\unrhd #2.”]

[M1.7 =^{tex} “

M1.7”]

[MP′_{h} =^{tex} “

MP’ h”]

[x ⊵_{h} y =^{tex} “#1.

\unrhd h #2.”]

[Hypothesize =^{tex} “

Hypothesize”]

[Gen′_{h} =^{tex} “

Gen’ h”]

[M3.2(a) =^{tex} “

M3.2(a)”]

[M3.2(a)_{h} =^{tex} “

M3.2(a) h”]

[M3.2(b)_{h} =^{tex} “

M3.2(b) h”]

[M3.1(S1′)_{h} =^{tex} “

M3.1(S1’) h”]

[M3.2(c)_{h} =^{tex} “

M3.2(c) h”]

[M3.1(S2′)_{h} =^{tex} “

M3.1(S2’) h”]

[M3.1(S5′)_{h} =^{tex} “

M3.1(S5’) h”]

[M3.1(S6′)_{h} =^{tex} “

M3.1(S6’) h”]

[M3.2(f) =^{tex} “

M3.2(f)”]

[ḃ =^{tex} “

\dot{\mathit{b}}”]

[ċ =^{tex} “

\dot{\mathit{c}}”]

[ḋ =^{tex} “

\dot{\mathit{d}}”]

[ė =^{tex} “

\dot{\mathit{e}}”]

[ḟ =^{tex} “

\dot{\mathit{f}}”]

[ġ =^{tex} “

\dot{\mathit{g}}”]

[ḣ =^{tex} “

\dot{\mathit{h}}”]

[i̇ =^{tex} “

\dot{\mathit{i}}”]

[j̇ =^{tex} “

\dot{\mathit{j}}”]

[k̇ =^{tex} “

\dot{\mathit{k}}”]

[l̇ =^{tex} “

\dot{\mathit{l}}”]

[ṁ =^{tex} “

\dot{\mathit{m}}”]

[ṅ =^{tex} “

\dot{\mathit{n}}”]

[ȯ =^{tex} “

\dot{\mathit{o}}”]

[ṗ =^{tex} “

\dot{\mathit{p}}”]

[q̇ =^{tex} “

\dot{\mathit{q}}”]

[ṙ =^{tex} “

\dot{\mathit{r}}”]

[ṡ =^{tex} “

\dot{\mathit{s}}”]

[ṫ =^{tex} “

\dot{\mathit{t}}”]

[u̇ =^{tex} “

\dot{\mathit{u}}”]

[v̇ =^{tex} “

\dot{\mathit{v}}”]

[ẇ =^{tex} “

\dot{\mathit{w}}”]

[ẋ =^{tex} “

\dot{\mathit{x}}”]

[ẏ =^{tex} “

\dot{\mathit{y}}”]

[ż =^{tex} “

\dot{\mathit{z}}”]

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

Priority table 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 [∗\\∗]; End table

B Index

[x ⊵_{h} y] * hypothetical modus ponens *, 9 [x ⊵ y] * macro modus ponens *, 8 [x ˙∧ y] * peano and *, 2 [x ˙⇔ y] * peano iff *, 2 [x ˙⇒ y] * peano imply *, 2 [x ˙∨ y] * peano or *, 2 [x ˙+ y] * peano plus *, 2 [x′] * peano succ, 2 [x ˙· y] * peano times *, 2 [ẋ] * peano var, 3 [ ˙∀x: y] peano all * indeed *, 2 [ ˙∃x: y] peano exist * indeed *, 2 [ ˙¬ x] peano not *, 2 [˙1] peano one, 2 [˙2] peano two, 2 [˙0] peano zero, 2

A1’: [A1′] axiom prime a one, 6 A1: [A1] axiom a one, 4 A2’: [A2′] axiom prime a two, 6 A2: [A2] axiom a two, 4 A3’: [A3′] axiom prime a three, 6 A3: [A3] axiom a three, 4 A4’: [A4′] axiom prime a four, 6 A4: [A4] axiom a four, 4 A5’: [A5′] axiom prime a five, 6 A5: [A5] axiom a five, 4 a: [ȧ] peano a, 3

b: [ḃ] peano b, 13

c: [ċ] peano c, 13

d: [ḋ] peano d, 13

e: [ė] peano e, 13

f: [ḟ] peano f, 13 free*: [ḟree^{∗}⟨a, x := b⟩] peano free star * set * to * end free3 free: [ḟree⟨a, x := b⟩] peano free * set * to * end free3

g: [ġ] peano g, 13 Gen’: [Gen′] rule prime gen, 6 Gen: [Gen′_{h}] hypothetical rule prime gen, 9 Gen: [Gen] rule gen, 4

h: [ḣ] peano h, 13 hypothesize: [Hypothesize] hypothesize, 9

i: [i̇] peano i, 13

j: [j̇] peano j, 13

k: [k̇] peano k, 13

L3.2(a)’: [L3.2(a)′] lemma prime l three two a, 8 L3.2(a): [L3.2(a)] lemma l three two a, 5 l: [l̇] peano l, 13

M1.7: [M1.7] mendelson one seven, 8 M3.1(S1): [M3.1(S1′)_{h}] hypothetical three one s one, 11 M3.1(S2): [M3.1(S2′)_{h}] hypothetical three one s two, 11 M3.1(S5): [M3.1(S5′)_{h}] hypothetical three one s five, 11 M3.1(S6): [M3.1(S6′)_{h}] hypothetical three one s six, 11 M3.2(a): [M3.2(a)_{h}] hypothetical three two a, 10 M3.2(a): [M3.2(a)] mendelson three two a, 10 M3.2(b): [M3.2(b)_{h}] hypothetical three two b, 10 M3.2(c): [M3.2(c)_{h}] hypothetical three two c, 11 M3.2(f): [M3.2(f)] mendelson three two f, 11 m: [ṁ] peano m, 13 MP’: [MP′] rule prime mp, 6 MP: [MP′_{h}] hypothetical rule prime mp, 8 MP: [MP] rule mp, 4

n: [ṅ] peano n, 13 nonfree*: [ṅonfree^{∗}(x, y)] peano nonfree star * in * end nonfree, 3 nonfree: [ṅonfree(x, y)] peano nonfree * in * end nonfree, 3

o: [ȯ] peano o, 13

P: [x^{P}] * is peano var, 3 p: [x =^{p} y] * peano is *, 2 p: [ṗ] peano p, 13 Peano variable, 3 pyk: * hypothetical modus ponens * [x ⊵_{h} y], 9 pyk: * is peano var [x^{P}], 3 pyk: * macro modus ponens * [x ⊵ y], 8 pyk: * peano and * [x ˙∧ y], 2 pyk: * peano iff * [x ˙⇔ y], 2 pyk: * peano imply * [x ˙⇒ y], 2 pyk: * peano is * [x =^{p} y], 2 pyk: * peano or * [x ˙∨ y], 2 pyk: * peano plus * [x ˙+ y], 2 pyk: * peano succ [x′], 2 pyk: * peano times * [x ˙· y], 2 pyk: * peano var [ẋ], 3 pyk: axiom a five [A5], 4 pyk: axiom a four [A4], 4 pyk: axiom a one [A1], 4 pyk: axiom a three [A3], 4 pyk: axiom a two [A2], 4 pyk: axiom prime a five [A5′], 6 pyk: axiom prime a four [A4′], 6 pyk: axiom prime a one [A1′], 6 pyk: axiom prime a three [A3′], 6 pyk: axiom prime a two [A2′], 6 pyk: axiom prime s eight [S8′], 7 pyk: axiom prime s five [S5′], 7 pyk: axiom prime s four [S4′], 7 pyk: axiom prime s nine [S9′], 7 pyk: axiom prime s one [S1′], 6 pyk: axiom prime s seven [S7′], 7 pyk: axiom prime s six [S6′], 7 pyk: axiom prime s three [S3′], 6 pyk: axiom prime s two [S2′], 6 pyk: axiom s eight [S8], 4 pyk: axiom s five [S5], 4 pyk: axiom s four [S4], 4 pyk: axiom s nine [S9], 4 pyk: axiom s one [S1], 4 pyk: axiom s seven [S7], 4 pyk: axiom s six [S6], 4 pyk: axiom s three [S3], 4 pyk: axiom s two [S2], 4 pyk: hypothesize [Hypothesize], 9 pyk: hypothetical rule prime gen [Gen′_{h}], 9 pyk: hypothetical rule prime mp [MP′_{h}], 8 pyk: hypothetical three one s five [M3.1(S5′)_{h}], 11 pyk: hypothetical three one s one [M3.1(S1′)_{h}], 11 pyk: hypothetical three one s six [M3.1(S6′)_{h}], 11 pyk: hypothetical three one s two [M3.1(S2′)_{h}], 11 pyk: hypothetical three two a [M3.2(a)_{h}], 10 pyk: hypothetical three two b [M3.2(b)_{h}], 10 pyk: hypothetical three two c [M3.2(c)_{h}], 11 pyk: lemma l three two a [L3.2(a)], 5 pyk: lemma prime l three two a [L3.2(a)′], 8 pyk: mendelson one seven [M1.7], 8 pyk: mendelson three two a [M3.2(a)], 10 pyk: mendelson three two f [M3.2(f)], 11 pyk: peano a [ȧ], 3 pyk: peano all * indeed * [ ˙∀x: y], 2 pyk: peano b [ḃ], 13 pyk: peano c [ċ], 13 pyk: peano d [ḋ], 13 pyk: peano e [ė], 13 pyk: peano exist * indeed * [ ˙∃x: y], 2 pyk: peano f [ḟ], 13 pyk: peano free * set * to * end free [ḟree⟨a, x := b⟩]3 pyk: peano free star * set * to * end free [ḟree^{∗}⟨a, x := b⟩]3 pyk: peano g [ġ], 13 pyk: peano h [ḣ], 13 pyk: peano i [i̇], 13 pyk: peano j [j̇], 13 pyk: peano k [k̇], 13 pyk: peano l [l̇], 13 pyk: peano m [ṁ], 13 pyk: peano n [ṅ], 13 pyk: peano nonfree * in * end nonfree [ṅonfree(x, y)], 3 pyk: peano nonfree star * in * end nonfree [ṅonfree^{∗}(x, y)], 3 pyk: peano not * [ ˙¬ x], 2 pyk: peano o [ȯ], 13 pyk: peano one [˙1], 2 pyk: peano p [ṗ], 13 pyk: peano q [q̇], 13 pyk: peano r [ṙ], 13 pyk: peano s [ṡ], 13 pyk: peano sub * is * where * is * end sub [a≡⟨b, x := c⟩]4 pyk: peano sub star * is * where * is * end sub [a≡⟨^{∗}b, x := c⟩]4 pyk: peano t [ṫ], 13 pyk: peano two [˙2], 2 pyk: peano u [u̇], 13 pyk: peano v [v̇], 13 pyk: peano w [ẇ], 13 pyk: peano x [ẋ], 13 pyk: peano y [ẏ], 13 pyk: peano z [ż], 13 pyk: peano zero [˙0], 2 pyk: rule gen [Gen], 4 pyk: rule mp [MP], 4 pyk: rule prime gen [Gen′], 6 pyk: rule prime mp [MP′], 6 pyk: system prime s [S′], 6 pyk: system s [S], 4

q: [q̇] peano q, 13

r: [ṙ] peano r, 13

S’: [S′] system prime s, 6 S1’: [S1′] axiom prime s one, 6 S1: [S1] axiom s one, 4 S2’: [S2′] axiom prime s two, 6 S2: [S2] axiom s two, 4 S3’: [S3′] axiom prime s three, 6 S3: [S3] axiom s three, 4 S4’: [S4′] axiom prime s four, 7 S4: [S4] axiom s four, 4 S5’: [S5′] axiom prime s five, 7 S5: [S5] axiom s five, 4 S6’: [S6′] axiom prime s six, 7 S6: [S6] axiom s six, 4 S7’: [S7′] axiom prime s seven, 7 S7: [S7] axiom s seven, 4 S8’: [S8′] axiom prime s eight, 7 S8: [S8] axiom s eight, 4 S9’: [S9′] axiom prime s nine, 7 S9: [S9] axiom s nine, 4 s: [ṡ] peano s, 13 S: [S] system s, 4

t: [ṫ] peano t, 13

u: [u̇] peano u, 13

v: [v̇] peano v, 13 variable, Peano, 3

w: [ẇ] peano w, 13

x: [ẋ] peano x, 13

y: [ẏ] peano y, 13

z: [ż] peano z, 13

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.