8
$\begingroup$

I'm wondering what exactly is meant when people say "Skolemization preserves satisfiability but not validity". I'm having trouble wrapping my brain around it because I think of Skolemization, when considered as an inference rule, to simply "be an okay thing to do" when working with a second-order formula.

Skolemization is said to preserve satisfiability but not validity. What exactly do satisfiability and validity mean in the context? Does "co-Skolemization" (dual to Skolemization as a second-order equivalence) have similar properties as Skolemization?


Skolemization, as far as I can tell, is based on the equivalence between the first-order formula (and therefore degenerate second-order formula)

$$ \forall x_1 \cdots x_n . \exists y . P(x_1, \cdots, x_n, y) $$

and the following second order formula, that moves the $\exists$ in front of the $\forall$.

$$ \exists f. \forall x_1 \cdots x_n . P(x_1, \cdots, x_n, f(x_1, \cdots, x_n))$$

It makes perfect sense when the expression is thought of as a game. In the first expression, the opponent first makes $n$ moves and then the player makes 1. In the second expression, the player moves first but commits to a response function of sorts rather than committing to a single move. That's not a proof, but it seems like good intuitive justification for why rewriting an expression like this is okay in the first place.

It seems to me that performing this translation at all only makes sense if we're talking about a closed expression. That is, $P(\cdots)$ must have no free variables or, equivalently, $P$ must be an $n+1$-place predicate (primitive or defined).


In propositional logic, satisfiability and validity can be though of as describing what happens to free variables. All variables are free because there's no way to bind them.

$ P \lor P $ is satisfiable because the assignment $ \{ P = \top \} $ satisfies it.

$ P \lor \lnot P $ is a tautology for obvious reasons. I don't know whether it's right to say $ P \lor \lnot P $ is valid.

An inference rule that maps $P$ to $P \lor Q$ is valid (disjunction introduction).

A rule that maps $P$ to $P \land Q$ preserves satisfiability. We can take any old assignment $\mu$ and construct $\mu \cup \{ Q = \top \}$ which satisfies the new expression.

In the context of Skolemization, are the meanings of satisfiability and validity similar?


Let "co-Skolemization" (probably has a real name) be the translation from

$$ \exists x_1 \cdots x_n . \forall y . P(x_1, \cdots, x_n, y) $$

to

$$ \forall f . \exists x_1 \cdots x_n . P(x_1, \cdots, x_n, f(x_1, \cdots, x_n)) $$

That seems just as legitimate as Skolemization, considered as an inference rule in a second-order setting. There's a caveat here that in a first-order theory definitions are provided for all fully saturated combinations of function symbols and arguments. Therefore "co-Skolemization" definitely takes us out of first-order land, but I don't know how relevant that is.

$\endgroup$
  • 3
    $\begingroup$ It's tangential to your question, but I don't understand your co-Skolemization. Why on earth would you need $f$ to take any inputs at all? In the first place, from the original "$\exists forall$" you immediately get "$\forall \exists$"... $\endgroup$ – user21820 Oct 7 '18 at 4:16
  • 3
    $\begingroup$ Then you're just plain wrong. As I stated in my first comment, it is a trivial first-order logic fact that "$\exists \forall$" implies "$\forall \exists$", and I don't know why you don't see that. Moreover, the reverse direction also trivially fails, so even satisfiability is not preserved. Consider "$\exists x \forall y ( x \ne y )$". $\endgroup$ – user21820 Oct 7 '18 at 9:41
  • $\begingroup$ @user21820 . removed reference to "co-Skolemization". Thanks. $\endgroup$ – Gregory Nisbet Oct 7 '18 at 19:23
  • 1
    $\begingroup$ @user21820: It appears that the "co-Skolemization" arose as "negate the sentence, Skolemize the negation, and then negate the result of that (including quantifiers binding the Skolem functions)". Since the higher-order Skolemization (which adds $\exists f$ bindings at the front of a sentence) preserves truth values, its dual would do likewise. $\endgroup$ – Henning Makholm Oct 8 '18 at 1:06
  • 1
    $\begingroup$ Perhaps it would be good if you can include that bit about the fact that the second-order Skolemization preserves truth, and that removing the outer second-order existential quantifier (and adding the symbol) preserves satisfiability, into your answer, along with the similar explanation about co-Skolemization. @GregoryNisbet, sorry for my error, which I've explained above. We can also view co-Skolemization as the second-order tautology: ∃x[1..k] ∀y ( P(x[1..k],y) ) ≡ ∀F ∃x[1..k] ( P(x[1..k],F(x[1..k])) ). $\endgroup$ – user21820 Oct 8 '18 at 5:36
7
$\begingroup$

A sentence is valid if it is true in every interpretation of its logical language.

A sentence is satisfiable if it is true in some interpetation of its logical language.

Since Skolemization adds new symbols to the logical language, I think it is useful to introduce concepts of relative validity and satisfiability:

