Should equality, like any other predicate, involve only bound variables in a valid FOL sentence?

Question

I have found a nice interactive tutorial about sequent calculus. It contains all the inference rules for the first order logic (13 rules in the green box). One can also find these rules on Wikipedia.

For my project I need to extend these rules to the case of FOL with equality. I found this document, which seems to be exactly what I need. In particular, what I have found is that one need to add one more axiom (page 17):

$ \frac{}{\Gamma \implies \Delta, t = t} $

One also adds the following three derivation rules:

$ \frac{\Gamma, t = t \implies \Delta}{\Gamma \implies \Delta} $

$ \frac{\Gamma, t_1 = t_2, \phi(t_2) \implies \Delta}{\Gamma, t_1 = t_2, \phi(t_1) \implies \Delta} $

$ \frac{\Gamma, t_1 = t_2 \implies \Delta, \phi(t_2)}{\Gamma, t_1 = t_2 \implies \Delta, \phi(t_1)} $

---

What is not clear to me, is that equality is a binary predicate (predicate that takes two arguments). So, $t_1 = t_2$ is not a valid FOL sentence because a valid sentence should not contain free variables. In other words, if we have a predicate operating on some variables, then these variables should be "removed" by an existential of universal quantifier.

So, my question is: Can equality be applied to unbound variables?

Maybe my problem is that I misinterpret the rule and the rule does not imply that there are unbound variables in the expressions.

ADDED:

To explain better what I mean, an example of a valid FOL sentence is:

$ \forall q_1 : ((\exists q_2 : A(q_1, q_2)) \land (\forall q_2 : B(q_1, q_2))) $

In the above expression, we have variables $q_1$ and $q_2$ but the whole expression does not "depend" on them because these dependencies are removed by the quantifiers.

Now, we can remove predicates $A$ or $B$ by equality. So, that instead of $A(q_1, q_2)$ we will have $q_1 = q_2$. In this case, equality will be applied to bound variables.

SO, it is not clear to me how equality can be applied to unbound variables. Or, in other words, if we have it, how should we interpret this expression? We say that $q_1 = q_2$ without saying anything about $q_1$ and $q_2$? So, what are $q_1$ and $q_2$ in this case?

Answer 1

If you want to stay in the realm of sentences, then yes, free variables are not allowed at all. However, a sequent calculus doesn't need to restrict itself to sentences; in fact, most presentations I've seen operate on sets of formulas (which personally I find annoying, but that's just my preference), which may or may not include free variables.

This is what's going on here. To quote from page $12$:

A sequent $S:=(\Gamma,\Delta)$ is a pair of formula sets

(emphasis mine). So there's no error either in the text or in your understanding of sentences, the text is simply setting up a different system than you were expecting.

---

It's a good idea at this point to carefully present the relevant completeness theorem for this sequent calculus. When only sentences are involved there are no difficulties, but once formulas enter the picture we have to be a bit careful. I'll follow the terminology from the text above.

First, the definitions (which differ a bit from most texts):

• Signatures and structures are defined in the usual way, except that we demand countability. This is a weird thing to do from a "pure logic" perspective, but in a computation-oriented context it makes sense - and by the downward Lowenheim-Skolem theorem, if we're restricting attention to countable languages we can also restrict attention to countable structures without affecting basic properties like validity, satisfiability, and entailment.

• An interpretation for a set of formulas $\Phi$ is then a pair $(\mathcal{S},\mathcal{V})$ where $\mathcal{S}$ is a structure and $\mathcal{V}$ is a variable assignment, that is, a map from the free variables of $\Phi$ (= the variables which are free in some element of $\Phi$) to (the underlying set of) $\mathcal{S}$.

  • Note that this differs from the usual meaning of "interpretation" in the semantics of first-order logic, where it is used instead to refer to the part of a structure giving meaning to the non-logical symbols.

• The notion of an interpretation satisfying a set of sentences is then defined in the usual Tarskian recursive manner. When an interpretation $(\mathcal{S},\mathcal{V})$ satisfies a set of formulas $\Phi$, we write "$(\mathcal{S},\mathcal{V})\models\Phi$" and say that the pair $(\mathcal{S},\mathcal{V})$ is a model of $\Phi$.

  • There's actually a bit of sloppiness in the text w/r/t the above two bulletpoints. The relevant notions are only introduced (e.g. in Definition $6$) for individual formulas in place of the *set of formulas $\Phi$, but later on (page $12$) everything is generalized to sets of formulas. In the above, I've written things as they should be.

With this in hand, we can state the completeness theorem:

Using the definition of $\vdash$ in the text, for all sequents $(\Gamma,\Delta)$, we have $$\Gamma\vdash\Delta\quad\iff\quad\forall \mbox{ interpretations }I, [\forall \gamma\in\Gamma(I\models\gamma)\implies \exists \delta\in\Delta(I\models\delta)].$$ (Technically the left-to-right direction is soundness, but due to its fairly trivial nature we generally consider it part of the completeness theorem. This is bad practice if we're working in a context where soundness isn't obvious of course, but that isn't happening here.)