Need help understanding variable label/scoping rules for first order logic

Question

I don't understand when we're allowed to use what label when we're writing a proof in first order logic.

During $\forall$-intro we introduce a new variable $c$ and then close out with something in terms of $x$:

Given arbitrary c from the domain:  [potentially problematic line]
   ...
   P(c)
∀x P(x)  [potentially problematic line]

And during $\exists$-elim we introduce a new variable $c$:

∃x P(x)
Given c from the domain such that P(c):  [potentially problematic line]
    ... 
    Q   [some line that has no dependency on c so we can pull it out]
Q

But with $\forall$-elim we're also introducing a new label $c$:

∀x P(x)
P(c)  [potentially problematic line]

And with $\exists$-intro we're potentially introducing a label $x$:

P(c)   
∃x P(x)  [potentially problematic line]

What I don't understand are when we're allowed to use what label. In each case, what must I "watch out for"? I can't tell when something needs to be a completely new label, versus when I can re-use a label again. Do I have to check for conflicts with things inside the current and any super-contexts? Or just the headers? Both? I just don't understand at all.

Answer 1

Four rules: we will start from the simple ones.

Universal instantiation (or : elimination) rule formalizes the intuitive principle :

"what hold of all holds of any".

In other terms, to say that $\forall x P(x)$ holds, means to say that every element in the "universe" of the interpretation will have property $P$.

Thus, let $t$ denotes an object whatever: we may safely assert that $t$ has property $P$, i.e. that $P(t)$ holds as well.

Thus :

$\forall x P(x) \vdash P(t)$.

Note : as usual, the language of FOL is made of : predicate symbols: $P_i$; function symbols: $f_i$; constant symbols: $c_i$; individual variables: $x_0, x_1,\ldots$ (countably many); connectives and quantifiers.

A term is : either a constant $c_i$ or a variable $x_i$, or an expression $f_i (t_1,\ldots, t_n)$, where $t_1,\ldots, t_n$ are terms.

---

Regarding Universal generalization (or : introduction) :

$\text { if } \Gamma \vdash \varphi, \text { then } \Gamma \vdash \forall x \varphi$,

we have to consider that the rule holds with a proviso : "provided that $x$ does not occur free in $\Gamma$".

(Obviously, when $\Gamma = \emptyset$, there is no $x$ free in it, and thus the rule becomes : $\text { if } \vdash \varphi, \text { then } \vdash \forall x \varphi$.)

What is the meaning of the proviso ?

Its role is to formalize the intuitive rule that if we can prove that "property" $P$ holds for an arbitrary element of the "universe", without using any information about it, then $P(x)$ must be true regardless of what element $x$ is, and this means that $∀x P(x)$ must be true.

---

Compare now with Existential introduction :

$\varphi[x/t] \vdash \exists x \varphi$.

The rule has no proviso on $t$.

Obviously, it is enough that $P$ is true of some (at least one) element $t$ in the universe, to license us to assert that $\exists x P(x)$ is true.

---

And we are left with Existential elimination:

$$\dfrac{\Gamma \vdash \exists x \ \varphi\qquad \Delta, \varphi[x/t] \vdash \psi}{\Gamma, \Delta \vdash \psi}.$$

Also this rule has the proviso that the term $t$ to be used must be "new", in the sense of having no other occurrences in the proof, except for $\varphi[x/t]$.

Again, the intuition is not very difficult. How can we deduce something from the assumption that "There is a $P$" ? We proceed by writing "Let $t$ be a $P$" (a new temporary assumption) and then we use it in order to derive further statements.

If in the proof we have used no additional properties about $t$, except for the fact that $t$ is a $P$, and the conclusion that we have reached does not contain $t$, we could safely discharge the temporary assumption and assert that the conclusion depends only on the fact that there is a $P$.

---

---

Note : rules can be expressed either using free variables and terms (see van Dalen, page 91 and Chiswell & Hodges, page 177) or, following Gentzen's original presentation, with individual parameters : $a,b,c$ (see Natural Deduction : Rules for Quantifiers), that are always used free, while symbols $x,y,z$ are used for bound variables.

Answer 2

The Universal Elimination and Existential Introduction have no 'potential issues'!

For Universal Instantiation: If $\forall x \ P(x)$ is true, then that literally means that everything has propoerty $P$. Hence, you can instantiate the variable with any constant (or, in general, variable-free term), and that always works. That is, I can infer $P(a)$, $P(b)$, $P(c)$, $P(f(a))$, etc. whether or not any of those constants or variable free terms already occur elsewhere in the proof or not.

The same goes for Existential Introduction: if you have that $P(a)$, $P(b)$, $P(c)$, $P(f(a))$, etc., then you can definitely infer $\exists x \ P(x)$, without worrying that there is some issue or conflict, for in all cases there is definitely something with property $P$.

Answer 3

For universal instantiation (elimination) and existential introduction we are not introducing a "new" "label" or a new anything. Universal instantiation states that if we've derived $\forall x.P(x)$ and we have a particular term $t$, then we can derive $P(t)$. $t$ can be any term, it doesn't need to be a variable or constant. $\forall x.P(x)$ allows us to derive $P(1+1)$ by choosing $t=1+1$. You have to already have the term $t$ to apply universal instantiation. There is nothing "new" that's being created. The story is basically the same for existential introduction.

