Formal Logic

Lasse Nielsen & Morten Ib Nielsen

Department of Computer Science, University of Copenhagen

July 7, 2006

1 Initial remarks

Initially we planned to show a simple result of Group Theory namely the uniqueness of the neutral element. Our idea was to develop propositional logic and predicate calculus first. Based on these we planned to develop the axiomatic set theory ZFC and finally when we had sets we could define groups. Unfortunately it turned out that this was much more cumbersome than we thought both because we are newcommers to Logiweb^{TM}and also because core Logiweb^{TM}is very low level. Being newcommers to Logiweb^{TM}we have used a lot of time trying to find out how to use the system. This hasn’t been easy due to the total absence of a hands on users manual. Thus we wasted a lot of time early on trying to parse other peoples code from earlier years in order to understand how to use pyk (the language used to construct proofs ect. in Logiweb^{TM}). This was a very frustrating and non-trivial task since this years pyk syntax is different from earlier years! A lot of emailing back and forth with Klaus Grue helped us, but progress was slow. Very late in the course we had the oportunity to sit down with Klaus in a kind of assisted programming session, where Klaus helped us with our problems as they occured - this was very rewarding. After that we revised our goals with respect to this project and we found that even though we were now able to prove things in Logiweb^{TM}our initial goal was out of range because of the assembler like nature of our predicate calculus. Instead we decided to take the first step towards a more high level interface to our predicate calculus.

2 Conclusion

In this report we define .... todo Mainly we have experienced that Logiweb^{TM}is very Soon it turned that it wasn’t as easy as we thought to master Logiweb^{TM}.

3 Introduction

In this report we set out to formally prove a simple result of Group Theory namely:

Theorem 3.1 Let e be a neutral element of a Group G then e is unique. Thus we can talk about the neutral element of a Group G.

The theorem above is very loosely formulated. In this report we set out to formalize the theorem and give a formal proof of it’s correctness. In order to do this we need to do a lot of other work. First in XXTODO we define Propositional Calculus and then in MMTODO we define First order Predicate Calculus. Then using this we define ZFC set theory in YYTODO and finally having set theory available we can define a Group in ZZTODO. Then in WWTODO we restate the above theorem in a formal setting and we give a formal proof of it’s correctness.

TODO mere jalla.

4 First order predicate calculus

Based on mathworld^{1} and thus on Kleene (2002) we define first-order predicate calculus below. We note that the axioms 1 through 10 together with the inference rule modus ponens constitutes the propositional calculus.

Our definitions are not excately like those found on Mathworld. The reason is that we have made ⇒ right associative this means that F ⇒ G ⇒ F really means F ⇒ (G ⇒ F) below.

The [Theory pred calc] contains the following axioms

1. [pred calc rule pc1: ΠF, G: F ⇒ G ⇒ F]

2. [pred calc rule pc2: ΠF, G, H: (F ⇒ G) ⇒ (F ⇒ G ⇒ H) ⇒ F ⇒ H]

3. [pred calc rule pc3: ΠF, G: F ⇒ G ⇒ F ∧ G]

4. [pred calc rule pc4: ΠF, G: F ⇒ F ∨ G]

5. [pred calc rule pc5: ΠF, G: F ⇒ G ∨ F]

6. [pred calc rule pc6: ΠF, G: F ∧ G ⇒ F]

7. [pred calc rule pc7: ΠF, G: F ∧ G ⇒ G]

8. [pred calc rule pc8: ΠF, G, H: (F ⇒ G) ⇒ (H ⇒ G) ⇒ F ∨ H ⇒ G]

9. [pred calc rule pc9: ΠF, G: (F ⇒ G) ⇒ (F ⇒ ¬G) ⇒ ¬F]

10. [pred calc rule pc10: ΠF: ¬¬F ⇒ F]

11. [pred calc rule pc11: ΠX , R, G, F: ⟨H≡F|X:=R⟩ ⊢⊢ ∀X . (F) ⇒ H] 12. [pred calc rule pc12: ΠX , R, G, F: ⟨H≡F|X:=R⟩ ⊢⊢ H ⇒ ∃X . (F)] We note that in first order predicate calculus metavariables used in functions

