Formal Logic

Lasse Nielsen & Morten Ib Nielsen

Department of Computer Science, University of Copenhagen

July 14, 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 newcomers to Logiweb^{TM} and also because core Logiweb^{TM} is very low level. Being newcomers 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 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 opportunity to sit down with Klaus in a kind of assisted programming session, where Klaus helped us with our problems as they occurred - 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

This Logiweb^{TM} page is an exam project on the course 202 Logik Spring 2006 at the Department of Computer Science, University of Copenhagen. The purpose with this project is to use Logiweb^{TM} to publish a machine checkable proof for a theorem of our choise - which we have done^{1}. Since both of us have backgrounds in mathematics and formal methods in computer science we started out having high ambitions. As hinted we had to revise our goals along the way for several reasons. Instead of doing a large and complicated proof we have decided to show how to use the Logiweb^{TM} system to define a theory (a set of axioms) and how to define and prove lemmas in a theory (both using axioms as well as already proved lemmas). Along the way we have explained key parts of the Logiweb^{TM} notation. It is our hope that this Logiweb^{TM} page will serve as a helping hand to future students on this course providing the getting started manual that we have been missing so much.

1This page has been verified and found correct by Logiweb^{TM} and is available at  http://www.diku.dk/hjemmesider/ansatte/grue/logiweb/20060417/home/mortenib/ finalversion/fixed/.

We start out defining a theory called pred calc containing one possible set of axioms and inference rules for the predicate calculus. Since these axioms are very low level we define, inspired by Natural Deduction (see [LiCS]), a set of higher level (and more intuitive) proof rules which we prove. Finally we use these higher level rules to prove lemma 6.6.

3 Introduction

This Logiweb^{TM} page is formally correct. This means that it has been verified and found correct by the Logiweb^{TM} proof engine. Therefore we can say that it is correct modulo errors in the proof engine. Is the content correct then? Well yes, but only in the sense that the lemmas we have proved are consequences of the axioms and proof rules we have introduced. There is no guarantee of soundness of our axioms and proof rules.

We have structured this document as follows. In section 4 we define the axioms and proof rules of predicate calculus. We conclude the section with two simple proofs namely the very (intuitively) obvious lemma trivia 4.1 and the lemma repeat 4.2. Then in section 5 we state and prove lemmas inspired by Natural Deduction. Finally in section 6 we use these lemmas to prove lemma 6.6. The appendix includes various Logiweb^{TM} dependent stuff like Tex definitions and Priority table but also our suggestions of how Logiweb^{TM} could be improved.

4 First order predicate calculus

Based on Mathworld^{2} 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 (pcmp) constitutes the propositional calculus. Our definitions are not exactly like those found on Mathworld for two reasons. First we have made ⇒ right associative in order to get rid of unnecessary parenthesis. This means that F ⇒ G ⇒ F really means F ⇒ (G ⇒ F) below. Second we had to express formulations such as in which x occurs free in a machine checkable way.

The [Theory pred calc] contains the following axioms:

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

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: X #R ⊢⊢ X #G ⊢⊢ ⟨G≡F|X:=R⟩ ⊢⊢ ∀X . (F) ⇒ G]

