Este artículo de wikipedia sobre lógica combinatoria dice que la lógica combinatoria, la lógica lambda y las máquinas de Turing son computacionalmente equivalentes, pero que ambas exceden el poder expresivo de la lógica de primer orden.
¿De qué manera exceden el poder expresivo de la lógica de primer orden?
¿Tenemos teoremas de integridad y solidez para Lambda/Lógica Combinatoria?
1: ¿De qué manera exceden el poder expresivo de la lógica de primer orden?
No sé si el cálculo lambda sin tipo y la lógica de primer orden se pueden comparar directamente, pero la teoría de tipo simple es un cálculo lambda con tipo y, al mismo tiempo, una formalización de la lógica de orden superior. Según wikipedia:
El cálculo lambda fue introducido por el matemático Alonzo Church en la década de 1930 [...]. Se demostró que el sistema original era lógicamente inconsistente en 1935 [...] en 1936 Church aisló y publicó solo la parte relevante para el cálculo, lo que ahora se llama cálculo lambda sin tipo. En 1940, también introdujo un sistema computacionalmente más débil, pero lógicamente consistente, conocido como cálculo lambda de tipo simple.
Como aprendí de "Las siete virtudes de la teoría de tipos simple", el sistema de prueba comúnmente utilizado para la teoría de tipos simple es equiconsistente con la teoría de conjuntos de Mac Lane . Esto, a su vez, se considera un "buen modelo" de "matemáticas predicativas". Hay rumores de que Randall Holmes tiene una prueba de que también New Foundations de Quine es equiconsistente con la teoría de conjuntos de Mac Lane.
2: ¿Tenemos teoremas de integridad y solidez para Lambda/Lógica Combinatoria?
El documento que introdujo la semántica de Henkin para la lógica de orden superior trató explícitamente la teoría de tipos simples y contenía el teorema de Henkin. Entonces, la integridad y la solidez son similares a la lógica de primer orden en cierto sentido. Sin embargo, ser equiconsistente con la teoría de conjuntos de Mac Lane significa que la consistencia de la teoría de tipo simple no se puede probar en un sentido absoluto.
El artículo en realidad dice que "típicamente" exceden el poder de la lógica de primer orden. La lógica de primer orden sobre un lenguaje de aritmética que incluye la suma y la multiplicación es Turing completa, ya que puede definir aritméticamente cada función recursiva:
Sin embargo, otra forma de comparar el cálculo lambda sin tipo y la lógica de primer orden es considerar lo que puede construir con funciones de primer orden frente a funciones de orden superior frente a funciones en cálculo lambda sin tipo que son esencialmente de orden infinito.
No quiero dar ninguna ofensa aquí. Solo puedo comentar como un laico que solo tiene una comprensión laica de las matemáticas universitarias.
Cabe señalar que no todos aquí creen que la lógica de primer orden no es Turing completa. Una máquina de Turing es una máquina de estados finitos con una cinta infinita. Es solo un ejercicio de codificación de computadora elemental (es decir, factible) para implementar esto.
Solo se requiere un pequeño subconjunto de Dartmouth Basic o Applesoft Basic para un sistema completo de Turing. En los últimos años, Terry Tao preguntó (posiblemente en este sitio) si había un grupo que estaba completo. Tal vez podríamos realizar un ejercicio de marcar casillas, observando que cualquiera de los objetos que encontramos en el curso de introducción a las matemáticas en la universidad, es suficiente por sí solo para construir un sistema completo de Turing.
La entrada de wikipedia para la lógica de primer orden es bastante detallada (muchos cientos de líneas).
Dice: La lógica de primer orden es capaz de formalizar muchas construcciones simples de cuantificadores en lenguaje natural, como "todas las personas que viven en Perth viven en Australia". Pero hay muchas características más complicadas del lenguaje natural que no se pueden expresar en la lógica de primer orden (clasificación única). "Cualquier sistema lógico que sea apropiado como instrumento para el análisis del lenguaje natural necesita una estructura mucho más rica que la lógica de predicados de primer orden" (Gamut 1991, p. 75).
El artículo de wikipedia también dice:
Las interpretaciones ordinarias de primer orden tienen un solo dominio de discurso sobre el cual se extienden todos los cuantificadores. La lógica de primer orden de orden múltiple permite que las variables tengan diferentes tipos, que tienen diferentes dominios. ... Cuando solo hay un número finito de clases en una teoría, la lógica de primer orden de muchas clasificaciones se puede reducir a una lógica de primer orden de una sola clasificación. Uno introduce en la teoría de clasificación única un símbolo de predicado unario para cada clasificación en la teoría de clasificación múltiple, y agrega un axioma que dice que estos predicados unarios dividen el dominio del discurso.
De lo anterior, estoy lejos de estar convencido de que la lógica de primer orden no sea adecuada para un tratamiento completo del lenguaje natural. Si seguimos la doctrina de Turing, ¿no estamos obligados a aceptar que podemos codificar un tratamiento completo del lenguaje natural utilizando cualquier sistema completo de Turing que, supongo por el artículo de wikipedia, ciertamente incluye lógica de primer orden?
Seguiré el artículo de Gamut en un intento de arrojar luz sobre esto. Pero prima facie, el artículo de Gamut es incorrecto porque plantea la pregunta: dice que no se puede expresar el lenguaje natural en el cálculo de predicados de clasificación única. Pero el artículo de Wikipedia deja en claro que esto puede no ser una limitación, al menos muestra que un cálculo de predicados de clasificación múltiple se puede codificar en un cálculo de predicados de clasificación única.
duende se fue
Pruebas