1http://mathworld.wolfram.com/First-OrderLogic.html.

F and predicates P are object metavariables.

The only proof rule in [Theory pred calc] is Modus Ponens which says • [pred calc rule pcmp: ΠF, G: F ⊢ F ⇒ G ⊢ G]

• [pred calc rule pcia: ΠF, G, X : X #G ⊢⊢ G ⇒ F ⊢ G ⇒ ∀X . (F)]

• [pred calc rule pcie: ΠF, G, X : X #G ⊢⊢ F ⇒ G ⊢ ∃X . (F) ⇒ G]

• [pred calc rule pcdeduction: ΠA, B: Ded(A, B) ⊢⊢ A ⊢ B]

todo hvorfor tilfoejer vi deduction. bemaerk pcmp er imply elim mens pcded er imply intro

4.1 Deduction lemma

Lemma 4.1 [pred calc lemma pcded: ΠF, G: (F ⊢ G) ⊢ F ⇒ G]

pred calc proof of pcded:
L01: Arbitrary ≫  F, G  ;
L02: Premise ≫  F ⊢ G  ;
L03: Block ≫  Begin  ;
L04: Arbitrary ≫  F, G  ;
L05: Premise ≫  F  ;
L06: L02 ⊳ L05 ≫  G  ;
L07: Block ≫  End  ;
L08: pcdeduction ⊳ L07 ≫  F ⇒ G  □

4.2 A little proof

Below we make some small proofs just to demonstrate how to do it but also in order to test our definitions above. Lemma 4.2 [pred calc lemma trivia: ∀F: F ⇒ F]

pred calc proof of trivia:
L01: Arbitrary ≫  F  ;
L02: pc2 ≫  {(F ⇒ F ⇒ F) ⇒ (F ⇒ (F ⇒ \atop F) ⇒ F) ⇒ F ⇒ F  ;}
L03: pc1 ≫  F ⇒ F ⇒ F  ;
L04: pcmp ⊳ L03 ⊳ L02 ≫  {(F ⇒ (F ⇒ F) ⇒ F) ⇒ F ⇒ \atop F  ;}
L05: pc1 ≫  F ⇒ (F ⇒ F) ⇒ F  ;
L06: pcmp ⊳ L05 ⊳ L04 ≫  F ⇒ F  □

Lemma 4.3 (Repetition) [pred calc lemma repeat: ΠF: F ⊢ F]

pred calc proof of repeat:
L01: Arbitrary ≫  F  ;
L02: Premise ≫  F  ;
L03: trivia ≫  F ⇒ F  ;
L04: pcmp ⊳ L02 ⊳ L03 ≫  F  □

Lemma 4.4 [pred calc lemma iatest: ΠG, Y: Y#G ⊢⊢ G ⇒ ∀Y. (Y ⇒ G)]

pred calc proof of iatest:
L01: Arbitrary ≫  G, Y  ;
L02: Side-condition ≫  Y#G  ;
L03: pc1 ≫  G ⇒ Y ⇒ G  ;
L04: pcia ⊳ ⊳ L02 ⊳ L03 ≫  G ⇒ ∀Y. (Y ⇒ G)  □

5 Natural deduction

TODO skriv noget tekst Lemma 5.1 [pred calc lemma andintro: ΠF, G: F ⊢ G ⊢ F ∧ G]

pred calc proof of andintro:
L01: Arbitrary ≫  F, G  ;
L02: Premise ≫  F  ;
L03: Premise ≫  G  ;
L04: pc3 ≫  F ⇒ G ⇒ F ∧ G  ;
L05: pcmp ⊳ L02 ⊳ L04 ≫  G ⇒ F ∧ G  ;
L06: pcmp ⊳ L03 ⊳ L05 ≫  F ∧ G  □

Lemma 5.2 [pred calc lemma andelim1: ΠF, G: F ∧ G ⊢ F]

pred calc proof of andelim1:
L01: Arbitrary ≫  F, G  ;
L02: Premise ≫  F ∧ G  ;
L03: pc6 ≫  F ∧ G ⇒ F  ;
L04: pcmp ⊳ L02 ⊳ L03 ≫  F  □

Lemma 5.3 [pred calc lemma andelim2: ΠF, G: F ∧ G ⊢ G]

pred calc proof of andelim2:
L01: Arbitrary ≫  F, G  ;
L02: Premise ≫  F ∧ G  ;
L03: pc7 ≫  F ∧ G ⇒ G  ;
L04: pcmp ⊳ L02 ⊳ L03 ≫  G  □

Lemma 5.4 [pred calc lemma orintro1: ΠF, G: F ⊢ F ∨ G]

pred calc proof of orintro1:
L01: Arbitrary ≫  F, G  ;
L02: Premise ≫  F  ;
L03: pc4 ≫  F ⇒ F ∨ G  ;
L04: pcmp ⊳ L02 ⊳ L03 ≫  F ∨ G  □

Lemma 5.5 [pred calc lemma orintro2: ΠF, G: G ⊢ F ∨ G]

pred calc proof of orintro2:
L01: Arbitrary ≫  F, G  ;
L02: Premise ≫  G  ;
L03: pc5 ≫  G ⇒ F ∨ G  ;
L04: pcmp ⊳ L02 ⊳ L03 ≫  F ∨ G  □

Lemma 5.6 [pred calc lemma orelim: ΠF, G, H: F ∨ G ⊢ (F ⊢ H) ⊢ (G ⊢ H) ⊢ H]

pred calc proof of orelim:
L01: Arbitrary ≫  F, G, H  ;
L02: Premise ≫  F ∨ G  ;
L03: Premise ≫  F ⊢ H  ;
L04: Premise ≫  G ⊢ H  ;
L05: pcded ⊳ L03 ≫  F ⇒ H  ;
L06: pcded ⊳ L04 ≫  G ⇒ H  ;
L07: pc8 ≫  {(F ⇒ H) ⇒ (G ⇒ H) ⇒ F ∨ \atop G ⇒ H  ;}
L08: pcmp ⊳ L05 ⊳ L07 ≫  (G ⇒ H) ⇒ F ∨ G ⇒ H  ;
L09: pcmp ⊳ L06 ⊳ L08 ≫  F ∨ G ⇒ H  ;
L10: pcmp ⊳ L02 ⊳ L09 ≫  H  □

TODO lemma changed from natural deduction!!! skriv afsnit om det.

Lemma 5.7 [pred calc lemma notintro: ΠF, G: (F ⊢ G) ⊢ (F ⊢ ¬G) ⊢ ¬F]

pred calc proof of notintro:
L01: Arbitrary ≫  F, G  ;
L02: Premise ≫  F ⊢ G  ;
L03: Premise ≫  F ⊢ ¬G  ;
L04: pcded ⊳ L02 ≫  F ⇒ G  ;
L05: pcded ⊳ L03 ≫  F ⇒ ¬G  ;
L06: pc9 ≫  (F ⇒ G) ⇒ (F ⇒ ¬G) ⇒ ¬F  ;
L07: pcmp ⊳ L04 ⊳ L06 ≫  (F ⇒ ¬G) ⇒ ¬F  ;
L08: pcmp ⊳ L05 ⊳ L07 ≫  ¬F  □

Lemma 5.8 [pred calc lemma notnotelim: ΠF: ¬¬F ⊢ F]

pred calc proof of notnotelim:
L01: Arbitrary ≫  F  ;

L02: Premise ≫  ¬¬F  ;
L03: pc10 ≫  ¬¬F ⇒ F  ;
L04: pcmp ⊳ L02 ⊳ L03 ≫  F  □

5.1 Derived theorems

Below we apply the theorems above to prove some other fairly standard rules. Lemma 5.9 [pred calc lemma mt: ΠF, G: F ⇒ G ⊢ ¬G ⊢ ¬F]

pred calc proof of mt:
L01: Arbitrary ≫  F, G  ;
L02: Premise ≫  F ⇒ G  ;
L03: Premise ≫  ¬G  ;
L04: Block ≫  Begin  ;
L05: Arbitrary ≫  F, G  ;
L06: Premise ≫  F  ;
L07: pcmp ⊳ L06 ⊳ L02 ≫  G  ;
L08: Block ≫  End  ;
L09: pcdeduction ⊳ L08 ≫  F ⊢ G  ;
L10: Block ≫  Begin  ;
L11: Arbitrary ≫  F, G  ;
L12: Premise ≫  F  ;
L13: repeat ⊳ L03 ≫  ¬G  ;
L14: Block ≫  End  ;
L15: pcdeduction ⊳ L14 ≫  F ⊢ ¬G  ;
L16: notintro ⊳ L09 ⊳ L15 ≫  ¬F  □

Lemma 5.10 [pred calc lemma notnotintro: ΠF: F ⊢ ¬¬F]

pred calc proof of notnotintro:
L01: Arbitrary ≫  F  ;
L02: Premise ≫  F  ;
L03: Block ≫  Begin  ;
L04: Arbitrary ≫  F  ;
L05: Premise ≫  F  ;
L06: Premise ≫  ¬F  ;
L07: repeat ⊳ L05 ≫  F  ;
L06: Block ≫  End  ;
L08: pcdeduction ⊳ L06 ≫  F ⇒ ¬F ⇒ F  ;
L09: pcmp ⊳ L02 ⊳ L08 ≫  ¬F ⇒ F  ;
L10: trivia ≫  ¬F ⇒ ¬F  ;
L11: pc9 ≫  {(¬F ⇒ F) ⇒ (¬F ⇒ ¬F) ⇒ \atop ¬¬F  ;}
L12: pcmp ⊳ L09 ⊳ L11 ≫  (¬F ⇒ ¬F) ⇒ ¬¬F  ;
L13: pcmp ⊳ L10 ⊳ L12 ≫  ¬¬F  □

Lemma 5.11 [pred calc lemma pbc: ΠF, G: (¬F ⊢ G) ⊢ (¬F ⊢ ¬G) ⊢ F]

pred calc proof of pbc:
L01: Arbitrary ≫  F, G  ;
L02: Premise ≫  ¬F ⊢ G  ;
L03: Premise ≫  ¬F ⊢ ¬G  ;
L04: notintro ⊳ L02 ⊳ L03 ≫  ¬¬F  ;
L05: notnotelim ⊳ L04 ≫  F  □

5.2 Law of the Excluded Middle

In this section we prove the Law of the Excluded Middle. Theorem 5.12 [pred calc lemma lem: ΠF: F ∨ ¬F]

pred calc proof of lem:
L01: Arbitrary ≫  F  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  F  ;
L04: Premise ≫  ¬(F ∨ ¬F)  ;
L05: Block ≫  Begin  ;
L06: Arbitrary ≫  F  ;
L07: Premise ≫  F  ;
L08: orintro1 ⊳ L07 ≫  F ∨ ¬F  ;
L09: Block ≫  End  ;
L10: pcdeduction ⊳ L09 ≫  F ⊢ F ∨ ¬F  ;
L11: Block ≫  Begin  ;
L12: Arbitrary ≫  F  ;
L13: Premise ≫  F  ;
L14: repeat ⊳ L04 ≫  ¬(F ∨ ¬F)  ;
L15: Block ≫  End  ;
L16: pcdeduction ⊳ L15 ≫  F ⊢ ¬(F ∨ ¬F)  ;
L17: notintro ⊳ L10 ⊳ L16 ≫  ¬F  ;
L18: orintro2 ⊳ L17 ≫  F ∨ ¬F  ;
L19: Block ≫  End  ;
L20: pcdeduction ⊳ L19 ≫  ¬(F ∨ ¬F) ⊢ F ∨ ¬F  ;
L21: Block ≫  Begin  ;
L22: Arbitrary ≫  F  ;
L23: Premise ≫  ¬(F ∨ ¬F)  ;
L24: repeat ⊳ L23 ≫  ¬(F ∨ ¬F)  ;
L25: Block ≫  End  ;
L26: pcdeduction ⊳ L25 ≫  ¬(F ∨ ¬F) ⊢ ¬(F ∨ ¬F)  ;
L27: notintro ⊳ L20 ⊳ L26 ≫  ¬¬(F ∨ ¬F)  ;
L28: notnotelim ⊳ L27 ≫  F ∨ ¬F  □

A Pyk definitions

([pred calc →^{pyk} “pred calc”]

[pc1 →^{pyk} “pc1”]

[pc2 →^{pyk} “pc2”]

[pc3 →^{pyk} “pc3”]

[pc4 →^{pyk} “pc4”]

[pc5 →^{pyk} “pc5”]

[pc6 →^{pyk} “pc6”]

[pc7 →^{pyk} “pc7”]

[pc8 →^{pyk} “pc8”]

[pc9 →^{pyk} “pc9”]

[pc10 →^{pyk} “pc10”]

[pc11 →^{pyk} “pc11”]

[pc12 →^{pyk} “pc12”]

[pcmp →^{pyk} “pcmp”] [pcded →^{pyk} “pcded”] [pcia →^{pyk} “pcia”] [pcie →^{pyk} “pcie”] [pcdeduction →^{pyk} “pcdeduction”] [trivia →^{pyk} “trivia”] [iatest →^{pyk} “iatest”] [andintro →^{pyk} “andintro”] [andelim1 →^{pyk} “andelim1”] [andelim2 →^{pyk} “andelim2”] [orintro1 →^{pyk} “orintro1”] [orintro2 →^{pyk} “orintro2”] [orelim →^{pyk} “orelim”] [notintro →^{pyk} “notintro”] [notnotintro →^{pyk} “notnotintro”] [notnotelim →^{pyk} “notnotelim”]

[mt →^{pyk} “mt”]

[pbc →^{pyk} “pbc”] [repeat →^{pyk} “repeat”] [lem →^{pyk} “lem”] [∗ ≡ ∗ →^{pyk} “" setequiv "”] [∗ = ∗ →^{pyk} “" setequals "”]

[¬∗ →^{pyk} “lnot "”]

[∗ ∧ ∗ →^{pyk} “" land "”]

[∗ ∨ ∗ →^{pyk} “" lor "”]

[∀ ∗ . (∗) →^{pyk} “forall " dot " end forall”] [∃ ∗ . (∗) →^{pyk} “exists " dot " end exists”] [∗ ∈ ∗ →^{pyk} “" setin "”] [problemone →^{pyk} “problemone”] )^{p}

B Tex definitions

• [¬x =^{tex} “\neg #1.”]

• [x ∧ y =^{tex} “#1. \wedge #2.”]

• [x ∨ y =^{tex} “#1. \vee #2.”]

• [x ⇒ y =^{tex} “#1. \Rightarrow #2.”]

• [∀y. (b) =^{tex} “\forall #1. . \left(#2.\right)”]

• [∃y. (b) =^{tex} “\exists #1. . \left(#2.\right)”]

• [y ∈ b =^{tex} “#1. \in #2.”]

• [y ≡ b =^{tex} “#1. \equiv #2.”]

• [y = b =^{tex} “#1. = #2.”]

C Priority table

Priority table Preassociative [problemone], [base], [bracket ∗ end bracket], [big bracket ∗ end bracket], [ $ ∗ $ ], [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̃^{∗}(∗, ∗, ∗)], [(∗)], [(∗)], [display(∗)], [statement(∗)], [[∗]^{·}], [[∗]^{−}], [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}(∗, ∗)], [check], [[∗ =^{∘} ∗]], [RootVisible(∗)], [A], [R], [C], [T], [L], [\{∗\}], [\overline{∗}], [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], [⟨∗≡ ∗ | ∗:=∗⟩], [⟨∗≡^{0} ∗ | ∗:=∗⟩], [⟨∗≡^{1} ∗ | ∗:=∗⟩], [⟨∗≡^{∗} ∗ | ∗:=∗⟩], [Ded(∗, ∗)], [Ded_{0}(∗, ∗)], [Ded_{1}(∗, ∗, ∗)], [Ded_{2}(∗, ∗, ∗)], [Ded_{3}(∗, ∗, ∗, ∗)], [Ded_{4}(∗, ∗, ∗, ∗)], [Ded_{4}^{∗}(∗, ∗, ∗, ∗)], [Ded_{5}(∗, ∗, ∗)], [Ded_{6}(∗, ∗, ∗, ∗)], [Ded_{6}^{∗}(∗, ∗, ∗, ∗)], [Ded_{7}(∗)], [Ded_{8}(∗, ∗)], [Ded_{8}^{∗}(∗, ∗)], [S], [Neg], [MP], [Gen], [Ded], [S1], [S2], [S3], [S4], [S5], [S6], [S7], [S8], [S9], [Repetition], [A1′], [A2′], [A4′], [A5′], [Prop 3.2a], [Prop 3.2b], [Prop 3.2c], [Prop 3.2d], [Prop 3.2e_{1}], [Prop 3.2e_{2}], [Prop 3.2e], [Prop 3.2f_{1}], [Prop 3.2f_{2}], [Prop 3.2f], [Prop 3.2g_{1}], [Prop 3.2g_{2}], [Prop 3.2g], [Prop 3.2h_{1}], [Prop 3.2h_{2}], [Prop 3.2h], [Block_{1}(∗, ∗, ∗)], [Block_{2}(∗)], [pred calc], [pc1], [pc2], [pc3], [pc4], [pc5], [pc6], [pc7], [pc8], [pc9], [pc10], [pc11], [pc12], [pcmp], [pcded], [pcia], [pcie], [pcdeduction], [trivia], [iatest], [andintro], [andelim1], [andelim2], [orintro1], [orintro2], [orelim], [notintro], [notnotintro], [notnotelim], [mt], [pbc], [repeat], [lem]; Preassociative [∗ {∗}], [∗/indexintro(∗, ∗, ∗, ∗)], [∗/intro(∗, ∗, ∗)], [∗/bothintro(∗, ∗, ∗, ∗, ∗)], [∗/nameintro(∗, ∗, ∗, ∗)], [∗′], [∗[ ∗]], [∗[∗→∗]], [∗[∗⇒∗]], [∗0], [∗1], [0b], [∗-color(∗)], [∗-color^{∗}(∗)], [∗^{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^{∗}}], [∗^{hide}]; 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 ∗], [MacroIndent(∗)]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; Preassociative [∗′]; Preassociative [∗ ’ ∗], [∗ ‘ ∗]; 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} ∗], [∗ < ∗], [∗ <′ ∗], [∗ ≤′ ∗], [∗ = ∗], [∗ ≠ ∗], [∗^{var}], [∗#^{0}∗], [∗#^{1}∗], [∗#^{∗}∗], [∗ ≡ ∗], [∗ = ∗]; Preassociative [¬∗], [¬∗]; Preassociative [∗ ∧ ∗], [∗ ¨∧ ∗], [∗ ˜∧ ∗], [∗ ∧_{c} ∗], [∗ ∧ ∗]; Preassociative [∗ ∨ ∗], [∗ ∥ ∗], [∗ ¨∨ ∗], [∗ ∨ ∗]; Preassociative [∃∗: ∗], [∀∗: ∗], [∀_{obj}∗: ∗], [∀ ∗ . (∗)], [∃ ∗ . (∗)]; Postassociative [∗ ¨⇒ ∗], [∗ ⇒ ∗], [∗ ⇔ ∗]; Postassociative [∗ : ∗], [∗ spy ∗], [∗!∗]; Preassociative

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

Preassociative [λ ∗ .∗], [Λ ∗ .∗], [Λ∗], [if ∗ then ∗ else ∗], [let ∗ = ∗ in ∗], [let ∗ ¨= ∗ in ∗]; Preassociative [∗#∗]; 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 ≫ ∗ = ∗; ∗], [Begin ∗; ∗ : End; ∗], [Last block line ∗ ≫ ∗; ], [Arbitrary ≫ ∗; ∗]; Postassociative [∗ | ∗]; Postassociative [∗ , ∗], [∗[ ∗]∗]; Preassociative [∗&∗], [→]; Preassociative [∗\\∗], [∗ linebreak[4] ∗], [∗\\∗]; Preassociative [∗ ∈ ∗]; End table

13