¿Bajo qué condiciones un sistema de prueba axiomática tiene un equivalente de deducción natural?

Por "sistema axiomático", tengo en mente un sistema de prueba al estilo de Hilbert con axiomas y (típicamente pocas) reglas básicas de inferencia, donde cada teorema es demostrable a partir de los axiomas y estas pocas reglas. En aras de una fácil comparación, un sistema secuencial de estilo Gentzen donde cada teorema puede dar una prueba con solo líneas incondicionales (secuencias donde no ocurre nada a la izquierda del torniquete).

Por "sistema de deducción natural" me refiero a un sistema de prueba que se basa en reglas de introducción y eliminación, proporcionando un conjunto relativamente grande de inferencias. Por ejemplo, un cálculo secuencial de estilo Gentzen con algunas pruebas que necesariamente contienen líneas con un conjunto de premisas no vacío a la izquierda del torniquete.

Mi pregunta se refiere a los requisitos de equivalencia, en el sentido de probar los mismos teoremas. Estoy particularmente interesado en lo que se puede decir en algún nivel de generalidad, sin restringirlo a una lógica particular como la lógica proposicional o de primer orden. Lo que sé sobre algunos casos particulares:

  1. Lógica proposicional (clásica): para asegurar la equivalencia a un sistema de deducción natural con un → -regla intro, el teorema de la deducción debe cumplirse en el sistema axiomático.
  2. Lógica de primer orden (clásica): para asegurar la equivalencia a un sistema de deducción natural con un ∀ -regla intro, generalizacion universal debe cumplirse en el sistema axiomatico.

Pero, ¿puede decirse algo interesante y más general acerca de las condiciones para la equivalencia, que se extienda especialmente a otras lógicas (p. ej., lógica modal y lógica de orden superior) y teorías axiomáticas en matemáticas? (¿Especialmente aquellas teorías lógicas y matemáticas que están incompletas?) ¿Qué condiciones se requieren para asegurar que habrá un equivalente de deducción natural para un sistema de prueba axiomática (y viceversa )? ¿Existen propiedades de un sistema de deducción axiomático o natural que bloqueen definitivamente la equivalencia?

Respuestas (1)

Por "sistema de deducción natural" me refiero a un sistema de prueba que se basa en reglas de introducción y eliminación, proporcionando un conjunto relativamente grande de inferencias. Por ejemplo, un cálculo secuencial de estilo Gentzen con algunas pruebas que necesariamente contienen líneas con un conjunto de premisas no vacío a la izquierda del torniquete.

Primero, la razón por la que los sistemas de deducción natural tienen más reglas es porque usan más conectivos lógicos... podrías hacer un sistema axiomático para más conectivos también, y tendría más axiomas. De hecho, la forma más natural de crear un sistema axiomático con reglas para todos los conectores habituales es hacer que esas reglas sean condicionales de las reglas típicas de Elim e Intro, por ejemplo, podría tener un axioma ( PAG → q ) → ( ( q → PAG ) → ( PAG ↔ q ) ) como la condicionalización axiomática de un típico ↔ Regla de introducción, mientras que algo como ( PAG ↔ q ) → ( PAG → q ) sería un buen candidato para axiomatizar la ↔ Elim regla de inferencia.

Señalo esto porque en el párrafo anterior pareces establecer una conexión entre el número de reglas y el hecho de que un sistema de deducción natural utiliza supuestos... pero no están relacionados, ya que uno puede hacer un sistema axiomático con esas mismas reglas. (pero condicionalidades de los mismos). Entonces, la diferencia central entre los sistemas axiomáticos y los sistemas de deducción natural es, de hecho, el hecho de que puede hacer suposiciones (es decir, comenzar 'subpruebas') o, como usted dice, un sistema secuencial con conjuntos de apoyo no vacíos.

Sin embargo, esta posible conexión entre las reglas y los axiomas también se puede utilizar para abordar su pregunta: al menos parecería que mientras condiciona las reglas Elim e Intro de la manera que sugerí anteriormente, puede asegurarse de que el sistema axiomático puede hacer todo lo que puede hacer un sistema de deducción natural. Y para ir al revés... bueno, si los axiomas en el sistema axiomático son de hecho las versiones condicionadas de las reglas Intro y Elim de un sistema de deducción natural, entonces el Teorema de Deducción parecería ser suficiente.

Por supuesto, si no existe tal conexión sistemática entre los axiomas y las reglas de inferencia, entonces todas las apuestas están canceladas, y tendrías que probar la equivalencia entre los diferentes sistemas sobre una base más ad hoc,... en otras palabras, yo no podría decirle ningún 'requisito general para la equivalencia' ... aparte de poder demostrar que ambos sistemas están completos por sí mismos, por supuesto.

Lo siento, no quise sugerir que "más reglas" fuera la característica definitoria de los sistemas ND, solo una característica típica. Supongo que los "requisitos más generales" que tenía en mente eran algo así como lo que obtienes de la correspondencia Curry-Howard (-Lambek), donde el teorema de deducción corresponde a la eliminación de abstracción en lógica combinatoria tipificada y → -intro corresponde a la función de abstracción en el cálculo lambda....
... Parece entonces que un requisito para la equivalencia de Hilbert<->ND<->Sequent es que el teorema de deducción se cumpla para el sistema de Hilbert, cada derivación de ND sea reducible a la forma normal, y el cálculo de secuentes debe admitir la eliminación por corte. ¿Esto parece correcto? Si eso es correcto, entonces, ¿el "requisito general" (al menos una condición necesaria) que busco (aunque, es cierto, solo en el mejor de los casos es torpe) es una coincidencia en este tipo de reglas estructurales/propiedades de normalización?
@Dennis Hmm, gran parte de lo que dices aquí en realidad me pasa por alto, ¡lo siento! Con suerte, algunos lógicos más expertos pueden ayudarlo ...
¡bueno, gracias! Debería agregar esto a la pregunta. Fue solo para tratar de aclarar lo que significaba para ti que pensé en preguntar sobre estas conexiones. ¡Así que tu respuesta ha sido de gran ayuda!
@Dennis ¡Ah, está bien! Supongo que a veces solo necesitas una caja de resonancia. Me alegro de ser de servicio, ja, ja! :) Pero sí, edite su publicación y, con suerte, logrará que otras personas respondan.
¿Bajo qué condiciones un sistema de prueba axiomática tiene un equivalente de deducción natural?
RespuestasAquíPolítica de privacidad1y, 0v