¿La lógica de primer orden define la decidabilidad?

Question

He leído la lógica de primer orden es en general indecidible, y eso podría ser decidible solo cuando se trabaja con operadores unarios. (Creo que esa es la lógica proposicional, corrígeme si estoy equivocado)

La pregunta es ¿Por qué Arity conduce a problemas indecidibles?

Me gustaría ver algún material de referencia, o al menos algunos simples ejemplo De esto, como una forma de pensar en este pasaje de Unario a N-ARY y por qué conduce a problemas indecidibles.

Answer 1

Lógica con unary predicados (no operadores), se llama monádico. Lo que se llama de la proposición La lógica solo tiene anular predicados, es decir, constantes true y false, y sin cuantificadores.

los indecidibilidad de la lógica predicada sigue porque la lógica de predicado (con al menos un predicado binario) es lo suficientemente potente para Describe cómo funciona una máquina turing, y así podemos expresar en la lógica declaraciones suficientemente complicadas sobre las máquinas de Turing para obtener indecidabilidad. Por el contrario, en la lógica monádica, donde solo tenemos predicados unarios, no podemos describir el funcionamiento de una máquina de turing. Estoy siendo deliberadamente vago aquí para dar una idea sin empantanarse en los tecnicismos.

Answer 2

Como Raphael señaló en un comentario, probablemente esté preguntando sobre la decidibilidad del problema de decisión clásica para los fragmentos de la lógica de primer orden con predicados unarios.

La búsqueda de fragmentos restringidos sintácticamente de lógica de primer orden donde la validez de las fórmulas es decidible fue un campo de investigación activo durante más de 100 años. Se entendió muy temprano que son las dependencias entre las variables las que dificultan el problema de la decisión. Y las dependencias se expresan mejor cuando se producen dos variables dentro de los argumentos de un predicado. Por lo tanto, los predicados binarios o los símbolos funcionales (si permite símbolos funcionales) son esenciales para la indecidibilidad.

Fue Löwenheim quien en 1915 dio un procedimiento de decisión para la lógica de primer orden con predicados unarios. Si está interesado, puede encontrar un artículo de exposición intrigante titulado "Sobre el problema de decisión clásica"Escrito por Yuri Gurevich en forma de un diálogo de dos personajes ficticios. El documento se publicó por primera vez en el Boletín de EATCS.

El documento no solo introduce el problema, sino que explica cómo la búsqueda se convirtió en encontrar una clasificación completa de fragmentos decidibles e indecidibles en términos de prefijos de cuantificadores.