Décidabilité de l'équivalence aux formules existentielles

Question

Je recherche un algorithme pour décider si une formule de première commande donnée sur un vocabulaire fixe admet une formule existentielle logiquement équivalente (c'est-à-dire une formule sous forme prénex où tous les quantificateurs sont existentiels).

Est-il connu si un tel algorithme existe ou n'existe pas? Au moins quand aucun symbole de fonctions n'est admis? Et s'il existe réellement, quelle est sa complexité?

Je sais que, compte tenu d'une formule, nous pouvons construire un équivalent sous forme prénex. Cependant, voici un exemple qui illustre qu'une formule, équivalente à une formule existentielle, admet également une formule prénex équivalente qui n'est pas existentielle:

Considérez le vocabulaire $ L = {e } $, où $ E $ est un symbole de relation binaire. Puis la formule$$ existe x , e (x, x) $$qui stipule qu'un graphique dirigé admet une boucle, est une formule existentielle et équivaut à$$ existe x forall y , , , , x = y rightarrow e (x, y) $$qui est sous forme prénex, mais pas existentielle. Ainsi, l'application de l'algorithme pour construire une forme prénex à la deuxième formule ne produirait pas une forme existentielle.