Question

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.

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top