How is a quantifier-free formula actually interpreted?

Question

A quantifier-free formula in FOL is simply a formula:

-that contains no quantifiers.

-it possibly has free variables.

How is such a formula interpreted?

My understanding is that if we're interested in satisfiability, we agree to take the existential closure of the formula.

Now consider a formula in the theory of reals which asks if the following statement is satisfiable:

$\exists x. ax^2 + bx + c=0$

According to the book "The Calculus of Computation" by Bradley and Manna, without quantifiers, free variables and constants play the same role. See for instance the example 3.1, p.72 in the book. A way to see this is to replace a quantifier-free formula by its existential closure and then replace the existentially quantified variables by fresh Skolem constants. So, then the above formula is equivalent to the following quantifier-free formula:

$ax^2 + bx + c=0$

Clearly this doesn't count as "quantifier elimination" at least not from the point of view of solving this quadratic! What am I missing?

Answer 1

OK, Leo provides a very nice answer here https://stackoverflow.com/questions/16762337/eliminating-forall-using-unsat?rq=1 but the short answer is that the two formulae above (the first one with the existential and the 2nd one with the Skolem constants) are not equivalent but equisatisfiable. QE produces equivalent formulae, but Skolemization doesn't therefore it is not considered QE.

Answer 2

How to interpret a formula with free variables ?

In mathematics, we usually have two kind of "equations" :

• $(x+1)(x-1)=x^2-1$

• $x^2-2x+1=0$

The first one is an identity and it is clearly implicitly universally quantified; i.e. it must be read as :

$\forall x [(x+1)(x-1)=x^2-1]$.

If we consider for simplicity the interpretation based on the domain $\mathbb N$ of natural numbers, and we instantiate it with a number $n$ whatever, we always get a true formula : $(n+1)(n-1)=n^2-1$, i.e. the "matrix" (the sub-formula without the quantifier) is always satisfied.

This is simply a consequence of the logical axiom (or law) :

$\forall x \varphi \rightarrow \varphi_t^x$, where $t$ is substitutable for $x$ in $\varphi$.

---

Formula $x^2-2x+1=0$, instead, must not be read as universally quantified, because it is simply false that every number $n \in \mathbb N$ satisfy it.

It must be read as :

$\exists x (x^2-2x+1=0)$.

How to interpret $x^2-2x+1=0$ with $x$ free ? To do this, we have to assign a "temporary" denotation to the free variable: this can be done in more than one way (all more or less equivalent).

We can, for example, use a variable assignement function $s : Var \to D$ where $Var$ is the set of variables of the language and $D$ is the domain of the interpretation : in our example $\mathbb N$.

Thus, if we consider the function $s$ that assigns to $x$ the number $0$ we have that :

$(x^2-2x+1=0)[s]$

is clearly false, because : $0-2 \times 0 +1 = 1 \ne 0$. We say that $s$ does not satisfy the formula.

If we consider instead the function $s'$ that assigns to $x$ the number $1$ we have that :

$(x^2-2x+1=0)[s']$

is true, because : $1-2+1 = 0$, and we say that $s'$ satisfy the formula (by the way, this shows that the formula $\exists x (x^2-2x+1=0)$ is true in $\mathbb N$, due to the fact that we have found a variable assignment that satisfy its "matrix").

The above argument is also the explanation of the assertion that "free variables and constants play the same role"; in order to show the satisfiability of a formula with a free variable, we treat the variable as a "temporary" name for an object in the domain of the interpretation (we assign to $x$ a denotation through the variable assignment function $s$).