Logic

2

Propositional Logic 2.1

Formal Language

When defining propositional logic we will eventually want to be able to express all of and, or, not, and implies. One possibility is to make all four operators part of our formal language. However, it turns out that and, or, and not can all be defined in terms of only implication and a constant falsum, which we will denote as $\bot$. The advantage of doing things this way is that later we will need fewer axioms because we will have fewer foundational terms we need to define the meaning of. The disadvantage is that to define and and or in terms of implication we will have to assume the law of the excluded middle or equivalently the law of double negation. This means that we will can only do classical logic. However, supporting intuitionist logic is not a goal of this development. So we will take the simpler formal language.

The first piece of formal language syntax we want to define is the implication operator. Below is the Watson command to define the operator. Watson calls mathematical statements sentences and so defines the non-terminal that represents mathematical statements sentence. The syntax non-terminal ::= replacement for defining productions in a context free grammar is actually standard and is called Backus–Naur form. The (500) is a Watson specific extension and allows defining the precedence of different pieces of syntax. This is not mathematically meaningful but simply helps with writing notation. For example, we want ¬p → q to mean (¬p) → q and not ¬(p → q).

37syntax implication
38    sentence (250) ::= sentence " → " sentence
39end

The next piece of syntax we will define is the constant symbol falsum. This represents a statement that is always false. The utility of this will become apparent shortly.

45syntax falsum
46    sentence ::= "⊥"
47end

This is the entire formal language of propositional logic. It is remarkably small yet it is capable of expressing all quantifier free logical statements.

Other Logical Operators

Although only implication and falsum are part of our formal language, we still need to be able to discuss and, or, and not. To do this we will use another Watson feature: definitions.

Definitions allow us to define new notation along with a replacement rule to explain what the definition means. Internally, Watson expands definitions into the underlying formal language before checking proofs. So definitions have no effect on proof checking. Instead they are simply a convenience for writing proofs. In theory, we do not need to employ definitions at all.

Let us make our first definition in order to define the negation operator. How can we express negation using only implication and falsum? If a proposition $p$ leads to a contradiction, then we can conclude that $p$ is false. We can write $p$ leading to a contradiction as $p \to \bot$ since $\bot$ represents a false statement, a.k.a. a contradiction. So since we know that $p \to \bot$ means $p$ is false, we can make this our definition of $\neg p$.

In order to explain this definition to Watson there are two steps. First we must define the actual syntax of the notation we want to use.

74notation not
75    sentence (400) ::= "¬" sentence
76end

This allows Watson to correctly parse the notation when we later write it. But we also need to define what the notation means. We can do this with a replacement rule. The reason these are separated into two different steps is that often we use the same notation to refer to multiple different things. For example, later we will use |x| to mean both numeric absolute value and set cardinality.

85definition
86    ¬p := p → ⊥
87end

The definition syntax is intuitive. You simply place the expression you want to define on the left, and the definition on the right. Where we wrote sentence in the notation command we give a variable name p in the definition command. We use := instead of = because = is a part of our formal language that we will later want to define. Instead we use := as a metalogical symbol for definitions. Note that this means it is not a good idea to make := a symbol in your formal language.

Next we can define or. Again we must think in terms of the operations we have already defined. One property of or that we know is that if $p \lor q$ is true and $p$ is not true, then $q$ is true. In fact, we can use this as our definition, defining $p \lor q$ as $\neg p \to q$.

102notation or
103    sentence (300>) ::= sentence " ∨ " sentence
104end

106definition
107    p ∨ q := ¬p → q
108end

Notice that the definition is not symmetric. When we prove the properties of or we will initially have to have separate proofs for the left and right sides.

We can define and in terms of or using the standard DeMorgan's Law relationship. That is we define $p \land q$ to mean $\neg(\neg p \lor \neg q)$. However, before we can make this definition we need one other definition: parentheses! Don't laugh. Parentheses are a part of mathematical notation too and they need a definition just like everything else.

119notation sentence.parentheses
120    sentence ::= "(" sentence ")"
121end

Parenthesis are somewhat unique though in that inserting parentheses shouldn't effect the meaning of the sentence beyond disambiguation. To track this fact, we are going to use another Watson feature: attributes. We can declare a new attribute like so:

128attribute reducible
129    attribute ::= @kw"reducible"
130end

Then when we make our definition we attach the annotation.

134@[reducible]
135definition
136    (p) := p
137end

How, exactly, this reducible annotation will be used will be explained later.

With this we are able to define and.

143notation and
144    sentence (350>) ::= sentence " ∧ " sentence
145end

147definition
148    p ∧ q := ¬(¬p ∨ ¬q)
149end

There is one final definition we would like to make: $p \leftrightarrow q$. The definition is completely standard however there is one thing to comment on. Notice that the definition of $p \leftrightarrow q$ includes two copies each of $p$ and $q$. If $p$ and $q$ themselves contain if and only ifs, then the size of the formal language sentence our notation describes would grow exponentially! Luckily Watson is equipped to handle this and stores the formal language sentences in a form where the size is linear with respect to the notation used.

