# How do I actually use free variables in first order logic?

I know what free variables are in the context of predicate logic, but I don't understand what they are supposed to accomplish.

Everything I have heard on the subject suggests that one of these is the case.

1. An unquantified $$\phi(x)$$ lacks a definite truth value.
2. An unquantified $$\phi(x)$$ is equivalent in meaning and truth value to $$\forall x (\phi(x))$$.
3. An unquantified $$\phi(x)$$ has semantic differences from $$\forall x (\phi(x))$$, but remains logically equivalent in terms of truth value. (i.e. $$B(x) \to A(x)$$ means "any bird is an animal", whereas $$\forall x (B(x) \to A(x))$$ means "all birds are animals", but the two still have the same truth value).

None of these answers seem satisfactory. The first option raises the question as to why free variables are considered syntactically valid at all, whereas the latter two make it seem like free variables are totally redundant. It's also odd that the sources disagree with each other in the first place; this seems like one of those things where there is one correct way and it's not up to opinion.

There's got to be something I'm missing here, but what is it?

• Number 2 is false. Consider the formula $x+2=3$ in a structure where $+$ is defined to be integer addition. That formula is only true for one value of $x$. Commented Dec 12, 2022 at 16:53
• @JohnDouma I've seen universal generalization frequently expressed as "$\phi(x)$, therefore $\forall \phi(x)$, so long as x does not appear in any other assumptions". By your example, it seems like this rule no longer holds if we introduce functions (like $+$ for integer addition) into the system.
– Nico
Commented Dec 12, 2022 at 17:00
• They are used to specify the scope of quantifier. Commented Dec 12, 2022 at 17:13
• In my opinion, having programmed some automated theorem provers, I don't consider any quantifier-free formula to be valid in FOL alone. It's usually just a convent shorthand for something which does have a quantifier. This becomes evident in very formal settings of set theory, for example, where there really is no such statement like $\emptyset\subseteq\emptyset$ existing on its own. Instead, we would formally write this as $\forall x(\forall y(y\notin x)\implies (\forall z(\forall w(w\notin z)\implies \forall t(t\in x\implies t\in z))))$. However, as you can tell, this is incomprehensible. Commented Dec 12, 2022 at 17:18
• @NicolinoWill I agree, my example is not that great, but your elaboration actually summarizes what I mean. A variable simply represents some constant, and all constants are defined, much like your example, through some quantifier. It's in this way I don't consider free variables as valid, as they are a sort of 'meaningless' atom, unless substituted with constants (which will end up quantified). But I am coming from a more philosophical perspective, coming from my research in automated theorem proving, where free-variables are unnecessary. Commented Dec 12, 2022 at 21:08

If a proposition with a free variable is true for all assignments of that free variable, then it's also true for all quantifications of that free variable, and so some authors consider it reasonable to say that the truth value of $$\phi(x)$$ is equal to the truth value of $$\forall x\phi(x)$$. This is your second bullet. This is not an equivalence. This is "syntactic sugar", and it only applies to propositions with free variables whose truth value we want (note that these did not have truth values prior to this decision, by bullet (1)). The subtlety is that $$\forall x\phi(x)\neq \exists x \phi(x)$$, which is the other way that we have of binding $$x$$. Moreover we cannot freely replace $$\phi(x)$$ with $$\forall x\phi(x)$$ because $$\exists x \phi(x) \to \exists x \forall x \phi(x)$$ is not even well-formed.