I'm looking for an algorithm to decide if a given first order formula over a fixed vocabulary admits a logically equivalent existential one (i.e. a formula in prenex form where all quantifiers are existentials).

Is it known if such an algorithm exists or does not exist? At least when no functions symbols are admitted? And if it actually exists, which is its complexity?

I know that, given a formula, we can build an equivalent one in prenex form. However, here is an example which illustrates that a formula, equivalent to an existential one, admits also an equivalent prenex formula which is not existential:

Consider the vocabulary $L=\{E\}$, where $E$ is a binary relation symbol. Then the formula $$\exists x\,E(x,x)$$ which states that a directed graph admits a loop, is an existential formula and is equivalent to $$\exists x\forall y\,\,\,\,x=y\rightarrow E(x,y)$$ which is in prenex form, but not existential. So applying the algorithm to build a prenex form to the second formula would not produce an existential one.

  • $\begingroup$ The formula $\exists x\,E(x,x)$ is already prenex so why would any "prenexifying" algorithm change it? $\endgroup$ – David Richerby Feb 13 '19 at 15:34
  • $\begingroup$ Exactly. The same also holds for $\exists x\forall y\,x=y\longrightarrow E(x,y)$. So simply prenexifying $\exists x\forall y\,x=y\longrightarrow E(x,y)$ would not allow us to obtain the equivalent existential form $\exists x\,E(x,x)$. $\endgroup$ – POA Feb 13 '19 at 15:41

Surely, no such algorithm can exist in the general case: for a statement of the form $\forall x.\varphi$ statement in arithmetic, with $\varphi$ quantifier-free, there is a $\exists y.\psi$ statement such that

$$ \forall x.\varphi\ \Leftrightarrow \exists y.\psi$$

if and only if the statement is $\Delta_0$, aka decidable. Because $\forall$ statements are undecidable in general, such an algorithm cannot exist.

Edit: The above reasoning is wrong! Indeed, the Bernays-Shönfinkel class of formulas includes the set of $\forall^*\exists^*$ formulas without function symbols (but with arbitrary relational symbols) and is decidable. The $\Delta_0$ statements of arithmetic are not strictly speaking, quantifier free, but only contain bounded quantifiers (which are still quantifiers in FOL!)

However, this suggests an alternate proof: if there were a decision procedure which decides whether an arbitrary sentence were equivalent to some $\exists^*$ sentence, then there would be a decision procedure for arbitrary (function-free) formulas as follows:

Given $\phi$ check whether it is equivalent to an existential formula $\psi$. If it is not, $\phi$ is not provable (otherwise it would be equivalent to the formula $\exists x.\top$).

If it is, then find such a $\psi$ (it's easy to show this is possible) and apply the decision procedure for the B-S class.

Finally, an exercise: repair the above proof using the undecidability of arithmetic.

| cite | improve this answer | |
  • $\begingroup$ @F.D.C. I'm mistaken, this fragment is actually decidable! I'll amend. $\endgroup$ – cody Feb 13 '19 at 16:30

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.