Can you use Skolemization to reduce a formula to the variables you want it to be about? I was trying to think of a nice algorithmic way to do it but only ended up having problems.

Say you have a formula $G$ in prenex normal form, i.e. something looking like this:

$$G \equiv Q_1x_1...Q_nx_n\;F$$

where $Q_i$ are quantifiers binding variables $x_i$ and occuring exclusively on the left of formula $F$ (which, consequently does not contain quantifiers itself). It is known that $G$ can be transformed into Skolem normal form, i. e. all existential quantifiers can be eliminated by substituting the variables they are binding by functions. But can any variable be substituted so that in the end the formula expresses something about the variables you wish to keep?

The possibly cheapest way to do it involves bracketing $F$ with its nearest quantifier.

[EDIT: as you can read in the comments, this manoeuvre involves a major flaw, which shall stay undeleted for the record.]

If the quantifier nearest to $F$ is $\exists$, it would go like this:

$$Q_1x_1...Q_{n-1}x_{n-1}\;\exists x_n\;F$$ $$Q_1x_1...Q_{n-1}x_{n-1}\;(\exists x_n\;F)$$ $$Q_1x_1...Q_{n-1}x_{n-1}\;(F[x_n/c_1])$$

...where $F[x_n/c_1]$ expresses that $x_n$ has been substituted by constant $c_1$ in $F$.

If the quantifier nearest to $F$ is $\forall$, the procedure takes some extra legwork and two negations:

$$Q_1x_1...Q_{n-1}x_{n-1}\;(\forall x_n F)$$ $$Q_1x_1...Q_{n-1}x_{n-1}\;(\neg \exists x_n\;\neg F)$$ $$Q_1x_1...Q_{n-1}x_{n-1}\;\neg (\exists x_n\;\neg F)$$ $$Q_1x_1...Q_{n-1}x_{n-1}\;(\neg F[x_n/c_1])$$

Iterating the process for all bound variables would leave you with a formula with no quantifiers but many constants you cannot assume much about.

To sustain "expessive power" regarding the variables designated to stay, there ought to be a way to substitute the rest of the variables by functions with arities higher than 0. I was thinking of (if required, repeatedly) putting the formula in the following form:

$$Q_1x_1...Q_{n-1}x_{n-1}\;(\forall y_{k} ... \forall y_n\;\exists x_n F)$$ $$Q_1x_1...Q_{n-1}x_{n-1}\;(\forall y_{k} ... \forall y_n\;F[x_n/f(y_{k},..., y_n)])$$

...where $y_i$ shall be the variables preserved in the final form and $x_i$ the variables to be eliminated.

Two problems arise:

1) As any quantifiers can bind $y_i$ in the original prenex normal form, the existential quantifiers binding $y_i$ must first be rephrased into universal ones for the Skolemization to yield functions of $y_i$. This does not always lead to a chain of universal quantifiers with no negations in between. It seems like it's not always possible to get rid of the negation in $\forall y_i \; \neg \forall y_{i-1}$.

2) Consequently, opportunities to rephrase $Q_ix_i\; Q_{i+1}x_{i+1}$ as $Q_{i+1}x_{i+1}\;Q_ix_i$ are limited.

So far, I managed to fabricate formulas containing only the variables I picked as survivors in the initial stage. Anyway, I could not avoid constants in every case. Can you think of a procedure with rules that would prevent constants appearing in any resulting formula?


Your version of Skolemization is incorrect, and we can see this at the very first step. "$\forall xL(x)$" is not equivalent to "$\neg L(x/c)$:" while the former implies the latter, the latter doesn't imply the former (how do we know $c$ wasn't "chosen badly"?) Similarly, "$\exists x L(x)$" is not equivalent to "$L(x/c)$:" while the latter implies the former,the former doesn't imply the latter (for the same reason as above. So the way you've introduced constants is broken.

Skolemization doesn't introduce new functions - rather, it introduces new existential quantifiers over functions. E.g. the Skolemized version of "$\forall x\exists yL(x, y)$" is "$\exists F^1\forall x(L(x, F(x)))$." (The "$^1$" indicates that $F$ is a unary function symbol.)

Things get clearer once we have more than one existential quantifier. The Skolemized version of "$\exists x\forall y\exists z L(x, y, z)$" is "$\exists F^0\exists G^1\forall y(L(F^0, y, G(y)))$." Note two things here:

  • All the existential function quantifiers are together, at the front.

  • We've proceeded from the outside in: the $F^0$ corresponds to $x$, and the $G^1$ corresponds to $y$.

Basically, the Skolemized version of a formula "$\overline{Q}\overline{x}L(\overline{x})$" is "There are functions picking witnesses for the existential quantifiers in $\overline{Q}$ appropriately."

By the way, we can also perform "partial" Skolemization: we can Skolemize away any subset of the first-order existential quantifiers while leaving the rest. For instance, $$\forall x\exists y\forall z\exists w\forall a\exists b(L(x, y, z,w, a, b))$$ is equivalent to $$\exists F^1\exists G^2\exists H^3\forall x \forall z\forall a(L(x, F(x), z, G(x, z), a, H(x, z, a)))$$ (this is the fully Skolemized version), but it's also equivalent to the partially Skolemized sentence $$\exists F^1\exists H^3\forall x\forall z\exists w\forall a(L(x, F(x), z, w, a, H(x, z, a))).$$ Note that when we leave an existential quantifier alone it stays where it was - it doesn't move to the front.


Unless I misunderstand you, this doesn't work.

Say you have $\forall x \exists y Loves(x,y)$ : Everyone loves someone.

By your method you get (again, if I understand you correctly):

$\forall x Loves(x,c_1)$

But that can't be right, for that would imply that there is something $c_1$ that everyone loves. But if I have $a$ and $b$ (and not other objects in my domain) and $a$ loves $b$, $b$ loves $a$, but $a$ and $b$ do not love themselves, then $\forall x \exists y Loves(x,y)$ is true but $\forall x Loves(x,c_1)$ is false: $c_1$ cannot be $a$, and also not be $b$, and there are no other objects.

This is exactly why you can only eliminate existentials by using a function that shows that the 'something' is dependent on the choice of objects for the universal quantifiers in front of it: if I pick $a$, I can point to $b$ as the something that $a$ loves, but if I pick $b$, I point to $a$. So you have to think about this process 'outside-in', rather than 'inside-out'.

  • $\begingroup$ Nice, +1! While the one-quantifier step is already broken (see my answer), this drives the point home, and might be clearer to the OP. $\endgroup$ – Noah Schweber Jul 3 '17 at 15:24

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.