Introduction to Logiweb

Klaus Grue

GRD-2005-06-02.UTC:10:16:52.703168

Contents

1 Peano arithmetic 1 1.1 Introduction of new constructs . . . . . . . . . . . . . . . . . . . 1 1.2 The constructs of Peano arithmetic . . . . . . . . . . . . . . . . . 2 1.3 Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.4 Axiomatic system . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.5 A lemma and a proof . . . . . . . . . . . . . . . . . . . . . . . . . 5

A Chores 6 A.1 The name of the page . . . . . . . . . . . . . . . . . . . . . . . . 6 A.2 Variables of Peano arithmetic . . . . . . . . . . . . . . . . . . . . 6 A.3 TEX definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 A.4 Test . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 A.5 Priority table . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

B Index 15

C Bibliography 19

1 Peano arithmetic

This Logiweb page [1] defines Peano arithmetic.

1.1 Introduction of new constructs

The following constructs allow to introduce a new construct (“introduce” in the normal sense of the word, not in the sense of a Logiweb revelation). The constructs allow to define the pyk aspect [p] and tex aspect [t] of a new construct [x] and also makes two entries in the index. The first of the constructs below adds the text [i] in front of one of the index entries.

[intro(x, i, p, t) ¨= [x =^{pyk} p][x =^{tex} t]]^{1}

1[intro(x, i, p, t) =^{pyk} “intro ∗ index ∗ pyk ∗ tex ∗ end intro”]

[intro(x, p, t) ¨= [x =^{pyk} p][x =^{tex} t]]^{2}

1.2 The constructs of Peano arithmetic

Terms of Peano arithmetic are constructed from zero [˙0]^{3}, successor [x′]^{4}, plus [x ˙+ y]^{5}, and times [x ˙· y]^{6}.

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

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

[˙1 ¨= ˙0′]
[˙2 ¨= ˙1′]
[x ˙∧ y ¨= ˙¬ (x ˙⇒ ˙¬ y)]
[x ˙∨ y ¨= ˙¬ x ˙⇒ y]
[x ˙⇔ y ¨= (x ˙⇒ y) ˙∧ (y ˙⇒ x)]
[ ˙∃x: y ¨= ˙¬ ˙∀x: ˙¬ y]

1.3 Variables

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

2[intro(x, p, t) =^{pyk} “intro ∗ pyk ∗ tex ∗ end intro”]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[ȧ ¨= ȧ]

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

[ṅonfree(x, y)]^{20} is true if the Peano variable [x] does not occur free in the Peano term/formula [y]. [ṅonfree^{∗}(x, y)]^{21} 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⟩]^{22} is true if the substitution [⟨a |x:= b⟩] is free. [ḟree^{∗}⟨a|x := b⟩]^{23} 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⟩]^{24} is true if [a] equals [⟨b |x:= c⟩]. [a≡⟨^{∗}b|x := c⟩]^{25} 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⟩]

19[ȧ =^{pyk} “peano a”] 20[ṅonfree(x, y) =^{pyk} “peano nonfree ∗ in ∗ end nonfree”] 21[ṅonfree^{∗}(x, y) =^{pyk} “peano nonfree star ∗ in ∗ end nonfree”] 22[ḟree⟨a|x := b⟩ =^{pyk} “peano free ∗ set ∗ to ∗ end free”] 23[ḟree^{∗}⟨a|x := b⟩ =^{pyk} “peano free star ∗ set ∗ to ∗ end free”] 24[a≡⟨b|x := c⟩ =^{pyk} “peano sub ∗ is ∗ where ∗ is ∗ end sub”] 25[a≡⟨^{∗}b|x := c⟩ =^{pyk} “peano sub star ∗ is ∗ where ∗ is ∗ end sub”]

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

1.4 Axiomatic system

System [S]^{26} of Mendelson [2] expresses Peano arithmetic. It comprises the axioms [A1]^{27}, [A2]^{28}, [A3]^{29}, [A4]^{30}, and [A5]^{31} and inference rules [MP]^{32} and [Gen]^{33} of first order predicate calculus. Furthermore, it comprises the proper axioms [S1]^{34}, [S2]^{35}, [S3]^{36}, [S4]^{37}, [S5]^{38}, [S6]^{39}, [S7]^{40}, [S8]^{41}, and [S9]^{42}. 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 [A] which the system can currently guess comes first. At a later stage, when a planned generalisation of the conclusion tactic has been implemented, the system will be able to guess [X] and [B] also. Guessing [C] would require a separate tactic.

[S rule A4: ∀C: ∀X: ∀B: ∀A: 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]

