Peano arithmetic

Klaus Grue

GRD-2005-06-20.UTC:11:17:32.910911

Contents

1 Peano arithmetic 1 1.1 The constructs of Peano arithmetic . . . . . . . . . . . . . . . . . 1 1.2 Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 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 a proof . . . . . . . . . . . . . . . . . 7

A Chores 8 A.1 The name of the page . . . . . . . . . . . . . . . . . . . . . . . . 8 A.2 Variables of Peano arithmetic . . . . . . . . . . . . . . . . . . . . 8 A.3 TEX definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 A.4 Test . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 A.5 Priority table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

B Index 18

C Bibliography 22

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}.

1[˙0 =^{pyk} “peano zero”] 2[x′ =^{pyk} “∗ peano succ”] 3[x ˙+ y =^{pyk} “∗ peano plus ∗”] 4[x ˙· y =^{pyk} “∗ peano times ∗”]

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.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.

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 ∗”]

15[ẋ =^{pyk} “∗ peano var”]

16[x^{P} =^{pyk} “∗ is peano var”]

17[ȧ =^{pyk} “peano a”]

[ṅ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.

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

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

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: ( ˙¬ 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.

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

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

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):

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} ẋ ;

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

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}.

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′: ( ˙¬ B ˙⇒ ˙¬ A) ˙⇒ ( ˙¬ B ˙⇒ A) ˙⇒ B] [S′ rule A4′: ∀C: ∀A: ∀X: ∀B: ⌈A⌉≡⟨⌈B⌉|⌈X ⌉ := ⌈C⌉⟩ ⊢⊢ ˙∀X: B ˙⇒ A]

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

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

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

1.6 Restatement of lemma and a 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  □

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

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 [ḃ]^{60}, [ċ]^{61}, [ḋ]^{62}, [ė]^{63}, [ḟ]^{64}, [ġ]^{65}, [ḣ]^{66}, [i̇]^{67}, [j̇]^{68}, [k̇]^{69}, [l̇]^{70}, [ṁ]^{71}, [ṅ]^{72}, [ȯ]^{73}, [ṗ]^{74}, [q̇]^{75}, [ṙ]^{76}, [ṡ]^{77}, [ṫ]^{78}, [u̇]^{79}, [v̇]^{80}, [ẇ]^{81}, [ẋ]^{82}, [ẏ]^{83}, and [ż]^{84} to denote variables of Peano arithmetic:

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

60[ḃ =^{pyk} “peano b”] 61[ċ =^{pyk} “peano c”] 62[ḋ =^{pyk} “peano d”] 63[ė =^{pyk} “peano e”] 64[ḟ =^{pyk} “peano f”] 65[ġ =^{pyk} “peano g”] 66[ḣ =^{pyk} “peano h”] 67[i̇ =^{pyk} “peano i”] 68[j̇ =^{pyk} “peano j”] 69[k̇ =^{pyk} “peano k”] 70[l̇ =^{pyk} “peano l”] 71[ṁ =^{pyk} “peano m”] 72[ṅ =^{pyk} “peano n”] 73[ȯ =^{pyk} “peano o”] 74[ṗ =^{pyk} “peano p”] 75[q̇ =^{pyk} “peano q”] 76[ṙ =^{pyk} “peano r”] 77[ṡ =^{pyk} “peano s”] 78[ṫ =^{pyk} “peano t”] 79[u̇ =^{pyk} “peano u”] 80[v̇ =^{pyk} “peano v”] 81[ẇ =^{pyk} “peano w”] 82[ẋ =^{pyk} “peano x”] 83[ẏ =^{pyk} “peano y”] 84[ż =^{pyk} “peano z”]

A.3 TEX definitions

[˙0 =^{tex} “

\dot{0}”]

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

’”]

[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)’”]

[ḃ =^{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}(∗, ∗, ∗, ∗)], [˙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)′]; 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 [∗ @ ∗], [∗ ⊳ ∗], [∗ ⊳ ⊳ ∗], [∗ ≫ ∗]; 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

* is peano var [x^{P}], 2

* peano and * [x ˙∧ y], 2

* peano iff * [x ˙⇔ y], 2

* peano imply * [x ˙⇒ y], 2

* peano is * [x =^{p} y], 2

* peano or * [x ˙∨ y], 2

* peano plus * [x ˙+ y], 1

* peano succ [x′], 1

* peano times * [x ˙· y], 1

