¿Por qué necesitamos una semántica formal para la lógica de predicados?

Considere esta pregunta resuelta. No elegiré la mejor respuesta ya que todas ellas han contribuido a mi comprensión del tema.

No estoy seguro de qué beneficio tenemos al definir formalmente la semántica de la lógica de predicados. Pero sí valoro tener un cálculo de prueba formal. Mi punto es que no necesitaríamos una semántica formal para justificar las reglas de inferencia de los cálculos de prueba.

Podríamos definir un cálculo que imite las "leyes del pensamiento", es decir, las reglas de inferencia que los matemáticos han usado durante cientos de años para probar sus teoremas. Tal cálculo ya existe: deducción natural. Luego definiríamos este cálculo como sólido y completo.

Esto puede justificarse al darse cuenta de que la semántica formal de la lógica de predicados es solo un modelo. La idoneidad del modelo solo puede justificarse intuitivamente. Por lo tanto, mostrar que la deducción natural es sólida y completa con referencia a la semántica formal no hace que la deducción natural sea más "verdadera". Sería tan bueno si justificamos directamente las reglas de la deducción natural de forma intuitiva. El desvío usando semántica formal no nos da nada.

Luego, habiendo definido que la deducción natural es sólida y completa, podríamos mostrar la solidez y la integridad de otros cálculos al mostrar que las pruebas que producen pueden traducirse a deducción natural y viceversa.

¿Son correctas mis reflexiones anteriores? ¿Por qué es importante demostrar la solidez y la integridad de los cálculos de prueba por referencia a la semántica formal?

Un comentario menor y una respuesta más seria.

Primero, no tiene sentido declarar un sistema de deducción natural completo por fiat. La deducción natural es interesante precisamente porque tiene una noción interna natural de consistencia y / o integridad, es decir, eliminación de cortes. Este es un teorema fantástico, y la OMI justifica por completo los intentos de proporcionar una semántica puramente teórica a prueba (y por la correspondencia CH, también justifica el uso de métodos operativos en la semántica del lenguaje de programación). Pero esto es interesante precisamente porque ofrece una noción más refinada de lograr la lógica correcta que la consistencia. Tomar el camino teórico de la prueba significa que tendrá que hacer más trabajo, pero a cambio obtendrá mejores resultados.

Sin embargo, sucede que a veces la lógica per setoma un papel secundario Podemos comenzar con una (familia de) modelos, y luego buscar formas de hablar sintácticamente sobre ellos, usando una lógica. La solidez y la integridad de una lógica con respecto a una familia de modelos indica que la lógica realmente captura todo lo interesante y verdadero que puede decir sobre la clase de modelos. Un ejemplo concreto de cuándo los modelos son más interesantes que las teorías lógicas ocurre en el análisis de programas y la verificación de modelos. Ahí, lo habitual es considerar que su modelo es la ejecución de un programa y que la lógica es un fragmento de lógica temporal. Las proposiciones que puede decir en estos lenguajes no son (deliberadamente) terriblemente emocionantes, por ejemplo, las desreferencias de puntero nulo nunca ocurren, pero es el hecho de que se aplica a ejecuciones de programas reales lo que le da interés.

Solo agregaré otra perspectiva para aumentar las respuestas anteriores. Primero, estas reflexiones valen la pena, y muchas personas han tenido ideas similares. En filosofía, esto a veces se llama "semántica de la teoría de la prueba", que apela al trabajo de Nuel Belnap, Dag Prawitz, Michael Dummett y otros en los años 60 y 70, quienes a su vez recurren al trabajo de Gentzen sobre la deducción natural. Per Martin-Löf y Jean-Yves Girard también parecen proponer variantes de esta posición en sus escritos. Y hablando de manera muy amplia, en lenguajes de programación este es el "enfoque sintáctico para la solidez de los tipos".

La cuestión es que, incluso si acepta que las reglas de la lógica no necesitan una interpretación semántica separada, no es muy interesante / útil decir que están justificadas por sí mismas y dejarlo así. La pregunta es qué logra una semántica formal y si es posible lograr lo mismo con menos desvíos. Sin embargo, el proyecto de unificar la teoría del modelo con la teoría de la prueba analítica es importante, pero aún no se ha resuelto, y se persigue activamente a lo largo de muchos frentes diferentes, incluida la lógica categórica, la semántica del juego y las "lúdicas" de Girard. Por ejemplo, además de lo que Charles mencionó, otro beneficio cualitativo de tener modelos es la capacidad de proporcionar contraejemplos a no-teoremas, y la pregunta es cómo darle sentido a esto en un enfoque "directo". Para una respuesta inspirada en los lúdicos, vea"Sobre el significado de la integridad lógica" de Michele Basaldella y Kazushige Terui.

Una semántica formal proporciona un significado directo de los términos en el cálculo independientemente de las reglas de prueba sintácticas para manipularlos. Sin una semántica formal, ¿cómo puede establecer si las reglas de deducción son correctas (solidez) o si tiene suficientes (integridad)?

