Converting open first order logic formulae to closed formulae

Question

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)

Answer 1

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$.

Comment

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.

Answer 2

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$.