Converting to clausal form for using Resolution on formulas with free variables

Question

The resolution rule in first order logic is used with FOL sentences (formulas without free variables). Is it possible to do Resolution on general FOL formulas? If so, how does the conversion to clausal form should be done? The conversion is important because for sentences, we eliminate existential quantifiers and move universal quantifiers outside, and drop them. So the resulting clausal form implicitly universally quantified. If we have free variables, this produces problems with this universally quantification.

Answer 1

The "basic" use of Resolution is to show that a formula $\mathcal A$ is valid.

The method applies to $\mathcal B := \lnot \mathcal A$ trying to derive the empty clause : $\square$.

If so, we conclude that $\mathcal B$ is not satisfiable, and thus that $\mathcal A$ is valid.

---

Having said that, what is the definition of valid for an open FOL formula, i.e. a formula with free occurrences of variables ?

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

Definition 3.4.3 : Let $FV(\varphi) = \{ z_1,\ldots, z_k \}$, then $Cl(\varphi) := ∀z_1 \ldots \forall z_k \varphi$ is the universal closure of $\varphi$.

Definition 3.4.4 : (i) $\mathfrak A \vDash \varphi$ iff $\mathfrak A \vDash Cl(\varphi)$,

(ii) $\vDash \varphi$ iff $\mathfrak A \vDash \varphi$ for all $\mathfrak A$.

Thus, an open formula is valid iff its universal closure is.

Compare with Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 88 :

[A formula] $\varphi$ is valid iff for every $\mathfrak A$ and every [function] $s : Var \to |\mathfrak A|$, $\mathfrak A$ satisfies $\varphi$ with $s$.

And page 99 :

A formula $θ$ is valid iff $∀x θ$ is valid.

---

Thus, in order to apply resolution to an open FOL formula $\alpha(x)$, we have to apply the procedure to $\lnot \forall x \alpha(x)$. If this formula is unsatisfiable, then $\alpha(x)$ is valid.