160notation iff
161    sentence (200) ::= sentence " ↔ " sentence
162end

164definition
165    p ↔ q := (p → q) ∧ (q → p)
166end

Axioms

Having defined our notation we are now ready to give the axioms of propositional logic. Just as we amazingly need only two operators to define the complete syntax of propositional logic, we also need just four axioms to completely describe the properties of those operators. When we introduce quantifiers we will add two more axioms which means we need just six axioms to define all of logic!

The first axiom is the most venerable and most intuitive of the four. It is the axiom of modus ponens. It says that if $p \to q$ and $p$ are both true then $q$ is also true. This might seem so obvious as to barely require stating but remember from the introduction that it is only the axioms that give the sentences in our formal language meaning. So far all we have told Watson is that we are allowed to write the literal symbol →. We have not yet told Watson what this symbol means. The axiom of modus ponens is what gives the implication symbol its meaning.

185axiom modus_ponens [p q : sentence] : (p → q) (p)
186    |- q
187end

Let's take a moment to understand the axiom command. Immediately following the keyword axiom is the name of the axiom. When we later write proofs we will invoke the axiom by referring to this name. Next comes the templates of the axiom. When we say that $p \to q$ and $p$ together imply $q$ we mean that this deduction holds for any possible $p$ and $q$. It is this idea of the statement being true for any possible $p$ and $q$ that the syntax [p q : sentence] tells Watson. After the templates comes a : to indicate the end of the templates and the beginning of the hypotheses. Finally, we mark the conclusion of the axiom with the |- symbol. This is a standard symbol from logic called a tack or turnstile and can be read as "entails." So we get that the hypotheses entail the conclusion.

In the axiom the implication has been eliminated from the hypothesis to reach the conclusion. As such the axiom of modus ponens is also often called the axiom of implication elimination. Modus ponens allows us to derive a new fact if we already know an implication. But how will we learn an implication in the first place? This will be accomplished with the second axiom of propositional logic: the axiom of implication introduction or, as we will call it, the deduction axiom.

208axiom deduction [p q : sentence] : (assume p |- q)
209    |- p → q
210end

This axiom has a hypothesis which is quite different from the ones we have seen before. You will notice that assume p |- q is neither part of our formal language nor a piece of notation we have defined. In fact it is not a mathematical statement at all, it is a metamathematical statement. When we write assume p |- q as a hypothesis, what we are telling Watson is that the conclusion can be reached if knowing that $p$ was true would allow us to prove that $q$ was true. Thus assume p |- q is not a statement that has a truth value within the mathematical system we are defining. It is not even a statement in that system! This is a question about the behavior of the proof system itself. Therefore it is metamathematical.

In Watson we call statements of the form assume p |- q facts to distinguish them from statements in our formal mathematical system which you will recall we are calling sentences. Watson will record which facts have been proven and facts can be hypotheses but a fact cannot be a conclusion of an axiom. To do so would be a category error. An axiom tells Watson about the definition of truth in the formal language we are defining. However it is Watson itself that decides which things are provable. To make a fact the conclusion of an axiom would be to declare that a certain proof exists, which might not be true. Whether such a proof exists is a concrete fact about the world, not an abstract truth function we can define specific cases of.

The final two axioms concern the falsum constant. The third axiom is the axiom of double negation. It says that if $\neg\neg p$ is true then $p$ is also true. It is the addition of this deduction that makes our logic classical. Because we defined and and or in terms of implication and falsum this axiom is required to prove facts about and and or. So almost no intuitionist reasoning will be possible in our system.

241axiom not_not.elim [p : sentence] : (¬¬p)
242    |- p
243end

The fourth and final axiom is the principle of explosion. It states that if we know $\bot$ to be true, anything at all can be proven.

248axiom explosion [p : sentence] : (⊥)
249    |- p
250end

This axiom may seem surprising but it would actually be implied by any system of reasoning about falsity. If we know that $q$ and $\neg q$ are both true then we can make the following (right now informal) argument that an arbitrary $p$ is true. Since $q$ is true $q \lor p$ is true. But $\neg q$ is true so since $q \lor p$ is true it must be that $p$ is true. Hence $p$. As we can see the principle of explosion will be true once we have defined all the normal logical deductions anyway. So, since it turns out that the principle of explosion will help us prove those deductions, it is reasonable to add it as an axiom.

Tactics

With our definitions and axioms in hand, we are now ready to begin proving theorems. Theorem statements in Watson look identical to axioms except, of course, that they come with a proof. What is the syntax for these proofs? The syntax is entirely defined by us! Watson has no built-in proof syntax. Instead we use the tactic command to define a new type of proof syntax and then write code in the scripting language Lua that transforms this proof syntax into a formal deduction that Watson can check. Let's define a simple proof syntax we can use to prove our first theorems.

The simplest proof step is claiming that a fact is true and providing a justification for that step. There are multiple ways of justifying a fact so we will create a non-terminal symbol that represents justifications. We can do this with the grammar_category command.

