La pregunta:
Supongamos que tengo una especificación de un problema que consiste en axiomas y una meta (es decir, el problema de prueba asociado es si la meta es satisfactoria dados todos los axiomas). Supongamos también que el problema no contiene inconsistencias / contradicciones entre los axiomas. ¿Hay alguna manera de determinar por adelantado (es decir, sin construir primero una prueba completa) que demostrar el problema requerirá un "razonamiento de orden superior"?
Por "razonamiento de orden superior", me refiero a aplicar pasos de prueba que requieren que se escriba la lógica de orden superior. Un ejemplo típico de "razonamiento de orden superior" sería la inducción: escribir un esquema de inducción en principio requiere el uso de una lógica de orden superior.
Ejemplo:
Se puede especificar el problema de la prueba "¿La suma de dos números naturales es conmutativa?" utilizando la lógica de primer orden (es decir, definir el número natural a través de constructores cero / succ junto con axiomas estándar, junto con axiomas que definen recursivamente una función "más"). Probar este problema requiere inducción en la estructura del primer o el segundo argumento de "más" (dependiendo de la definición exacta de "más"). ¿Podría haberlo sabido antes de intentar probarlo, por ejemplo, analizando la naturaleza del problema de entrada ...? (Por supuesto, este es solo un ejemplo simple con fines ilustrativos; en realidad, sería interesante para problemas de prueba más difíciles que la conmutatividad de más).
Un poco más de contexto:
En mi investigación, con frecuencia trato de aplicar demostradores automáticos de teoremas de primer orden como Vampire, eprover, etc. para resolver problemas de prueba (o partes de problemas de prueba), algunos de los cuales pueden requerir un razonamiento de orden superior. A menudo, los probadores requieren bastante tiempo para presentar una prueba (siempre que haya una prueba que solo requiera técnicas de razonamiento de primer orden). Por supuesto, tratar de aplicar un comprobador de teoremas de primer orden a un problema que requiere un razonamiento de orden superior generalmente resulta en un tiempo de espera.
Por lo tanto, me he estado preguntando si hay algún método / técnica que pueda decirme de antemano si un problema de prueba requerirá técnicas de razonamiento de orden superior (lo que significa "no pierdas el tiempo tratando de pasarlo a un probador de teoremas de primer orden" ) o no, al menos tal vez para problemas de entrada particulares.
Busqué en la literatura una respuesta a mi pregunta y pregunté a algunos colegas investigadores del área del teorema que lo demostraban, pero hasta ahora no recibí ninguna buena respuesta. Mi expectativa sería que haya algunas investigaciones sobre ese tema de personas que intentan combinar la prueba interactiva de teoremas y la prueba automática de teoremas (¿comunidad Coq? ¿Comunidad Isabelle (Sledgehammer)?), Pero hasta ahora, no pude encontrar nada.
Supongo que, en general, el problema que describí aquí es indecidible (¿verdad?). ¿Pero tal vez hay buenas respuestas para versiones refinadas del problema ...?
fuente
Respuestas:
Brevemente, cada teorema establecido en la lógica de primer orden tiene una prueba de primer orden.
En su libro "Una introducción a la lógica matemática y la teoría de tipos", Peter B. Andrews desarrolla tanto la lógica de primer orden como un sistema de lógica de orden superior Q 0 , que generalmente se considera la base teórica de los probadores modernos de orden superior. . (Consulte la introducción a la lógica HOL, por ejemplo).
Para Q 0 y sistemas similares, Andrews muestra que las lógicas de orden superior que describe pueden considerarse como extensiones conservadoras de la lógica de primer orden y escribe (segunda edición, p. 259) que, en resumen, cada teorema de primer orden de la teoría de tipos tiene una prueba de primer orden ".
Sin embargo, dadas sus preocupaciones prácticas, también cito el siguiente párrafo:
"Sin embargo, algunos teoremas de la lógica de primer orden pueden probarse de manera más eficiente mediante el uso de conceptos que pueden expresarse solo en la lógica de orden superior. Se pueden encontrar ejemplos en [Andrews y Bishop, 1996] y [Boolos, 1998, Capítulo 25] Statman demostró [Statman, 1978, Proposición 6.3.5] que la longitud mínima de una prueba en lógica de primer orden de un wff de lógica de primer orden puede ser extraordinariamente más larga que la longitud mínima de una prueba de la misma wff en lógica de segundo orden. Un resultado relacionado de Godel [Godel, 1936] es que, en general, 'pasar a la lógica del siguiente orden superior tiene el efecto, no solo de hacer ciertas proposiciones que antes no eran comprobables, sino también de hacer es posible acortar, en una cantidad extraordinaria, infinitamente muchas de las pruebas ya disponibles ". Una prueba completa de esto se puede encontrar en [Buss,1994] ".
fuente