It's universal generalization (introduction) and existential elimination that have the weird side-conditions. It is common when defining the terms of a logic to add a (usually countably infinite) set of variable terms. You will see a definition like (e.g.): A term is a variable from some denumerable set of variables $V$ or it is a function symbol applied to a tuple of terms compatible with the arity of the functional symbol. $V$ is a fixed set throughout their discussion. Fixing $V$ is a mistake, in my opinion, that makes things less clean and more complicated. Instead, the notion of term should be explicitly parameterized by the set of variables $V$. We can use the exact same definition but just say that it is defining "terms-with-variables-in-$V$". This leads to the notion of formula also being parameterized by $V$, i.e. "formulas-with-variables-in-$V$".

There are a lot of benefits to this approach^1,2. First, we no longer need an infinite set of variables. Any term or formula or derivation can only use a finite number of variables. Relatedly, we no longer need to give semantics to an infinite number of variables even though all but finitely many of them are unused. It has other benefits for the semantics that I won't elaborate on here. Next, a closed term/formula is simply a term-/formula-with-variables-in-$\varnothing$. However, the key thing in this case is the slight change to the definition of formula. We get: A formula-with-variables-in-$V$ is of the form (...the usual stuff...) or $Qx.\varphi$ where $Q$ is a quantifier and $\varphi$ is a formula-with-variables-in-$(V\cup\{x\})$.

Just like terms-with-variables-in-$V$ led to formulas-with-variables-in-$V$, formulas-with-variables-in-$V$ lead to derivations-with-variables-in-$V$. $\Gamma\vdash_V\varphi$ states that given a list of premises, $\Gamma$, consisting of formulas-with-variables-in-$V$ and a formula-with-variables-in-$V$, $\varphi$, we can derive $\varphi$ from $\Gamma$. Of course, the need for this is to handle the quantifiers. In particular, universal generalization and existential elimination can be written as³: $$\dfrac{\Gamma\vdash_{V\cup\{x\}}\varphi\qquad x\notin V}{\Gamma\vdash_V \forall x.\varphi}\qquad\dfrac{\Gamma\vdash_V \exists x.\varphi\qquad \Gamma,\varphi\vdash_{V\cup\{x\}}\psi\qquad x\notin V}{\Gamma\vdash_V \psi}$$

In fact, if we were willing to change the syntax so that $Qx.\varphi$ was a formula-with-variables-in-$V$ only when $x\notin V$, then we could drop the side-condition on the universal generalization rule. The cost would be that formulas like $\forall x.(\forall x. P(x))$ would be ill-formed. Note that there is a bit of a subtlety with the existential elimination rule. For $\Gamma\vdash_V\psi$ to make sense, $\psi$ has to be a formula-with-variables-in-$V$. For $\Gamma,\varphi\vdash_{V\cup\{x\}}\psi$ to make sense, $\psi$ needs to be a formula-with-variables-in-$(V\cup\{x\})$. We are implicitly lifting $\psi$ to a formula-with-variables-in-$(V\cup\{x\})$ which makes sense because formula-with-variables-in-$V$ aren't required to use all the variables in $V$, and so we can view them as formula-with-variables-in-$V'$ for $V'\supseteq V$ that just don't use any of the extra variables. All this is to say that $x$ is not allowed to occur free in $\psi$.

Universal instantiation and existential introduction can be written as: $$\dfrac{\Gamma\vdash_V\forall x.\varphi}{\Gamma\vdash_V\varphi[t/x]}\qquad\dfrac{\Gamma\vdash_V\varphi[t/x]}{\Gamma\vdash_V\exists x.\varphi}$$ where in both cases $t$ is a term-with-variables-in-$V$ and $\varphi[t/x]$ means $\varphi$ with all free occurrences of $x$ replaced with $t$. If $\varphi$ is a formula-with-variables-in-$(V\cup\{x\})$ and $t$ is a term-with-variables-in-$U$, then $\varphi[t/x]$ is a formula-with-variables-in-$(V\cup U)$. In particular, when $U=V$, this just produces a formula-with-variables-in-$V$, effectively eliminating $x$ from the set of variables (assuming it isn't in $U$ or $V$, but it is harmless if it is).

The system I've sketched above tells you exactly when you need a "fresh" variable and what that means (namely one not contained in the current set of variables parameterizing your derivation). For more traditional presentations, the side-conditions require checking through all the premises, but this presentation avoids that by making the set of free variables explicit and a parameter. In effect, this doesn't so much eliminate as incrementalize the freshness check by forcing you to keep track of free variables as you go. For either presentation, when working by hand the simplest thing to do for universal generalization or existential elimination is to simply introduce a variable that has not been used before anywhere in the derivation. This is stronger than necessary but can always be arranged. For existential elimination, we also need to make sure this variable doesn't occur in $\psi$ (your Q).

¹ Another aspect of making this choice is that we can no longer derive $\exists x.\top$ without additional axioms/rules (see https://math.stackexchange.com/a/3002858/305738). That is, the domain being non-empty is no longer required. You can easily add $\exists x.\top$ as an axiom (or add a constant) if you do want to enforce a non-empty domain.

² An approach like this is also fairly common when formalizing logics within mechanized proof assistants.

³ With respect to a Fitch-style layout of a derivation, $\Gamma$ would roughly consist of all the hypotheses and theorems that were derived earlier, i.e. all the lines above the current line. The statements above the line would be subderivations which, once completed, would warrant us adding the conclusion below the line as a new proven result in the current derivation (which might itself be some subderivation). You could imagine drawing a box around subderivations and labeling them with the free variables that are allowed to occur in them. Then you would just need to make sure that every formula only used the variables labeling the box. Universal generalization and existential elimination would introduce new sub-boxes labeled by any variable of your choice which doesn't occur in any containing box.