277grammar_category justification

Then we will claim that a fact is true by using the follows tactic. Notice that we provide both the justification for the given fact and the tactic that will complete the rest of the proof given this new fact.

283tactic tactic.follows
284    -- The name before the colon is the name that can be used in Lua to access 
285    -- the sub-tactic. The name after the colon is the non-terminal.
286    tactic ::= @kw"follows" goal:@fact just:justification ";" next:tactic
287end

One form of justification for a fact is applying a theorem. We will call this justification by. To use a theorem we need to fill in any template parameters the theorem has. We will create a new non-terminal for the templates.

293grammar_category templates

295tactic justification.by
296    justification ::= @kw"by" thm:@name tmps:templates
297end

And then we will fill in the syntax for a list of template instantiations.

301grammar_category template

303tactic templates.some
304    templates ::= tmp:template rest:templates
305end

307tactic templates.none
308    templates ::=
309end

311tactic template
312    template ::= "[" frag:@any_fragment "]"
313end

The pattern of a some and none variant is a common way of expressing a list within a context free grammar.

Another possible justification is using a whole subproof to prove a given fact. We will call this justification as which reminds us of a proof remark like "the fact follows as this subproof demonstrates."

322tactic justification.tactic
323    justification ::= @kw"as" tactic:tactic
324end

Another useful tactic will be todo. This can be used when we are in the middle of writing our proofs. It will prove anything we want but Watson will mark our proof as unfinished so we know to return and finish it later. This is similar to sorry in Lean.

331tactic tactic.todo
332    tactic ::= @kw"todo"
333end

The final tactic we will need is the simplest tactic of all: do nothing. This is useful if the goal of our proof has already been proven and we don't need to do anything more.

339tactic tactic.empty
340    tactic ::=
341end

And and Or

We will start by proving the basic facts about or. For or there are two introduction rules. Left and right introduction. That is, if we know $p$ is true then we know $p \lor q$ is true. And also if we know $q$ is true then $p \lor q$ is true. As we mentioned before, the definition of or is asymmetric so the proofs of these two facts are different.

351theorem or.intro_right [p q : sentence] : (q)
352    |- p ∨ q
353proof
354    -- p ∨ q means ¬p → q by definition. so we want to prove an implication.
355    -- we will start by assuming that ¬p is true.
356    follows assume ¬p |- q as
357        -- however q is a hypothesis so there is nothing to be proved
358    ;
359
360    -- we have assume ¬p |- q but we want ¬p → q so we will use the deduction
361    -- theorem to convert between these
362    follows ¬p → q by deduction [¬p] [q];
363qed

This proof features a very common style of deduction: we assume $p$ and deduce $q$. Then we apply the deduction theorem to conclude $p \to q$. Let's add a new tactic that automatically performs this reasoning.

369tactic tactic.assume_then
370    tactic ::= @kw"assume" assumption:@fragment(sentence) @kw"then" 
371               conclusion:@fragment(sentence) just:justification ";" next:tactic
372end

TODO: explanation

375tactic tactic.assume
376    tactic ::= kw:@kw"assume" assumption:@fragment(sentence) ";" next:tactic
377end

We can use this new tactic to prove the other or introduction rule.

381theorem or.intro_left [p q : sentence] : (p)
382    |- p ∨ q
383proof
384    -- since p ∨ q is really ¬p → q it suffices to show ¬p → q.
385    assume ¬p then q as
386        -- we have both p and ¬p which is a contradiction. recall that ¬p means
387        -- p → ⊥ so we can derive ⊥ and then use explosion to get q.
388        follows ⊥ by modus_ponens [p] [⊥];
389        follows q by explosion [q];
390    ;
391qed

In this proof we see two more common proof patterns that we will make into tactics. If we can derive $\bot$ then our proof is always done because we can use the explosion theorem. This represents the normal proof idea of having reached a contradiction. The contradiction tactic will automatically search the facts we have proven to see if we have both a fact and its negation. If it finds such a contradiction it will complete the proof. Otherwise it will produce an error.

401tactic tactic.contradiction
402    tactic ::= @kw"contradiction" just:justification
403end

The other proof pattern we observed came at the start. We saw that $p \lor q$ was defined as $\neg p \to q$ so it suffices to show this second fact. We wrote a comment to explain this but it is better to have Watson actually check the equivalence for us. We will introduce a new tactic suffices that changes the goal to a new goal using the given justification to show that the new goal is sufficient to prove the old goal.

412tactic tactic.suffices
413    tactic ::= @kw"suffices" goal:@fragment(sentence) just:justification ";" 
414               next:tactic
415end

If the two goals are definitionally equal, as they were in or.intro_left, no justification is needed. Let's add a new, empty, justification for when there isn't actually anything to prove.

421tactic justification.empty
422    justification ::=
423end

