Why does Skolemming not preserve validity?

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.


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.


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.

Tags:

Logic

First Order Logic

Satisfiability

Related

If $\int_0^x f^2(t)dt \le f(x)$ for all $x \in [0,1]$, then $\min_{[0,1]} f(x) \le 1$? Find the values of $p$ and $q$ Then value of $\alpha^2 +4\alpha$ in Infinite series Can someone help me finish this: evaluate $S_n = \frac{x}{1-x^2}+\frac{x^2}{1-x^4}+ ... + \frac{x^{2^{n-1}}}{1-x^{2^{n}}}$ Combinatorics meaning of $L_m=\sum_{j=m}^{n}(-1)^{j-m}\binom{j-1}{m-1}S_j$ Finding the probability that someone has the disease, given they test positive on two tests Converse of Bolzano-Weierstrass theorem What sequences are Cauchy in all metrics for a given topology? Finding the complex square roots of a complex number without a calculator Prove that $\int_0^1\frac{\operatorname{Li}_3(1-z)}{\sqrt{z(1-z)}}\mathrm dz=-\frac{\pi^3}{3}\log 2+\frac{4\pi}3\log^3 2+2\pi\zeta(3)$ Evaluating $\int_{0}^{\infty} \frac{1}{a_{n}x^{n} + ... + a_{2}x^{2} + a_{o}}dx$ via Residue Theory? How to come up with a greedy solution and prove it?

Recent Posts