* peano var [ẋ], 2 [x ˙∧ y] * peano and *, 2 [x ˙⇔ y] * peano iff *, 2 [x ˙⇒ y] * peano imply *, 2 [x ˙∨ y] * peano or *, 2 [x ˙+ y] * peano plus *, 1 [x′] * peano succ, 1 [x ˙· y] * peano times *, 1 [ẋ] * peano var, 2 [ ˙∀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, 1

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, 2 axiom a five [A5], 4 axiom a four [A4], 4 axiom a one [A1], 4 axiom a three [A3], 4 axiom a two [A2], 4 axiom prime a five [A5′], 6 axiom prime a four [A4′], 6 axiom prime a one [A1′], 6 axiom prime a three [A3′], 6 axiom prime a two [A2′], 6 axiom prime s eight [S8′], 6 axiom prime s five [S5′], 6 axiom prime s four [S4′], 6 axiom prime s nine [S9′], 6 axiom prime s one [S1′], 6 axiom prime s seven [S7′], 6 axiom prime s six [S6′], 6 axiom prime s three [S3′], 6 axiom prime s two [S2′], 6 axiom s eight [S8], 4 axiom s five [S5], 4 axiom s four [S4], 4 axiom s nine [S9], 4 axiom s one [S1], 4 axiom s seven [S7], 4 axiom s six [S6], 4 axiom s three [S3], 4 axiom s two [S2], 4

b: [ḃ] peano b, 8

c: [ċ] peano c, 8

d: [ḋ] peano d, 8

e: [ė] peano e, 8

f: [ḟ] peano f, 8 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, 8 Gen’: [Gen′] rule prime gen, 6 Gen: [Gen] rule gen, 4

h: [ḣ] peano h, 8

i: [i̇] peano i, 8

j: [j̇] peano j, 8

k: [k̇] peano k, 8

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

m: [ṁ] peano m, 8 MP’: [MP′] rule prime mp, 6 MP: [MP] rule mp, 4

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

o: [ȯ] peano o, 8

P: [x^{P}] * is peano var, 2 p: [x =^{p} y] * peano is *, 2 p: [ṗ] peano p, 8 peano a [ȧ], 2 peano all * indeed * [ ˙∀x: y], 2 peano b [ḃ], 8 peano c [ċ], 8 peano d [ḋ], 8 peano e [ė], 8 peano exist * indeed * [ ˙∃x: y], 2 peano f [ḟ], 8 peano free * set * to * end free [ḟree⟨a, x := b⟩]3 peano free star * set * to * end free [ḟree^{∗}⟨a, x := b⟩]3 peano g [ġ], 8 peano h [ḣ], 8 peano i [i̇], 8 peano j [j̇], 8 peano k [k̇], 8 peano l [l̇], 8 peano m [ṁ], 8 peano n [ṅ], 8 peano nonfree * in * end nonfree [ṅonfree(x, y)], 2 peano nonfree star * in * end nonfree [ṅonfree^{∗}(x, y)], 3 peano not * [ ˙¬ x], 2 peano o [ȯ], 8 peano one [˙1], 2 peano p [ṗ], 8 peano q [q̇], 8 peano r [ṙ], 8 peano s [ṡ], 8 peano sub * is * where * is * end sub [a≡⟨b, x := c⟩]3 peano sub star * is * where * is * end sub [a≡⟨^{∗}b, x := c⟩]3 peano t [ṫ], 8 peano two [˙2], 2 peano u [u̇], 8 peano v [v̇], 8 Peano variable, 2 peano w [ẇ], 8 peano x [ẋ], 8 peano y [ẏ], 8 peano z [ż], 8 peano zero [˙0], 1

q: [q̇] peano q, 8

r: [ṙ] peano r, 8 rule gen [Gen], 4 rule mp [MP], 4 rule prime gen [Gen′], 6 rule prime mp [MP′], 6

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, 6 S4: [S4] axiom s four, 4 S5’: [S5′] axiom prime s five, 6 S5: [S5] axiom s five, 4 S6’: [S6′] axiom prime s six, 6 S6: [S6] axiom s six, 4 S7’: [S7′] axiom prime s seven, 6 S7: [S7] axiom s seven, 4 S8’: [S8′] axiom prime s eight, 6 S8: [S8] axiom s eight, 4 S9’: [S9′] axiom prime s nine, 6 S9: [S9] axiom s nine, 4 s: [ṡ] peano s, 8 S: [S] system s, 4 system prime s [S′], 6 system s [S], 4

t: [ṫ] peano t, 8

u: [u̇] peano u, 8

v: [v̇] peano v, 8 variable, Peano, 2

w: [ẇ] peano w, 8

x: [ẋ] peano x, 8

y: [ẏ] peano y, 8

z: [ż] peano z, 8

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.