Se han propuesto "leyes del pensamiento" antes de que ocurriera la deducción natural. Los silogismos de Aristóteles fueron una de esas colecciones. Si los hubiéramos definido como sólidos y completos, tal vez aún los estaríamos usando hoy, en lugar de desarrollar técnicas lógicas más avanzadas. El punto es que, si los silogismos capturan completamente las leyes del pensamiento, ¿por qué necesitaríamos idear más lógicas? ¿Qué pasaría si de hecho fueran inconsistentes? Tener una semántica junto con el cálculo de prueba formal y las pruebas de solidez e integridad que los conectan proporciona una medida para juzgar el valor de dicho sistema de razonamiento. Ya no se mantendría aislado.

$X\lor \neg X$incluso ir tan lejos como para argumentar que debemos aceptar que no hay una lógica verdadera y adoptar una actitud pluralista, utilizando la lógica más apropiada para la ocasión. Dada la gran cantidad de lógicas disponibles para los informáticos (lógica lineal, lógica de separación, lógica constructiva de orden superior, muchas lógicas modales, todas en variedades clásicas e intuitivas), adoptar una actitud pluralista es algo que la mayoría de nosotros probablemente no hemos dado ni un segundo pensó, porque las lógicas son una herramienta para resolver un problema en particular y tratamos de seleccionar el más apropiado. Una semántica formal es una forma de juzgar la adecuación de la lógica.

Otra razón para tener una semántica formal es que hay más lógicas que el cálculo de predicados. Muchas de estas lógicas están diseñadas para razonar sobre un tipo particular de sistema. (Estoy pensando en la lógica modal). Aquí se conoce la clase de sistemas y la lógica viene después (aunque, históricamente, esto tampoco es cierto). Nuevamente, la solidez nos dice si los axiomas de la lógica capturan correctamente el "comportamiento" del sistema, y ​​la integridad nos dice si tenemos suficientes axiomas. Sin una semántica, ¿cómo sabríamos si las reglas de deducción son suficientes y no tienen sentido?

Un ejemplo de lógica que se definió de manera puramente sintáctica y todavía se está trabajando para proporcionarle una semántica formal es la lógica BAN para razonar sobre protocolos criptográficos. Las reglas de inferencia lógica parecen razonables, entonces, ¿por qué proporcionar una semántica formal? Desafortunadamente, la lógica BAN se puede utilizar para demostrar que un protocolo es correcto, aunque pueden existir ataques a dichos protocolos. Por lo tanto , las reglas de deducción son incorrectas , al menos con respecto a la semántica esperada.

Estoy de acuerdo con supercooldave, pero hay otra razón más pragmática para querer más que un conjunto u otro de reglas de inferencia que caracterizan una lógica: un conjunto dado de reglas de inferencia no suele ser bueno para responder al tipo de problemas que se enfrentan al poner la lógica usar.

Si tiene una lógica especificada por una lista de axiomas y un par de reglas como un sistema de Hilbert, por lo general será difícil trabajar cómo demostrar un teorema dado en el sistema, y ​​sin una visión teórica, no va a para poder probar que una proposición dada no puede ser probada en el sistema. Los modelos tradicionales son buenos para probar propiedades que se mantienen para toda la lógica por inducción.

Cuatro tipos de herramientas son útiles para resolver problemas que la mayoría de los lógicos quieren resolver, organizados de menor a mayor semántica:

1. Los sistemas de estilo Hilbert son buenos para caracterizar la relación de consecuencia lógica de una lógica, y generalmente son buenos para categorizar varias lógicas, como las lógicas modales rivales;
2. Los sistemas de Tableau son buenos para formalizar algoritmos de decisión. Por lo general, si una lógica es decidible, se puede encontrar un sistema de cuadro final como algoritmo de decisión, y si no se puede encontrar un sistema de cuadro potencialmente no final que proporcione un procedimiento de semi-decisión. Si se quiere mostrar un límite superior en la complejidad de la capacidad de decisión (es decir, la clase de complejidad de una lógica), los sistemas de cuadro generalmente son el primer lugar en el que uno mira.
3. Las teorías de pruebas analíticas, como la deducción natural de Gentzen y el cálculo posterior, dan representaciones de pruebas que son buenas para el razonamiento y ofrecen la noción de prueba analítica, que es útil para probar propiedades útiles como la interpolación de una teoría.
4. Las teorías del modelo de estilo Tarski a menudo son aún mejores para razonar sobre la lógica, porque se abstraen casi por completo de los detalles sintácticos de la lógica. En la lógica modal y la teoría de conjuntos, son mucho mejores en la entrega de los resultados que esos lógicos tienden a tener un interés muy limitado en la teoría del cuadro y la prueba analítica.

Como supercoolda ha mencionado la lógica intuicionista: sin la regla del medio excluido, la teoría del modelo se vuelve mucho más complicada, y las teorías de prueba analíticas se vuelven más importantes, típicamente la semántica de elección. Las técnicas algebraicas, como la teoría de categorías, se vuelven preferidas para abstraerse de la complejidad sintáctica.