Let $A \in WFF_{FOL}^\Sigma$ be an open formula, ie. it has occurrences of free variables. How do you transform this formula into a closed formula $B$?

It is my impression that you do this by adding, for each free variable in $A$, a universal quantifier to capture that variable. e.g., if $A = \exists x R(x,y,z)$, then $B = \forall y \forall z (\exists x R(x,y,z))$, and $A ↔ B$. Another example; $A = \exists x R(x,y) → \forall x P(x,z)$, $B = \forall y \forall z (\exists x R(x,y) → \forall x P(x,z))$Since all the quantifiers that you add to $A$ are universal, I also think that the order that you add these quantifiers in does not matter.

Logical Equivalence?
It turns out that, with the definitions that I am working with, translating an open formula to a closed formula yields a closed formula that is satisfiable in the same structure as the open formula. Logical equivalence is a special case of this. If you are working with other definitions, it may be that you get logically equivalent formulae by translating from open to closed formula.

Definitions ($A$ and $B$ are formulae, $M$ is a structure, $v$ is an assignment)
$A$ is valid iff for all structures $M : M ⊨ A$
$B \Rightarrow A$: $\forall v. M \models_v B → A$
$B \models A$: $\forall M. \, \text{if} \, (\forall v. M \models_v B) \, \text{then}\, (\forall u . M \models_u A)$
If $A$ and $B$ are closed formulae: $B \models A$ iff $B \Rightarrow A$. (This does not hold, in general, for open formulae.)
$A \Leftrightarrow B$ iff $A \Rightarrow B$ and $B \Rightarrow A$ (logical equivalence)

  • $\begingroup$ In this case, it makes a very important difference which logic text you follow. Could you mention the definition your book uses for the logical validity of a formula with free variables? There are several inequivalent definitions in practice. $\endgroup$ May 11, 2014 at 11:43
  • $\begingroup$ @Mauro ALLEGRANZA: If I remember correctly, having taught out of it, the definitions Enderton uses imply that a formula $\phi$ is not, in general, logically equivalent to its universal closure $\phi'$. He gets the weaker result that $\models \phi$ if and only if $\models \phi'$. Other authors have different definitions. $\endgroup$ May 11, 2014 at 11:57
  • $\begingroup$ @CarlMummert - you remember well... Of course, we have that, for $\alpha(x)$ with $x$ free : $\forall x \alpha(x) \vDash \alpha(x)$, but not $\alpha(x) \vDash \forall x \alpha(x)$ (see page 88). $\endgroup$ May 11, 2014 at 12:24
  • $\begingroup$ @CarlMummert - in Mendelson, instead, we have that $\vDash_M \mathcal B$ iff $\vDash_M \forall x \mathcal B$ (see page 61). $\endgroup$ May 11, 2014 at 12:29
  • $\begingroup$ @CarlMummert I intended to translate an open formula to a closed one in order to prove it. But now I'm not so sure that this is a valid strategy, since it does not preserve logical equivalence. And the book does not seem to mention proving open formulae, in particular (ie. it only seems to give example of formulae that may be open or closed). Maybe I should try to find a counter-model instead $\endgroup$ May 11, 2014 at 14:36

2 Answers 2


Can be useful to know the textbook you are using.

I'll refer to Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001).

The axioms are [see page 112] :

The logical axioms are all generalizations of wffs of the following forms, where $x$ and $у$ are variables and $\alpha$ and $\beta$ are wffs:

  1. Tautologies;

  2. $\forall x \alpha \rightarrow \alpha[x/t]$, where $t$ is substitutable for $x$ in $\alpha$;

  3. $\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$;

  4. $\alpha \rightarrow \forall x \alpha$, where $x$ does not occur free in $\alpha$.

If the language includes equality, the usual axiom for it are added.

Modus ponens is the sole rule of inference.

The basic definition [see page 88] is :

Definition. Let $\Gamma$ be a set of wffs, $\varphi$ a wff. Then $\Gamma$ logically implies $\varphi$, written $\Gamma \vDash \varphi$, iff for every structure $\mathcal A$ for the language and every function $s : V \rightarrow |\mathcal A|$ [where $V$ is the set of variables of the language] such that $\mathcal A$ satisfies every member of $\Gamma$ with $s$, $\mathcal A$ also satisfies $\varphi$ with $s$.

We say that $\varphi$ and $\psi$ are logically equivalent iff $\varphi \vDash \psi$ and $\psi \vDash \varphi$.

Consider now the formula $\varphi := x = y$.

We have :

$\vdash \forall x (x = y) \rightarrow x = y$, by Ax.2.

Thus, using modus ponens :

$\forall x (x = y) \vdash x = y$,

and, by soundness :

$\forall x (x = y) \vDash x = y$.

But $x = y \nvDash \forall x (x = y)$.

To show this, consider an interpretation with domain $\mathbb N$ and let the number $0$ assigned to $x$ and $y$; clearly we have that $0=0$ is true and $\forall x (x = 0)$ is false.

Thus, by the above definition of logical implication :

$x = y \nvDash \forall x (x = y)$.

Note. Considering your symbolism, we have found $\mathcal M$ and $v$ such that $\mathcal M \nvDash_v B \rightarrow A$.


Some authors adopt "restrictions" in order to prevent this kind of "unpleasant" situations.

See Dirk van Dalen, Logic and Structure (5th ed - 2013), page 67 :

Definition 3.4.4 (iv) : $\Gamma \vDash \varphi$ iff (if $\mathcal A \vDash \Gamma$, then $\mathcal A \vDash \varphi$), where $\Gamma \cup \{ \varphi \}$ consists of sentences.


In Metamath, both $φ ⊢ ∀ \: x \: φ$ and $∀ \: x \: φ ⊢ φ$ are provable whether $x$ occurs in $φ$ or not (1, 2). $φ → ∀ \: x \: φ$ and $∀ \: x \: φ → φ$ are also provable, but the first only if $x$ does not occur in $φ$ (3, 4). Allegranza's answer instanciates $φ$ both with $0 = 0$ and $x = 0$.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .