Proving that the closure of a closed formula is the formula itself

Question

Closed Formula. A formula (in a first order language) is said to be closed if it has no free variables.

Closure of a Formula. Let $A[x_0, . . . , x_{n−1}]$ be a formula (in a first order language) whose free variables are among $x_0, . . . , x_{n−1}$ and $x_{n−1}$ is free in $A$, where $x_0, . . . , x_{n−1}$ are the first $n$ variables in alphabetical order. We call $\forall x_{n-1}\ldots\forall x_1\forall x_{0}A$ the closure of $A$.

Question.

Using these definitions, how can I show that if $A$ is closed, it is its own closure?

---

I thought that I will begin by assuming that $Q$ is the closure of $P$. But I don't understand what exactly it is that I need to show. Do I need to show that $P\leftrightarrow Q$ or that they are syntactically exactly same formula or something else? In any case I don't how to proceed. Can anyone help?

Answer 1

The definitions as stated may be problematic. Take any closed formula $A$. Then by the first definition $A$ has no free variables. Thus there is no natural number $n$ such that $x_{n-1}$ is a free variable in $A$, and so the second definition does not apply to $A$ and hence does not define the closure of $A$.

If the text from which these definitions come implicitly assumes that the second definition defines the closure for every formula, then the text is simply wrong. If however, the text does not assume that, then it must either specify later that the closure of a closed formula is itself, or it must never use that fact, since it cannot be proven from the two given definitions simply because of the above reason.

In any case, one correct way to define the closure of an arbitrary formula is as follows:

(This definition follows the textbook's convention that the permitted variables are $x_0,x_1,x_2,\cdots$.)

Take any first-order formula $A$. Let $n$ be the smallest natural number such that $x_k$ is not a free variable in $A$ for every $k \ge n$. Then define the closure of $A$ to be $\forall x_0\ \cdots \forall x_{n-1}\ ( A )$, where the imprecision notation "$\forall x_0\ \cdots \forall x_{n-1}$" is meant to be interpreted as the string of quantifiers over the first $n$ variables, which is empty if $n = 0$.

This definition is (unlike the one in the question) well-defined for all formulae, because every formula only contains finitely many variables, and hence the required $n$ always exists. Also, this definition satisfies the property that the closure of a closed formula is itself, which is easy to prove.

Anyway note that such a definition of closure is only compatible with the syntactical flavour of first-order logic that allows variable shadowing, namely that a quantified variable may be used outside the scope of the quantifier, such as in "$P(x,y) \land \forall y,z\ ( P(x,y) \land P(x,z) \to y=z )$", where the outer $y$ is shadowed by the quantified $y$ inside the scope of the quantifier. In practice this is a bad idea as it is confusing, but it is still often used in a formal definition of first-order logic.

Another definition of closure that is compatible even with flavours of first-order logic that do not allow variable shadowing is as follows:

(This definition does not care what the permitted variables are.)

Take any first-order formula $A$. Let $v_{1..n}$ be the sequence of free variables in $A$ in order of their first occurrences. Then define the closure of $A$ to be $\forall v_1\ \cdots \forall v_n\ ( A )$, where the imprecision notation "$\forall v_1\ \cdots \forall v_n$" is meant to be interpreted as the string of quantifiers over the sequence $v$ of variables, which is empty if $n = 0$.

Again, this definition applies to all formulae, and it is easy to prove that the closure of a closed formula is itself. Furthermore, this closure only adds the quantifiers needed, which is exactly what we would do in practice.

Answer 2

You need to show that the formulae are syntactically equal.

The closure of a formula $\phi$ is the formula $\forall x_1 \ldots \forall x_n.\phi$ where $fv(\phi) = \{ x_1, \ldots, x_n \}$. If $\fv(\phi) = \emptyset$, then we of course will not prefix $\phi$ with any quantifiers, and the result is obvious just $\phi$.

Answer 3

According to the definition, if the formula $A$ is closed, it has no free variables.

Thus, there is no $n$ such that:

the free variables of $A$ are among $x_0, \ldots,x_{n−1}$ and $x_{n−1}$ is free in $A$.

Thus, the closure of $A$ has no "added" universal quantifiers upfront, which means that it is $A$ itself.

---

If we have a formula $A$, like $x_2=c_1$, the definition gives us a "recipe" to produce its closure (in this case we have $n=3$):

$∀x_2∀x_1∀x_0(x_2=c_1)$

because we have to prenex the universal quantifiers for the first $n$ variables in alphabetical order.

If instead $A$ is $∃x_2(x_2=c_1)$, and we apply the definition:

"let $A[x_0,\ldots,x_{n−1}]$ be a formula whose free variables are among $x_0,\ldots,x_{n−1}$ and $x_{n−1}$ is free",

we get no $n$, because neither $x_2$ nor $x_1$ nor $x_0$ are free.

Thus, we have to "prenex" nothing and we get: $∃x_2(x_2=c_1)$ which is $A$ itself.

Note : in this case, it is not correct to say that $∀x_2∀x_1∀x_0(∃x_2(x_2=c_1))$ is the closure of $∃x_2(x_2=c_1)$.

Of course, the two are equivalent, because we can prove that:

if $x$ does not occur free in $\alpha$, then $\vdash \alpha \leftrightarrow ∀x \alpha$.