Armed with these new tactics we can prove the elimination rule for or. It says that if we know $p \lor q$ is true and that both $p$ and $q$ imply $r$ then $r$ is also true. This is a natural inference rule and we could have chosen this as an axiom instead of double negation elimination.

430theorem or.elim [p q r : sentence] : (p ∨ q) (p → r) (q → r)
431    |- r
432proof
433    -- assuming ¬r will lead to a contradiction. thus we will have ¬¬r which
434    -- we can convert to r using the not_not.elim axiom.
435    assume ¬r then ⊥ as
436        -- p gives us r which is a contradiction. so we have ¬p
437        assume p then ⊥ as
438            follows r by modus_ponens [p] [r];
439            contradiction
440        ;
441        -- but since p ∨ q we must then have q
442        follows q by modus_ponens [¬p] [q];
443        -- which also gives us r
444        follows r by modus_ponens [q] [r];
445        -- so we have a contradiction still
446        contradiction
447    ;
448    follows r by not_not.elim [r];
449qed

Once again there is a common proof pattern here we can make into a tactic. We assume a fact and then derive a contradiction from it. This allows us to conclude the negation of that fact. We will call the tactic assume for_contra.

455tactic tactic.assume_contra
456    tactic ::= @kw"assume" assumption:@fragment(sentence) @kw"for_contra" ";" 
457               next:tactic
458end

Also, and this is an entirely aesthetic concern, writing follows everywhere is boring. Let's introduce thus and 'hence' which do the same thing as follows but makes the proof easier to read when one fact follows directly from what was previously shown.

464tactic tactic.thus
465    tactic ::= @kw"thus" goal:@fact just:justification ";" next:tactic
466end

468tactic tactic.hence
469    tactic ::= @kw"hence" goal:@fact just:justification ";" next:tactic
470end

472tactic tactic.furthermore
473    tactic ::= @kw"furthermore" goal:@fact just:justification ";" next:tactic
474end

476tactic tactic.indeed
477    tactic ::= @kw"indeed" goal:@fact just:justification ";" next:tactic
478end

We are now ready to prove that or is commutative.

483theorem or.comm [p q : sentence] : (p ∨ q)
484    |- q ∨ p
485proof
486    assume p then q ∨ p by or.intro_right [q] [p];
487    assume q then q ∨ p by or.intro_left [q] [p];
488    thus q ∨ p by or.elim [p] [q] [q ∨ p];
489qed

If we know $p \lor q$ and that $p$ is false then we must have $q$. Once again, since the definition of or is asymmetric the two proofs are not the same.

494theorem or.not_left [p q : sentence] : (p ∨ q) (¬p)
495    |- q
496proof
497    -- this theorem is how we defined or! p ∨ q is by definition ¬p → q
498    follows ¬p → q;
499    thus q by modus_ponens [¬p] [q];
500qed

Just like with suffices it is helpful to have Watson check if our goal is definitionally equal, let's add the have tactic when we are claiming a fact we already have is definitionally equal to a new form.

506tactic tactic.have
507    tactic ::= @kw"have" f1:@fragment(sentence) @kw"from" f2:@fragment(sentence)
508               ";" next:tactic
509end

We can apply or.not_left to prove or.not_right.

513theorem or.not_right [p q : sentence] : (p ∨ q) (¬q)
514    |- p
515proof
516    assume ¬p for_contra;
517    thus q by or.not_left [p] [q];
518    contradiction
519qed

Next let's move on to proving properties about and. Whereas or has two introduction rules and one elimination rule, and has one introduction rule and two elimination rules.

525theorem and.intro [p q : sentence] : (p) (q)
526    |- p ∧ q
527proof
528    -- we can expand the definition of p ∧ q
529    suffices ¬(¬p ∨ ¬q);
530    assume ¬p ∨ ¬q for_contra;
531    -- but either of these possibilities leads to a contradiction
532    assume ¬p then ⊥ as contradiction;
533    assume ¬q then ⊥ as contradiction;
534    thus ⊥ by or.elim [¬p] [¬q] [⊥];
535qed

This time the definition of and is symmetrical so the proofs of the two elimination rules are the same.

540theorem and.elim_left [p q : sentence] : (p ∧ q)
541    |- p
542proof
543    assume ¬p for_contra;
544    thus ¬p ∨ ¬q by or.intro_left [¬p] [¬q];
545    have ¬(¬p ∨ ¬q) from p ∧ q;
546    contradiction
547qed

549theorem and.elim_right [p q : sentence] : (p ∧ q)
550    |- q
551proof
552    assume ¬q for_contra;
553    thus ¬p ∨ ¬q by or.intro_right [¬p] [¬q];
554    have ¬(¬p ∨ ¬q) from p ∧ q;
555    contradiction
556qed

Then the proof of and commutativity is very simple.

560theorem and.comm [p q : sentence] : (p ∧ q)
561    |- q ∧ p
562proof
563    follows p by and.elim_left [p] [q];
564    follows q by and.elim_right [p] [q];
565    thus q ∧ p by and.intro [q] [p];
566qed

If And Only If