Suppose $\mathcal L\subseteq \mathcal L'$ are logical languages, and $\mathfrak A$ is an interpretation of $\mathcal L$. Then,

  • An $\mathcal L'$-sentence is valid relative to $\mathfrak A$ if it is true in every extension of $\mathfrak A$ to an interpretation of $\mathcal L'$.
  • An $\mathcal L'$-sentence is satisfiable relative to $\mathfrak A$ if it is true in some extension of $\mathfrak A$ to an interpretation of $\mathcal L'$.

(Beware that "relative" validity and satisfiability is probably not standard terminology; I made it up for the purpose of this explanation).

Now, when we Skolemize an $\mathcal L$-sentence $\varphi$, we get an extended language $\mathcal L'\supseteq \mathcal L$ and an $\mathcal L'$-sentence $\varphi'$. This trades truth for satisfiability in the sense that

For every interpretation $\mathfrak A$ of $\mathcal L$ it holds that $\varphi$ is true in $\mathfrak A$ if and only if $\varphi'$ is satisfiable relative to $\mathfrak A$.

In other words, if $\varphi$ is true in $\mathfrak A$, then we can find some interpretation of the Skolem functions that makes $\varphi'$ true, and vice versa. But we have no guarantee that every possible interpretation of the Skolem functions will preserve the truth of $\varphi$ -- indeed, usually they won't (as Bram28's counterexample shows).

This means that if we just have $\varphi$ and is not looking at a particular $\mathfrak A$, the Skolemization preserves validity:

  1. $\varphi$ is satisfiable $\iff$
  2. There is some interpretation of $\mathcal L$ where $\varphi$ is true $\iff$
  3. There is some interpretation of $\mathcal L$ which extends to some interpretation of $\mathcal L'$ where $\varphi'$ is true $\iff$
  4. There is some interpretation of $\mathcal L'$ where $\varphi'$ is true $\iff$
  5. $\varphi'$ is satisfiable.

If we try to replicate this argument with "valid" instead of "satisfiable", we get stuck after step 3:

  1. Every interpretation of $\mathcal L$ extends to some interpretation of $\mathcal L'$ where $\varphi'$ is true.

Whereas the original (3) had two "some" that we could collapse to one in (4), here we have a combination of "every" and "some". And that cannot be collapsed to a simple statement about interpretations of $\mathcal L'$ and $\varphi'$ -- in particular it is not equivalent to $\varphi'$ being valid.

$\endgroup$
11
$\begingroup$

When the existentials that are being removed in the process of Skolemization are not preceded y universals, you simply use a new constant for the respective variables.

As such, consider the formula:

$$\exists x (P(a) \lor \neg P(x))$$

This is a valid formula, since in any domain there is always an object that will satisfy the formula $P(a) \lor \neg P(x)$, namely whatever object $a$ refers to.

However, if we Skolemize, we get:

$$P(a) \lor \neg P(b)$$

which is not a valid formula, since there is a domain and interpretation where this statement is false: make sure that $a$ and $b$ refer to different objects, and where the object that $a$ refers to does not have the property expressed by $P$, while the object referred to by $b$ does have that property.

$\endgroup$
  • $\begingroup$ Why is it not valid? You can have $a=b$, right? $\endgroup$ – Kevin Oct 7 '18 at 2:31
  • 4
    $\begingroup$ @Kevin Check the definition of "valid". It doesn't mean that the formula could be true if you cleverly choose meanings for the basic non-logical symbols (like $P,a,b$) in it. It means that the formula is guaranteed to be true no matter what meanings you give its basic non-logical symbols. $\endgroup$ – Andreas Blass Oct 7 '18 at 2:35
  • $\begingroup$ @AndreasBlass: That's a fine explanation, but it should be in the answer. $\endgroup$ – Kevin Oct 7 '18 at 2:37
  • 3
    $\begingroup$ I'm new to this subject, so this question might be silly, but the Skolemization as defined by OP is about switching the order of the quantifiers and creating a function for this. I don't see any of these here, so what is happening? Why did the existence quantifier disappear? How do you Skolemize without a forall quantifier? Where is the function? Thank you very much in advance :) $\endgroup$ – Pedro A Oct 7 '18 at 16:50
  • 1
    $\begingroup$ @PedroA Remember that constant symbols are just $0$-ary function symbols. The $b$ which is introduced is an $n$-ary function symbol, where $n$ is the number of universal quantifiers preceding the corresponding existential quantifier; since $n=0$ we're just looking at a constant symbol. $\endgroup$ – Noah Schweber Oct 7 '18 at 18:10
5
$\begingroup$

When you Skolemize, you drop the existential quantifier in front of $f$. Every structure that is a model of the original formula can be extended by providing an interpretation of $f$. Such an extension may or may not be a model of the Skolemized formula. Even though the original formula may be valid, the Skolemized formula doesn't have to be. What is guaranteed is that the two formulae are equisatisfiable.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.