Logique du premier ordre arity définit de décidabilité?

Question

J'ai lu la logique du premier ordre est en général indécidable, et qui pourrait être décidable que lorsque l'on travaille avec des opérateurs unaires. (Je pense que la logique propositionnelle est, corrigez-moi si je me trompe)

La question est pourquoi arity conduit à des problèmes indécidables?

Je voudrais voir des documents de référence, ou au moins quelques simples exemple de celui-ci, comme un moyen de penser à ce passage de unaire à n-aire et pourquoi il conduit à des problèmes indécidables.

Answer 1

Logique avec unaire prédicats (non opérateurs), est appelée monadique . Ce qui est appelé propositionnelle logique que a arité prédicats, à savoir, les constantes true et false, et pas quantificateurs.

indécidabilité de la logique de prédicats suit parce que la logique prédicat (avec au moins un prédicat binaire) est puissant assez pour décrire comment fonctionne la machine de Turing , et nous pouvons exprimer dans la logique suffisamment compliquée déclarations sur les machines de Turing pour obtenir indécidabilité. En revanche, dans la logique monadique, où nous avons seulement prédicats unaires, nous ne pouvons pas décrire le fonctionnement d'une machine de Turing. Je suis ici délibérément vague pour donner une idée sans s'enliser dans des aspects techniques.

Answer 2

Comme Raphaël a dans un commentaire que vous demandez probablement sur l'indécidabilité du problème de décision classique des fragments de logique de premier ordre avec des prédicats unaires.

La recherche de fragments syntaxiquement restreints de la logique du premier ordre où la validité des formules est décidable est un domaine de recherche actif depuis plus de 100 ans. Il a été très tôt compris que ce sont les dépendances entre les variables qui rendent le problème de décision difficile. Et les dépendances sont mieux exprimées lorsque deux variables se produisent dans les arguments d'un prédicat. Par conséquent prédicats binaires ou des symboles fonctionnels (si vous permettez des symboles fonctionnels) sont essentiels pour indécidabilité.

Il était Löwenheim qui en 1915 a donné une procédure de décision pour la logique du premier ordre avec prédicats unaires. Si vous êtes intéressé, vous trouverez peut-être intrigant un document d'exposition intitulé « sur la décision classique problème » écrit par Yuri Gurevich sous la forme d'un dialogue de deux personnages fictifs. Le document a été publié dans le Bulletin de EATCS. ??

Le document introduit non seulement le problème, mais explique comment la recherche développée dans la recherche d'une classification complète des fragments décidables et indécidables en termes de préfixes quantificateurs.