Since if and only if is just a special case of and it has the same introduction and elimination rules. We just refer to the theorems we proved for and.

573theorem iff.intro [p q : sentence] : (p → q) (q → p)
574    |- p ↔ q
575proof
576    suffices (p → q) ∧ (q → p);
577    follows (p → q) ∧ (q → p) by and.intro [p → q] [q → p];
578qed

580theorem iff.elim_fwd [p q : sentence] : (p ↔ q)
581    |- p → q
582proof
583    follows p → q by and.elim_left [p → q] [q → p];
584qed

586theorem iff.elim_rev [p q : sentence] : (p ↔ q)
587    |- q → p
588proof
589    follows q → p by and.elim_right [p → q] [q → p];
590qed

And we can also prove a few more standard properties.

594theorem iff.mp [p q : sentence] : (p ↔ q) (p)
595    |- q
596proof
597    follows p → q by iff.elim_fwd [p] [q];
598    thus q by modus_ponens [p] [q];
599qed

601theorem iff.mpr [p q : sentence] : (p ↔ q) (q)
602    |- p
603proof
604    follows q → p by iff.elim_rev [p] [q];
605    thus p by modus_ponens [q] [p];
606qed

If and only if is an equivalence relation.

610theorem iff.refl [p : sentence] :
611    |- p ↔ p
612proof
613    assume p then p;
614    thus p ↔ p by iff.intro [p] [p];
615qed

617theorem iff.symm [p q : sentence] : (p ↔ q)
618    |- q ↔ p
619proof
620    follows p → q by iff.elim_fwd [p] [q];
621    follows q → p by iff.elim_rev [p] [q];
622    thus q ↔ p by iff.intro [q] [p];
623qed

625theorem iff.trans [p q r : sentence] : (p ↔ q) (q ↔ r)
626    |- p ↔ r
627proof
628    assume p then r as
629        thus q by iff.mp [p] [q];
630        thus r by iff.mp [q] [r];
631    ;
632    assume r then p as
633        thus q by iff.mpr [q] [r];
634        thus p by iff.mpr [p] [q];
635    ;
636    thus p ↔ r by iff.intro [p] [r];
637qed

Sometimes if $p \leftrightarrow q$ we say that $p$ and $q$ are equivalent. We can make this notion rigorous in the following sense: for any property that holds of $p$, that same property also holds of $q$ (and vice versa). We can show that this equivalence holds by induction over all possible formal sentences containing $p$.

646theorem iff.equiv.imp1 [p q r : sentence] : (p ↔ q) (p → r)
647    |- q → r
648proof
649    assume q then r as
650        follows p by iff.mpr [p] [q];
651        thus r by modus_ponens [p] [r];
652    ;
653qed

655theorem iff.equiv.imp2 [p q r : sentence] : (p ↔ q) (r → p)
656    |- r → q
657proof
658    assume r then q as
659        follows p by modus_ponens [r] [p];
660        thus q by iff.mp [p] [q];
661    ;
662qed

664theorem iff.equiv.falsum [p q : sentence] : (p ↔ q) (⊥)
665    |- ⊥
666proof
667    -- not much to prove... 
668qed

With these three proofs we can see that for any property $m(p)$, if $p \leftrightarrow q$ then we will also have $m(q)$. To complete the proof we would have to perform induction over all possible properties $m$. However such an induction would have to take place outside of the formal system. In any specific case we could prove it as a theorem, but the general case is a metatheorem. Watson is not capable of proving such metatheorems, so we will have to add it as an axiom. But we should remember that our reasons for adding this axiom are different than our reasons for the other axioms.

To write the axiom we will need some way of denoting a property of $p$.

681notation sentence.with_sentence
682    sentence (1000) ::= @name "(" sentence ")"
683end

Then we can state the axiom, which we will call iff.rw for if and only if rewrite.

688axiom iff.rw [p q : sentence] [m(_) : sentence(sentence)] : (p ↔ q) (m(p))
689    |- m(q)
690end

First Order Logic 2.2

The logical connectives we have developed thus far allows us to discuss the relationships between various propositions. However, if you examine the formal language we have thus far defined, you will realize that the only sentence that does not contain another sentence within it is $\bot$. This means that every sentence we can discuss is built up from logical combinations of $\bot$. This means that every formal sentence is either trivially false or trivially true. Obviously, this doesn't make for a very interesting mathematical system!

Terms and Equality

When we do mathematics, what form do our most basic assertions take? That is, if you have some sentence with no logical connectives in it, what will it look like? We claim, rather boldly, that every single assertion in traditional mathematics that is not trivially true or false is a claim about the relationship between two or more objects. (If you do not believe this, it may help to consider the definition of the assertion you are thinking of. For example, the statement "$n$ is even" may at first appear to be about just one object, until you remember that the definition of "is even" is "there is some $k$ such that $n = 2 \cdot k$".)