12. [pred calc rule pc12: ΠX , R, G, F: X #R ⊢⊢ X #G ⊢⊢ ⟨G≡F|X:=R⟩ ⊢⊢ G ⇒ ∃X . (F)]

The proof rules in the [Theory pred calc] are:

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

4.1 A conservative extension

The rule pcdeduction is not really a part of Predicate Calculus according to Mathworld but it is a conservative extension in the sense than we cannot prove anything using this rule that we cannot prove without it. We include it in order to make proofs shorter and thus easier to understand for humans. As a curiosity we cannot prove that pcdeduction is a conservative extension formally ^{3}.

3In a machine checkable way.

4.2 A troublesome extension

It seems fair to conclude B if both A ⊢ B and A are known. This is the proof rule modus ponens. Unfortunately Logiweb^{TM} does not allow the use of modus ponens on anything other than lemmas e.g. modus ponens cannot be used on line numbers in proofs. One of the aims of this project is to introduce and prove natural deduction like proof rules enabling the use of pred calc on a higher level. Since we cannot use line numbers with modus ponens we cannot prove the implication introduction rule (see [LiCS, p. 27]). Therefore we need to add the following rule as a proof rule in [Theory pred calc].

• [pred calc rule pcunsound: ΠF, G: (F ⊢ G) ⊢ F ⊢ G]

We have been told that this rule makes the system unsound, but we have not seen and cannot find an example of this. We have been told (by Klaus Grue via email) that it requires some special side conditions in order to be sound. Alas we have been unable to communicate with Klaus Grue in the week up to our deadline. Therefore we have been unable to ameliorate this deficiency but we are convinced that we only use the rule in sound ways. Given the right side conditions we expect that our proofs could be patched simply by adding these side conditions.

4.3 Notation

Some of the notation used above is most likely unfamiliar. So let’s spend a few paragraphs explaining it before we continue. The meaning of the axioms and proof rules above are of course given by their definition but in order to understand the definitions we need to explain the basic syntax (or at least the part of it we use) in Logiweb^{TM} definitions and proofs.

• The symbol Π is the for all meta quantifier.

• The symbol ⊢ is placed between two propositions. The meaning of A ⊢ B is that if A can be proved then so can B. ⊢ can be used sequentially in the way that A ⊢ B ⊢ C means if A can be proved, then if B can be proved, then so can C. That is if A and B can be proved then so can C.

• The symbol ▷ is placed between a rule and a line number. It is the opposite of ⊢ in the sense that if R is a rule saying that A ⊢ B and L is a line concluding A, then R ▷ L concludes B.

• Explanation of ≫. A line in a proof consists of the symbol ≫ with the use of a rule on the left, and the conclusion on the right. The example above would give the line R ▷ L ≫ B.

• The meaning of ⊩ is almost the same as ⊢. If the condition on the left evaluates to true, then the proposition on the right can be proved. The condition on the left of a ⊩ is a so called side-condition. The only side-conditions we use are expressed using substitution and ♯ (explained below).

• The ▷▷ symbol is used much like ▷, but it is the opposite of ⊩ instead of ⊢, thus the line number on the right of the symbol must conclude that the side-condition is fulfilled.

• The side-condition ⟨A ≡ B | C := D⟩ is fulfilled, if the proposition B where any occurrence of the meta-variable C is replaced by the proposition D is exactly equal to the proposition A. Another way to express this using a more common notation of substitution would be A ≡ B[D/C]. It is important to note that this substitution avoids variable capture. An example of why variable capture would be unsound is the propositional formula ∀x∃y : (x ∨ y) ∧ (¬x ∨ ¬y). We see that this is a tautology since the choice of y ≡ ¬x satisfies the formula. But if we substituted y for x in this formula then we would get an absurdity.

• The side-condition A♯B is fulfilled if the meta-variable A does not occur (free) in the proposition B.

4.4 Some small proofs

Having explained the syntax of definitions and proofs we continue with two simple but useful lemmas just to show how it is done. Lemma 4.1 is proved using only axioms and proof rules while the proof of lemma 4.2 uses the result of lemma 4.1 as well.

Lemma 4.1 [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.2 (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  □

5 Natural deduction

The axioms and proof rules in [Theory pred calc] constitutes a very low level proof system. In order to ameliorate this we introduce and prove some higher level (and more intuitive) proof rules. These proof rules are inspired by natural deduction as defined in [LiCS]. We conclude this section by justifying why we have replaced two rules from [LiCS] with a new rule.

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: implyintro ⊳ L03 ≫  F ⇒ H  ;
L06: implyintro ⊳ 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  □

Lemma 5.7 [pred calc lemma implyintro: ΠF, G: (F ⊢ G) ⊢ F ⇒ G]

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

Lemma 5.8 [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: implyintro ⊳ L02 ≫  F ⇒ G  ;
L05: implyintro ⊳ L03 ≫  F ⇒ ¬G  ;
L06: pc9 ≫  (F ⇒ G) ⇒ (F ⇒ ¬G) ⇒ ¬F  ;
L07: pcmp ⊳ L04 ⊳ L06 ≫  (F ⇒ ¬G) ⇒ ¬F  ;
L08: pcmp ⊳ L05 ⊳ L07 ≫  ¬F  □

Lemma 5.9 [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  □

Lemma 5.10 [pred calc lemma forallintro: ΠF, G, X : X #G∨¬G ⊢⊢ F ⊢ ∀X . (F)]

pred calc proof of forallintro:
L01: Arbitrary ≫  F, G, X  ;
L02: Side-condition ≫  X #G ∨ ¬G  ;
L03: Premise ≫  F  ;
L04: lem ≫  G ∨ ¬G  ;
L05: Block ≫  Begin  ;
L06: Arbitrary ≫  G, F  ;
L07: Premise ≫  G ∨ ¬G  ;
L08: repeat ⊳ L03 ≫  F  ;
L09: Block ≫  End  ;
L10: pcdeduction ⊳ L09 ≫  G ∨ ¬G ⇒ F  ;
L11: pcia ⊳ ⊳ L02 ⊳ L10 ≫  G ∨ ¬G ⇒ ∀X . (F)  ;
L12: pcmp ⊳ L04 ⊳ L11 ≫  ∀X . (F)  □

Remark 5.11 In lemma 5.10 we use the side condition X #G ∨ ¬G. We would like to use the equivalent X #G instead but we haven’t been able to find a way to prove the former side condition from the latter. Another example of reasoning about side conditions is the following. If we have ⟨G≡F|X:=R⟩ and X #R then it follows that X #G. Unfortunately we haven’t heard of any ways to reason about side conditions therefore we are forced to assume side conditions in lemmas whenever we need them even though they might be deductable.

Lemma 5.12 [pred calc lemma forallelim: ΠX , R, G, F: X #R ⊢⊢ X #G ⊢⊢ ⟨G≡F|X:=R⟩ ⊢⊢ ∀X . (F) ⊢ G]

pred calc proof of forallelim:
L01: Arbitrary ≫  X , R, G, F  ;
L02: Side-condition ≫  X #R  ;
L03: Side-condition ≫  X #G  ;
L04: Side-condition ≫  ⟨G≡F|X:=R⟩  ;
L05: pc11 ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳ L04 ≫  ∀X . (F) ⇒ G  ;
L06: Block ≫  Begin  ;
L07: Arbitrary ≫  X , G, F  ;
L08: Premise ≫  ∀X . (F)  ;
L09: pcmp ⊳ L08 ⊳ L05 ≫  G  ;
L10: Block ≫  End  ;
L11: pcdeduction ⊳ L10 ≫  ∀X . (F) ⊢ G  □

Lemma 5.13 [pred calc lemma existsintro: ΠX , R, G, F: X #R ⊢⊢ X #G ⊢⊢ ⟨G≡F|X:=R⟩ ⊢⊢ G ⊢ ∃X . (F)]

pred calc proof of existsintro:
L01: Arbitrary ≫  X , R, G, F  ;
L02: Side-condition ≫  X #R  ;

L03: Side-condition ≫  X #G  ;
L04: Side-condition ≫  ⟨G≡F|X:=R⟩  ;
L05: pc12 ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳ L04 ≫  G ⇒ ∃X . (F)  ;
L06: Block ≫  Begin  ;
L07: Arbitrary ≫  X , G, F  ;
L08: Premise ≫  G  ;
L09: pcmp ⊳ L08 ⊳ L05 ≫  ∃X . (F)  ;
L10: Block ≫  End  ;
L11: pcdeduction ⊳ L10 ≫  G ⊢ ∃X . (F)  □

Lemma 5.14 [pred calc lemma existselim: ΠX , F, G: X #G ⊢⊢ ∃X . (F) ⊢ (F ⊢ G) ⊢ G]

pred calc proof of existselim:
L01: Arbitrary ≫  X , F, G  ;
L02: Side-condition ≫  X #G  ;
L03: Premise ≫  ∃X . (F)  ;
L04: Premise ≫  F ⊢ G  ;
L05: implyintro ⊳ L04 ≫  F ⇒ G  ;
L06: pcie ⊳ ⊳ L02 ⊳ L05 ≫  ∃X . (F) ⇒ G  ;
L07: pcmp ⊳ L03 ⊳ L06 ≫  G  □

5.1 Derived lemmas

Below we apply the lemmas above together with the defining rules of [Theory pred calc] to prove some other fairly standard and very useful lemmas.

Lemma 5.15 (Modus Tollens) [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.16 [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.17 (Proof by Contradiction) [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  □

Lemma 5.18 (Law of the Excluded Middle) [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  □

5.2 A word on ⊥

The proof rules of natural deduction in [LiCS] uses bottom. Bottom represents the concept of unsoundness, that is it should be impossible to prove bottom in a sound logic. The way to prove bottom would be to prove any absurdity, that is for any proposition A to prove both A and not A. In [LiCS] this is captured in the proof rule \frac{¬A A}{⊥}. In [LiCS] bottom is used in two ways. First if you under the assumption of a proposition A can prove bottom then you can conclude that A is false, that is not A is true. In [LiCS] this is captured by the proof rule

\frac{A ; ⋮ ; ⊥}{¬A} (notelim). This makes sense if we assume that the logical system is sound, because this means that it is free of absurdities, so if A was true it would be impossible to prove an absurdity thus A must be false. Second the assumption of bottom can be used to conclude anything. In [LiCS] this is captured in the proof rule \frac{⊥}{A} (botelim).

Since the predicate logic from Mathworld, which we have used as a basis for [Theory pred calc], doesn’t use or define the notion of bottom, we cannot adopt the rules of natural deduction directly. We have chosen to solve this problem by replacing the problematic proof rules above with a new proof rule called notintro. This way we can avoid the use of bottom alltogether while we preserve the rest of the system.

To justify our actions we hand proof the following metatheorem:

Theorem 5.19 Let Nat’ be the system of proof rules introduced in section 5 and let Nat be the same system without the rule notintro but with rules notelim and botelim added. Let F be fixed and define ⊥ ≡ F ∧ ¬F^{4}. Then the following holds:

1. If B can be proved in Nat then B[F ∧ ¬F/⊥] can be proved in Nat’.

2. If B can be proved in Nat’ then B can be proved in Nat.

PROOF:

Both claims in this metatheorem are proved by induction on the derivation of the proof on the left hand side of the implication. To save space we only consider the interesting cases. Thus we skip all of the rules the two systems have in common.

Proof of 1: In this proof A′ ≡ A[F ∧ ¬F/⊥].

The rule \frac{A ¬A}{⊥}. Given proofs of A and ¬A we need to prove F ∧ ¬F. Using the induction hypothesis on the proofs of A and ¬A, we get proofs of A′ and ¬A′ using our system of lemmas. Now we have proofs of A′ and ¬A′, which means that we can also prove A′ and ¬A′ using F or ¬F as assumptions. Now we can construct the proof of F ∧ ¬F like this:

\frac{\frac{\frac{¬F ; ⋮ ; A′  ¬F ; ⋮ ; ¬A′}{¬¬F}}{F}  \frac{F ; ⋮ ; A′  F ; ⋮ ; ¬A′}{¬F}}{F ∧ ¬F}

The rule \frac{⊥}{A}. Given proof of F ∧ ¬F we need to prove A′. Using the induction hypothesis we get a proof of F ∧ ¬F. Using andelim1 and andelim2 we obtain proofs of F and ¬F. Finally (using weakening) we can construct proofs of F and ¬F under the assumption of ¬A′. Now we can construct the proof of A′ as follows:

\frac{\frac{\frac{¬A′ ; ⋮ ; F ∧ ¬F}{F} \frac{¬A′ ; ⋮ ; F ∧ ¬F}{¬F}}{¬¬A′}}{A′}

The rule \frac{A⊢⊥}{¬A}. Using the induction hypothesis on the proof of A ⊢ ⊥ we obtain a proof of A′ ⊢ F∧¬F. Using the andelim1 and andelim2 lemmas, we get proofs of A′ ⊢ F and A′ ⊢ ¬F. Now we can construct the proof of ¬A′ like this:

\frac{\frac{A′ ; ⋮ ; F ∧ ¬F}{F} \frac{A′ ; ⋮ ; F ∧ ¬F}{¬F}}{¬A′}

4F must be fixed for all occurrences of bottom e.g. ⊥ ∨ ⊥ must be translated to (F ∧ ¬F) ∨ (F ∧ ¬F) and can’t be translated to (F ∧ ¬F) ∨ (G ∧ ¬G).

That concludes all the interesting rules. The other rules follow by using the induction hypothesis on the given proofs, and using the same rule to conclude the desired proposition.

Proof of 2: There is only one interesting rule, and that is notintro. Given the proofs of A ⊢ B and A ⊢ ¬B we wish to prove ¬A. We construct the proof like this.

\frac{\frac{A ⋮ B A ; ⋮ ; ¬B}{⊥}}{¬A}

That concludes all the interesting rules. The other rules follow by using the induction hypothesis on the given proofs, and using the same rule to conclude the desired proposition.

■

5.2.1 A practical lemma

Above we saw that ⊥ could be replaced with F ∧ ¬F and that the proof rule botelim allows us to conclude anything once we have ⊥. This gives rise to the following very usefull lemmas.

Lemma 5.20 [pred calc lemma bottomelim: ΠF, G: F ∧ ¬F ⊢ G]

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

Lemma 5.21 [pred calc lemma lemnotintro: ΠF, G: (F ⇒ G ∧ ¬G) ⊢ ¬F]

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

6 Application of natural deduction lemmas

In this section we set out to prove lemma 6.6 which is the main result of this project. The content of the lemma is simple, but the formal proof is quite long. Therefore we have split it into six lemmas. Finally we prove an easy result containing quantifiers in lemma 6.8. We have also tried to prove ΠF, G, X , H, P: X #G ⊢⊢ X #H ⊢⊢ ⟨H≡F|X:=G⟩ ⊢⊢ P ⇒ ∀X . (F) ⊢ ¬P ⇒ ∃X . (F) ⊢ ∃X . (F)

but we ran into problems when we tried to used side conditions within blocks. Either we got a false side condition or a metageneralization error. Therefore these attempts have been removed from our final report.

Lemma 6.1 [pred calc lemma hlplem1: ΠP, Q: (P ⇒ Q) ⇒ Q ⊢ Q ⇒ P ⊢ P ⇒ Q ⊢ P]

pred calc proof of hlplem1:
L01: Arbitrary ≫  P, Q  ;
L02: Premise ≫  (P ⇒ Q) ⇒ Q  ;
L03: Premise ≫  Q ⇒ P  ;
L04: Premise ≫  P ⇒ Q  ;
L05: pcmp ⊳ L04 ⊳ L02 ≫  Q  ;
L06: pcmp ⊳ L05 ⊳ L03 ≫  P  □

Lemma 6.2 [pred calc lemma hlplem2: ΠP, Q: P ⊢ ¬P ⊢ Q]

pred calc proof of hlplem2:
L01: Arbitrary ≫  P, Q  ;

L02: Premise ≫  P  ;
L03: Premise ≫  ¬P  ;
L04: andintro ⊳ L02 ⊳ L03 ≫  P ∧ ¬P  ;
L05: bottomelim ⊳ L04 ≫  Q  □

Lemma 6.3 [pred calc lemma hlplem3: ΠP, Q: ¬(P ⇒ Q) ⊢ ¬P ⊢ (P ⇒ Q) ∧ ¬(P ⇒ Q)]

pred calc proof of hlplem3:
L01: Arbitrary ≫  P, Q  ;
L02: Premise ≫  ¬(P ⇒ Q)  ;
L03: Premise ≫  ¬P  ;
L04: Block ≫  Begin  ;
L05: Arbitrary ≫  P, Q  ;
L06: Premise ≫  P  ;
L07: hlplem2 ⊳ L06 ⊳ L03 ≫  Q  ;
L08: Block ≫  End  ;
L09: pcdeduction ⊳ L08 ≫  P ⇒ Q  ;
L10: andintro ⊳ L09 ⊳ L02 ≫  (P ⇒ Q) ∧ ¬(P ⇒ Q)  □

Lemma 6.4 [pred calc lemma hlplem4: ΠP, Q: ¬(P ⇒ Q) ⊢ P]

pred calc proof of hlplem4:
L01: Arbitrary ≫  P, Q  ;
L02: Premise ≫  ¬(P ⇒ Q)  ;
L03: Block ≫  Begin  ;
L04: Arbitrary ≫  P, Q  ;
L05: Premise ≫  ¬P  ;
L06: hlplem3 ⊳ L02 ⊳ L05 ≫  (P ⇒ Q) ∧ ¬(P ⇒ Q)  ;
L07: Block ≫  End  ;
L08: pcdeduction ⊳ L07 ≫  ¬P ⇒ (P ⇒ Q) ∧ ¬(P ⇒ Q)  ;
L09: lemnotintro ⊳ L08 ≫  ¬¬P  ;
L10: notnotelim ⊳ L09 ≫  P  □

Lemma 6.5 [pred calc lemma hlplem5: ΠP, Q: (P ⇒ Q) ⇒ Q ⊢ Q ⇒ P ⊢ P]

pred calc proof of hlplem5:
L01: Arbitrary ≫  P, Q  ;
L02: Premise ≫  (P ⇒ Q) ⇒ Q  ;
L03: Premise ≫  Q ⇒ P  ;
L04: Block ≫  Begin  ;
L05: Arbitrary ≫  P, Q  ;
L06: Premise ≫  (P ⇒ Q) ⇒ Q  ;
L07: Premise ≫  Q ⇒ P  ;
L08: Premise ≫  P ⇒ Q  ;
L09: hlplem1 ⊳ L06 ⊳ L07 ⊳ L08 ≫ P  ;

L10: Block ≫  End  ;
L11: pcdeduction ⊳ L10 ≫  {((P ⇒ Q) ⇒ Q) ⇒ (Q ⇒ \atop P) ⇒ (P ⇒ Q) ⇒ P  ;}
L12: pcmp ⊳ L02 ⊳ L11 ≫  (Q ⇒ P) ⇒ (P ⇒ Q) ⇒ P  ;
L13: pcmp ⊳ L03 ⊳ L12 ≫  (P ⇒ Q) ⇒ P  ;
L14: Block ≫  Begin  ;
L15: Arbitrary ≫  P, Q  ;
L16: Premise ≫  P ⇒ Q  ;
L17: pcmp ⊳ L16 ⊳ L13 ≫  P  ;
L18: Block ≫  End  ;
L19: pcdeduction ⊳ L18 ≫  P ⇒ Q ⊢ P  ;
L20: Block ≫  Begin  ;
L21: Arbitrary ≫  P, Q  ;
L22: Premise ≫  ¬(P ⇒ Q)  ;
L23: hlplem4 ⊳ L22 ≫  P  ;
L24: Block ≫  End  ;
L25: pcdeduction ⊳ L24 ≫  ¬(P ⇒ Q) ⊢ P  ;
L26: lem ≫  (P ⇒ Q) ∨ ¬(P ⇒ Q)  ;
L27: orelim ⊳ L26 ⊳ L19 ⊳ L25 ≫  P  □

Lemma 6.6 (Main result) [pred calc lemma goal1: ΠP, Q: ((P ⇒ Q) ⇒ Q) ⇒ ((Q ⇒ P) ⇒ P)]

pred calc proof of goal1:
L01: Arbitrary ≫  P, Q  ;
L02: Block ≫  Begin  ;
L03: Arbitrary ≫  P, Q  ;
L04: Premise ≫  (P ⇒ Q) ⇒ Q  ;
L05: Block ≫  Begin  ;
L06: Arbitrary ≫  P, Q  ;
L07: Premise ≫  Q ⇒ P  ;
L08: hlplem5 ⊳ L04 ⊳ L07 ≫  P  ;
L09: Block ≫  End  ;
L10: pcdeduction ⊳ L09 ≫  (Q ⇒ P) ⇒ P  ;
L11: Block ≫  End  ;
L12: pcdeduction ⊳ L11 ≫  {((P ⇒ Q) ⇒ Q) ⇒ ((Q ⇒ \atop P) ⇒ P)  □}

Lemma 6.7 [pred calc lemma hlplem6: ΠX , F, G, H: X #G ⊢⊢ X #H ⊢⊢ ⟨H≡F|X:=G⟩ ⊢⊢ ∀X . (F) ⊢ ∃X . (F)]

pred calc proof of hlplem6:
L01: Arbitrary ≫  X , F, G, H  ;
L02: Side-condition ≫  X #G  ;
L03: Side-condition ≫  X #H  ;
L04: Side-condition ≫  ⟨H≡F|X:=G⟩  ;

L05: Premise ≫  ∀X . (F)  ;

L06: forallelim ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳

L04 ⊳ L05 ≫ H ;

L07: existsintro ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳

L04 ⊳ L06 ≫ ∃X . (F) □

Lemma 6.8 [pred calc lemma goal2: ΠF, G, X , H, K: X #G ⊢⊢ X #H ⊢⊢ ⟨H≡F|X:=G⟩ ⊢⊢ ∀X . (F) ⊢ ¬∃X . (F) ⇒ K]

pred calc proof of goal2:
L01: Arbitrary ≫  F, G, X , H, K  ;
L02: Side-condition ≫  X #G  ;
L03: Side-condition ≫  X #H  ;
L04: Side-condition ≫  ⟨H≡F|X:=G⟩  ;
L05: Premise ≫  ∀X . (F)  ;

L06: hlplem6 ⊳ ⊳ L02 ⊳ ⊳ L03 ⊳ ⊳

L04 ⊳ L05 ≫ ∃X . (F) ;

L07: Block ≫  Begin  ;
L08: Arbitrary ≫  F, X , K  ;
L09: Premise ≫  ∃X . (F)  ;
L10: Premise ≫  ¬∃X . (F)  ;
L11: andintro ⊳ L09 ⊳ L10 ≫  ∃X . (F) ∧ ¬∃X . (F)  ;
L12: bottomelim ⊳ L11 ≫  K  ;
L13: Block ≫  End  ;
L14: pcdeduction ⊳ L13 ≫  ∃X . (F) ⇒ ¬∃X . (F) ⇒ K  ;
L15: pcmp ⊳ L06 ⊳ L14 ≫  ¬∃X . (F) ⇒ K  □

A Ways Logiweb^{TM} could be improved

Working with Logiweb^{TM} have given us some ideas of how the system could be improved and how it could be made more userfriendly. Our ideas are summarized below:

• A getting started manual explaining the basic concepts and quirks of the system including simplified examples. Man pages together with the base and check pages leaves a lot to be desired.

• Sample pages / proofs for the current version of the pyk compiler (we have used a lot of time searching other peoples Logiweb^{TM} pages to gain knowledge but it has often been in vain because the syntax had changed).

• Better error messages and / or an explanation of how to read them. Also it would be nice if error messages included the line number of the error.

• It would be nice if L^{A}TEX errors and warnings could be displayed. Just knowing that there is an error leaves a lot of detective work to be done.

• A pre-parser substituting ( with parenthesis, ) with end parenthesis, , with comma ect. would be nice.

References

[LiCS] Logic in Computer Science - Modelling and Reasoning about Systems, Second Edition - 2004. By Michael Huth & Mark Ryan ISBN: 0-521-54310-X

B 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”] [pcunsound →^{pyk} “pcunsound”] [pcia →^{pyk} “pcia”] [pcie →^{pyk} “pcie”] [pcdeduction →^{pyk} “pcdeduction”] [trivia →^{pyk} “trivia”] [repeat →^{pyk} “repeat”] [andintro →^{pyk} “andintro”] [andelim1 →^{pyk} “andelim1”] [andelim2 →^{pyk} “andelim2”] [orintro1 →^{pyk} “orintro1”] [orintro2 →^{pyk} “orintro2”] [orelim →^{pyk} “orelim”] [notintro →^{pyk} “notintro”] [implyintro →^{pyk} “implyintro”] [notnotintro →^{pyk} “notnotintro”] [notnotelim →^{pyk} “notnotelim”]

[mt →^{pyk} “mt”]

[pbc →^{pyk} “pbc”] [lem →^{pyk} “lem”] [forallintro →^{pyk} “forallintro”] [forallelim →^{pyk} “forallelim”] [existsintro →^{pyk} “existsintro”] [existselim →^{pyk} “existselim”] [bottomelim →^{pyk} “bottomelim”] [lemnotintro →^{pyk} “lemnotintro”] [hlplem1 →^{pyk} “hlplem1”] [hlplem2 →^{pyk} “hlplem2”] [hlplem3 →^{pyk} “hlplem3”] [hlplem4 →^{pyk} “hlplem4”] [hlplem5 →^{pyk} “hlplem5”] [goal1 →^{pyk} “goal1”] [hlplem6 →^{pyk} “hlplem6”] [goal2 →^{pyk} “goal2”] [∗ ≡ ∗ →^{pyk} “" setequiv "”] [∗ = ∗ →^{pyk} “" setequals "”]

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

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

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

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

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

D Priority table

Priority table Preassociative [test], [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], [pcunsound], [pcia], [pcie], [pcdeduction], [trivia], [repeat], [andintro], [andelim1], [andelim2], [orintro1], [orintro2], [orelim], [notintro], [implyintro], [notnotintro], [notnotelim], [mt], [pbc], [lem], [forallintro], [forallelim], [existsintro], [existselim], [bottomelim], [lemnotintro], [hlplem1], [hlplem2], [hlplem3], [hlplem4], [hlplem5], [goal1], [hlplem6], [goal2]; 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