26[S =^{pyk} “system s”]

27[A1 =^{pyk} “axiom a one”]

28[A2 =^{pyk} “axiom a two”]

29[A3 =^{pyk} “axiom a three”]

30[A4 =^{pyk} “axiom a four”]

31[A5 =^{pyk} “axiom a five”]

32[MP =^{pyk} “rule mp”]

33[Gen =^{pyk} “rule gen”]

34[S1 =^{pyk} “axiom s one”]

35[S2 =^{pyk} “axiom s two”]

36[S3 =^{pyk} “axiom s three”]

37[S4 =^{pyk} “axiom s four”]

38[S5 =^{pyk} “axiom s five”]

39[S6 =^{pyk} “axiom s six”]

40[S7 =^{pyk} “axiom s seven”]

41[S8 =^{pyk} “axiom s eight”]

42[S9 =^{pyk} “axiom s nine”]

[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.5 A lemma and a proof

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

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

The first four lines of the proof has revealed an error in the conclusion tactic which has to be corrected before the proof will be accepted:

S proof of L3.2(a):

L01: S5 ≫  ȧ ˙+ ˙0 =^{p} ȧ  ;
L02: Gen ⊳ L01 ≫  ˙∀ȧ: ȧ ˙+ ˙0 =^{p} ȧ  ;

L03: A4 @ ẋ @ ȧ @

ȧ ˙+ ˙0 =^{p} ȧ @

ẋ ˙+ ˙0 =^{p} ẋ ≫

˙∀ȧ: ȧ ˙+ ˙0 =^{p} ȧ ˙⇒ ẋ ˙+ ˙0 =^{p} ẋ ;
L04: MP ⊳ L03 ⊳ L02 ≫  ẋ ˙+ ˙0 =^{p} ẋ  □

43[L3.2(a) =^{pyk} “lemma 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 [ḃ]^{44}, [ċ]^{45}, [ḋ]^{46}, [ė]^{47}, [ḟ]^{48}, [ġ]^{49}, [ḣ]^{50}, [i̇]^{51}, [j̇]^{52}, [k̇]^{53}, [l̇]^{54}, [ṁ]^{55}, [ṅ]^{56}, [ȯ]^{57}, [ṗ]^{58}, [q̇]^{59}, [ṙ]^{60}, [ṡ]^{61}, [ṫ]^{62}, [u̇]^{63}, [v̇]^{64}, [ẇ]^{65}, [ẋ]^{66}, [ẏ]^{67}, and [ż]^{68} to denote variables of Peano arithmetic:

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

44[ḃ =^{pyk} “peano b”] 45[ċ =^{pyk} “peano c”] 46[ḋ =^{pyk} “peano d”] 47[ė =^{pyk} “peano e”] 48[ḟ =^{pyk} “peano f”] 49[ġ =^{pyk} “peano g”] 50[ḣ =^{pyk} “peano h”] 51[i̇ =^{pyk} “peano i”] 52[j̇ =^{pyk} “peano j”] 53[k̇ =^{pyk} “peano k”] 54[l̇ =^{pyk} “peano l”] 55[ṁ =^{pyk} “peano m”] 56[ṅ =^{pyk} “peano n”] 57[ȯ =^{pyk} “peano o”] 58[ṗ =^{pyk} “peano p”] 59[q̇ =^{pyk} “peano q”] 60[ṙ =^{pyk} “peano r”] 61[ṡ =^{pyk} “peano s”] 62[ṫ =^{pyk} “peano t”] 63[u̇ =^{pyk} “peano u”] 64[v̇ =^{pyk} “peano v”] 65[ẇ =^{pyk} “peano w”] 66[ẋ =^{pyk} “peano x”] 67[ẏ =^{pyk} “peano y”] 68[ż =^{pyk} “peano z”]

A.3 TEX definitions

[intro(x, i, p, t) =^{tex} “\index{#2.: #3. @#2.: $[#1/tex name/tex.]$ #3.}% \index{#3. $[#1/tex name/tex.]$}% \tex{ $[#1/tex name/tex. \stackrel {\mathrm {tex}}{=} #4/tex name. ]$}$[ #1/tex name/tex.% ]$\footnote{$[#1/tex name/tex. \stackrel {\mathrm {pyk}}{=} #3/tex name. ]$}”]

[intro(x, i, p, t) =^{name} “ intro(#1. , #2. , #3. , #4. )”]

[intro(x, p, t) =^{tex} “\index{\alpha #2. @\back \makebox[20mm][l]{$[#1/tex name/tex.]$}#2.}% \index{#2. $[#1/tex name/tex.]$}% \tex{ $[#1/tex name/tex. \stackrel {\mathrm {tex}}{=} #3/tex name. ]$}$[ #1/tex name/tex.% ]$\footnote{$[#1/tex name/tex. \stackrel {\mathrm {pyk}}{=} #2/tex name. ]$}”]

[intro(x, p, t) =^{name} “ intro(#1. , #2. , #3. )”]

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

[ḃ =^{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}], [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}(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗, ∗)], [intro(∗, ∗, ∗)], [˙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)]; 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], 2

* peano succ [x′], 2

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

* peano var [ẋ], 2 [x^{P}] * is peano var, 2 [x ˙∧ y] * peano and *, 2 [x ˙⇔ y] * peano iff *, 2 [x ˙⇒ y] * peano imply *, 2 [x =^{p} y] * peano is *, 2 [x ˙∨ y] * peano or *, 2 [x ˙+ y] * peano plus *, 2 [x′] * peano succ, 2 [x ˙· y] * peano times *, 2 [ẋ] * peano var, 2

[A5] axiom a five, 4

[A4] axiom a four, 4

[A1] axiom a one, 4

[A3] axiom a three, 4

[A2] axiom a two, 4

[S8] axiom s eight, 4

[S5] axiom s five, 4

[S4] axiom s four, 4

[S9] axiom s nine, 4

[S1] axiom s one, 4

[S7] axiom s seven, 4

[S6] axiom s six, 4

[S3] axiom s three, 4

[S2] axiom s two, 4 [L3.2(a)] lemma l three two a, 5 [ȧ] peano a, 3 [ ˙∀x: y] peano all * indeed *, 2 [ḃ] peano b, 6 [ċ] peano c, 6 [ḋ] peano d, 6 [ė] peano e, 6 [ ˙∃x: y] peano exist * indeed *, 2 [ḟ] peano f, 6 [ġ] peano g, 6 [ḣ] peano h, 6 [i̇] peano i, 6 [j̇] peano j, 6 [k̇] peano k, 6 [l̇] peano l, 6 [ṁ] peano m, 6 [ṅ] peano n, 6 [ṅonfree(x, y)]peano nonfree * in * end nonfree, 3 [ṅonfree^{∗}(x, y)] peano nonfree star * in * end nonfree, 3 [ ˙¬ x] peano not *, 2 [ȯ] peano o, 6 [˙1] peano one, 2 [ṗ] peano p, 6 [q̇] peano q, 6 [ṙ] peano r, 6 [ṡ] peano s, 6 [ṫ] peano t, 6 [˙2] peano two, 2 [u̇] peano u, 6 [v̇] peano v, 6 [ẇ] peano w, 6 [ẋ] peano x, 6 [ẏ] peano y, 6 [ż] peano z, 6 [˙0] peano zero, 2

[Gen] rule gen, 4

[MP] rule mp, 4

[S] system s, 4

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

intro * index * pyk * tex * end intro [intro(x, i, p, t)], 1 intro * pyk * tex * end intro [intro(x, p, t)], 2 intro: [intro(x, i, p, t)] intro * index * pyk * tex * end intro, 1 intro: [intro(x, p, t)] intro * pyk * tex * end intro, 2

lemma l three two a [L3.2(a)], 5 peano a [ȧ], 3 peano all * indeed * [ ˙∀x: y], 2 peano b [ḃ], 6 peano c [ċ], 6 peano d [ḋ], 6 peano e [ė], 6 peano exist * indeed * [ ˙∃x: y], 2 peano f [ḟ], 6 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 [ġ], 6 peano h [ḣ], 6 peano i [i̇], 6 peano j [j̇], 6 peano k [k̇], 6 peano l [l̇], 6 peano m [ṁ], 6 peano n [ṅ], 6 peano nonfree * in * end nonfree [ṅonfree(x, y)], 3 peano nonfree star * in * end nonfree [ṅonfree^{∗}(x, y)], 3 peano not * [ ˙¬ x], 2 peano o [ȯ], 6 peano one [˙1], 2 peano p [ṗ], 6 peano q [q̇], 6 peano r [ṙ], 6 peano s [ṡ], 6 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 [ṫ], 6 peano two [˙2], 2 peano u [u̇], 6 peano v [v̇], 6 Peano variable, 2 peano w [ẇ], 6 peano x [ẋ], 6 peano y [ẏ], 6 peano z [ż], 6 peano zero [˙0], 2

rule gen [Gen], 4 rule mp [MP], 4

system s [S], 4

variable, Peano, 2

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.