Thus, in order to do mathematics, we will need both objects and at least one relationship between them. We will call an object of study in our mathematical system a "term." (This name comes from the fact that all mathematical statements, if examined deeper and deeper, will eventually terminate at an object). We will inform Watson of our desire for a new category of syntactical object using the syntax_category command.

722syntax_category term

We will want parentheses for terms as well.

726notation term.parentheses
727    term ::= "(" term ")"
728end

730@[reducible]
731definition
732    (a:term) := a
733end

Next, we will need some relationship between terms. All but the most exotic of mathematical systems contain a notion of equality.

738syntax equality
739    sentence (500) ::= term " = " term
740end

We can also define notation for not equals.

744notation inequality
745    sentence (500) ::= term " ≠ " term
746end

748@[reducible]
749definition
750    a ≠ b := ¬a = b
751end

We will need just two axioms to describe the behavior of equality. Once again, these can be thought of as introduction and elimination rules. The first axiom, the introduction rule, asserts that any term is equal to itself. In other words, equality is reflexive.

758axiom eq.refl [a : term] :
759    |- a = a
760end

The second axiom, the elimination rule, says that, if two objects are equal, then they should have all the same properties. Precisely, we mean that if $a = b$ then for any sentence which is true, if we replace all occurrences of $a$ with $b$, the sentence remains true. In order to describe this rule to Watson, we will need notation for a sentence which contains a term.

768notation sentence.with_term
769    sentence (1000) ::= @name "(" term ")"
770end

And now we can state the axiom.

774axiom eq.subst [p(_) : sentence(term)] [a b : term] : (a = b) (p(a))
775    |- p(b)
776end

From these two axioms, and with judicious choice of the substitution property, we can derive that equality is an equivalence relation.

781theorem eq.symm [a b : term] : (a = b)
782    |- b = a
783proof
784    follows a = a by eq.refl  [a];
785    thus    b = a by eq.subst [_ = a] [a] [b];
786qed

788theorem eq.trans [a b c : term] : (a = b) (b = c)
789    |- a = c
790proof
791    follows a = c by eq.subst [a = _] [b] [c];
792qed

Quantifiers

You may have noticed that, although we now have equality as a nontrivial sentence, we in fact cannot use it because we have no terms! Right now, our formal language contains no terms whatsoever, so we could never actually write an equality. To fix this, we will now introduce quantifiers, statements of the form $\exists n, n + n = n$ or $\forall x, x + 1 > x$. The bound variables in the quantifiers will be our first terms.

Similarly to how we only needed to define one of $\lor$ and $\land$ and then could define the remaining one in terms of the other, we only need to add one of $\exists$ and $\forall$ to our formal language. (In fact, this connection is no coincidence. Consider applying DeMorgan's laws to a statement with an infinite number of $\lor$s or $\land$s).

For reasons that will become apparent in a moment, we will choose $\exists$ to be in our formal language. The @binding(term) syntax tells Watson to add a new variable name which holds a term when evaluating the sentence. As discussed in the introduction, this notion is not context free which is why it necessitates a special case within Watson.

815syntax exists
816    sentence (000) ::= "∃" @binding(term) ", " sentence
817end

And we can now define $\forall$ in terms of $\exists$. The explanation of which variables are bound goes on the notation command not the definition command because Watson needs to know which variables exist in order to parse statements before it resolves definitions. Unlike with the syntax commands, bindings in a notation command can be present only for certain children. This will be important later for notation like $\{x \in X ~|~ p(x) \}$ where $x$ should be available on the right but doesn't make sense when evaluating $X$.

827notation forall
828    sentence (000) ::= "∀" x:@binding(term) ", " sentence(x)
829end

831definition
832    ∀x, p(x) := ¬∃x, ¬p(x)
833end

We will also introduce notation for the “at most one” and “unique” existential quantifiers.

838notation exists.at_most_one
839    sentence (000) ::= "∃*" x:@binding(term) ", " sentence(x) 
840end

842@[reducible]
843definition
844    ∃*x, p(x) := ∀y, ∀z, p(y) ∧ p(z) → y = z
845end

847notation exists.unique
848    sentence (000) ::= "∃!" x:@binding(term) ", " sentence(x) 
849end

851@[reducible]
852definition
853    ∃!x, p(x) := (∃x, p(x)) ∧ (∃*x, p(x))
854end

To make sense of quantifiers we will need two axioms. Did you guess that they are once again an introduction rule and an elimination rule? The introduction rule for $\exists$ is simple: if we have a particular object with a property, then we certainly know that there exists an object with that property.

861axiom exists.intro [p(_) : sentence(term)] [a : term] : (p(a))
862    |- ∃x, p(x)
863end

The elimination rule is significantly more complex. In traditional mathematics, $\exists$ elimination works like this: given $\exists x, p(x)$ we can obtain a new variable $y$ such that $p(y)$. The variable $y$ must be "fresh" in the sense that we haven't used it before. We call $y$ the witness to the existential statement. Watson has no way of expressing that a variable is fresh and so we cannot use this system. The reason Watson doesn't support freshness is twofold: On the one hand, as we will soon see, it is unnecessary. But more generally, it makes the system significantly more complicated as sentences can no longer be understood entirely on their own but must now carry with them the context of which variables were "fresh" when they were created.

How can we do without freshness? To understand the problem let's try a simple solution first. We can add a new term to our constant language to serve as the witness. If we imagine the witness is called $\varepsilon$ then we might use the following syntax declaration and axiom.

 syntax witness 
     term ::= "ε"
 end

 axiom exists.elim [p(_) : sentence(term)] : (∃x, p(x))
     |- p(ε)
 end

What would be the problem with this? The issue is that we are using the same witness for every existential. For example, it is the case both that $\exists x, \text{even}(x)$ and $\exists x, \text{odd}(x)$. Then using our axiom we would get that $\text{even}(\varepsilon)$ and $\text{odd}(\varepsilon)$ but obviously no such $\varepsilon$ could exist. This is exactly why the witness is required to be fresh.

Since the issue arises from using the same witness for different existentials, we might imagine using the following alternate idea.

 syntax witness 
     term ::= "ε" @binding(term) ", " sentence
 end

 axiom exists.elim [p(_) : sentence(term)] : (∃x, p(x))
     |- p(εx, p(x))
 end

Returning to our even-odd example, this time we would get that $\text{even}(\varepsilon x, \text{even}(x))$ and $\text{odd}(\varepsilon x, \text{odd}(x))$ which is not contradictory as $\varepsilon x, \text{even}(x)$ and $\varepsilon x, \text{odd}(x)$ are two different terms. This system does work. In fact, it is called Hilbert's Epsilon Operator and has certain uses in formal logic and set theory.

Why then are we not using the epsilon operator? The issue is that the epsilon operator actually implies the Axiom of Choice! To see why, consider a collection of non-empty sets $X$. Then construct the map $f : X \to \bigcup X$ defined as $x \mapsto \varepsilon y, y \in x$. We can prove that such a $y$ exists (every $x$ is non-empty) and so this is a valid choice function. We do not want our logical system to imply the Axiom of Choice so we will have to make some changes.

The trouble with the epsilon operator is that it allowed us to make an infinite number of parallel choices. Extracting a witness from an existential should behave less like a function and more like a reasoning step. To try and enforce this we might imagine using the same witness term as above but with the following new axiom:

 axiom exists.elim [p(_) : sentence(term)] [q : sentence] 
     : (∃x, p(x)) (p(εx, p(x)) → q)
     |- q
 end

The idea behind this axiom is that we don't actually get to extract a witness for any proposition, we just get to imagine we could do so for one particular proposition. However, this axiom is no different from the previous axiom. By simply setting $q$ to be $p(\varepsilon x, p(x))$ we extract the previous, bad, axiom.

The issue is that the witness itself appears in the conclusion we are drawing. However we can use a trick to prevent this: we include the conclusion we want in the witness term. This brings us to the final existential elimination axiom we will actually be using.

951syntax witness
952    term (000) ::= "∃ᵉ" @binding(term) ", " sentence " ⊢ " sentence
953end

955axiom exists.elim [p(_) : sentence(term)] [q : sentence] 
956    : (∃x, p(x)) (p(∃ᵉx, p(x) ⊢ q) → q)
957    |- q
958end

We may read the syntax $\exists^e x, p(x) \vdash q$ as "the witness for the existential $\exists x, p(x)$ which will be used to prove $q$." The fact that $q$ is embedded into the witness prevents us from proving the axiom of choice. The reason is that if we attempt to define a proof function in the same way as before, we will no longer be able to apply the existential elimination axiom to all the witnesses simultaneously. The goal in the existential elimination cannot name the witness. So we must finish the proof as the next step after applying the axiom and thus won't be able to quantify over all witnesses.

Using these two axioms we can prove the introduction and elimination rules for $\forall$ as theorems. The $\forall$ elimination rule is the dual of the $\exists$ introduction rule:

974theorem forall.elim [p(_) : sentence(term)] [a : term] : (∀x, p(x))
975    |- p(a)
976proof
977    -- we rewrite the forall as an existential
978    have ¬∃x, ¬p(x) from ∀x, p(x);
979    
980    -- and then if ¬p(a) we have a counterexample to the above
981    assume ¬p(a) for_contra;
982    thus ∃x, ¬p(x) by exists.intro [¬p(_)] [a];
983
984    -- which leads to a contradiction
985    contradiction
986qed

The $\forall$ introduction rule is dual to the $\exists$ elimination rule. Traditionally, we would pick a fresh variable to prove the property of and then deduce that the property must hold for all variables. Here, our existential witnesses serve as the arbitrary variable.

993theorem forall.intro [p(_) : sentence(term)] : (p(∃ᵉx, ¬p(x) ⊢ ⊥))
994    |- ∀x, p(x)
995proof
996    assume ∃x, ¬p(x) for_contra;
997
998    -- from the existential we extract the witness. the specific x such that
999    -- ¬p(x). we had p(x) as our hypothesis, chosen to create a contradiction
1000    -- here. of course, the point is it shouldn't matter what value we had as
1001    -- the witness in our hypothesis; all should be equally easy to prove.
1002    assume ¬p(∃ᵉx, ¬p(x) ⊢ ⊥) then ⊥ as contradiction;
1003
1004    -- then we extract the conclusion from the existential
1005    thus ⊥ by exists.elim [¬p(_)] [⊥];
1006qed

As you can see, using the witnesses can be quite cumbersome. We can abstract these four rules into the following tactics:

The existential introduction rule becomes:

1012tactic justification.using
1013    justification ::= kw:@kw"using" use:@fragment(term)
1014end

The existential elimination rule becomes:

1017grammar_category obtain_vars

1019tactic tactic.obtain
1020    tactic ::= @kw"obtain" list:obtain_vars just:justification ";" next:tactic
1021end

1023tactic obtain_vars.last
1024    obtain_vars ::= var:@name @kw"st" st:@fragment(sentence)
1025end

1027tactic obtain_vars.more
1028    obtain_vars ::= var:@name @kw"and" rest:obtain_vars
1029end

1031tactic obtain_vars.more_st
1032    obtain_vars ::= var:@name @kw"st" st:@fragment(sentence) @kw"and" rest:obtain_vars
1033end

This is the forall introduction rule:

1036tactic tactic.arbitrary
1037    tactic ::= kw:@kw"arbitrary" var:@name ";" next:tactic
1038end

1040tactic tactic.arbitrary_st
1041    tactic ::= kw:@kw"arbitrary" var:@name @kw"st" st:@fragment(sentence) ";" next:tactic
1042end

And here is the forall elimination rule:

1045tactic justification.specializing
1046    justification ::= @kw"specializing" forall:@fragment(sentence)
1047end

We can see these all play nicely together in the following classic theorem (which will be the first theorem using a predicate on two terms).

1052notation sentence.with_term_term
1053    sentence (1000) ::= @name "(" term ", " term ")"
1054end

1056theorem exists_forall.swap [p(_0, _1) : sentence(term, term)] : (∃x, ∀y, p(x, y))
1057    |- ∀y, ∃x, p(x, y)
1058proof    
1059    obtain x' st ∀y, p(x', y);
1060    arbitrary y';
1061    follows p(x', y') specializing ∀y, p(x', y);
1062    thus ∃x, p(x, y') using x';
1063qed

With our development of quantifiers we have completed the traditional presentation of first order logic. In fact, it is called first order logic because the quantifiers quantifier over just one sort of object, terms. Everything we have done so far makes sense in almost any mathematical system. The next step on our journey is to introduce sentences and terms specific to our context, in this case set theory. However, before we do this, there is one extension we can make to our system that will make our lives easier.

The Iota Operator 2.3

Using the tools of Watson it is easy to define complex sentences that take other terms or sentences as arguments. This is because, in some sense, a sentence is self contained. However, terms do not behave this way. Thus far, the only terms we have defined come on the inside of quantifiers. This makes it impossible to define self contained terms.

 definition my_term
     foo := what could go here? we aren't in a quantifier
 end

This situation could be resolved if our specific mathematical language contained some primitive, self-contained terms for us to use. However, set theory is usually presented without any such self contained terms. Of course, mathematicians use self contained terms all the time. What do they mean by this? Take the empty set for example. Traditionally, it is understood that if you see a formula containing $\varnothing$ you are supposed to expand it using the following three rules:

$$x = \varnothing \overset{\text{def}}{\iff} \forall y, y \not\in x$$ $$\varnothing \in x \overset{\text{def}}{\iff} \exists y, y \in x \land y = \varnothing$$ $$x \in \varnothing \overset{\text{def}}{\iff} \bot$$

This is a significantly more complex notion of definition than the find and replace system that Watson supports. These notions could be instead be added as axioms, which is what the Metamath proof system does.

However there is a different way of thinking about term definitions we can use instead. A term is well defined if we know that it exists and we know that it is unique. We can introduce a new term into our formula language that represents the unique term with a given property. Following the tradition of the Principia Mathematica, this is called the iota operator and is denoted with an inverted iota.

1112syntax iota
1113    term (000) ::= "℩" @binding(term) ", " sentence
1114end

This term only has meaning if there is actually a unique object with the given property. Otherwise, it can be thought of as an arbitrary term.

1119axiom iota.unique [p(_) : sentence(term)] : (∃!x, p(x))
1120    |- p(℩x, p(x))
1121end

In the future we will make definitions in terms of this iota operator. One advantage of the iota operator over other systems is that it makes sense for any first order logical system, regardless of the particular predicates or terms that are present. Additionally it is a conservative extension meaning that every sentence containing an iota operator could be converted to one without and all sentences which correspond in this way will have the same truth value. This means that the iota operator is just a notation convenience and doesn't fundamentally change our system.

With all the pieces in place, we are ready to begin set theory.