Cálculo de demostración

En lógica matemática , un cálculo de prueba o un sistema de prueba se construye para probar afirmaciones .

Un sistema de prueba incluye los componentes: ^{[1] [2]}

• Lenguaje formal : El conjunto L de fórmulas admitidas por el sistema, por ejemplo, la lógica proposicional o la lógica de primer orden .
• Reglas de inferencia : Lista de reglas que pueden emplearse para demostrar teoremas a partir de axiomas y teoremas.
• Axiomas : Fórmulas que se consideran válidas en L. Todos los teoremas se derivan de axiomas.

Una prueba formal de una fórmula bien formada en un sistema de prueba es un conjunto de axiomas y reglas de inferencia del sistema de prueba que infiere que la fórmula bien formada es un teorema del sistema de prueba. ^[2]

Por lo general, un cálculo de demostración dado abarca más de un sistema formal particular, ya que muchos cálculos de demostración están subdeterminados y pueden usarse para lógicas radicalmente diferentes. Por ejemplo, un caso paradigmático es el cálculo consecuente , que puede usarse para expresar las relaciones de consecuencia tanto de la lógica intuicionista como de la lógica de relevancia . Por lo tanto, en términos generales, un cálculo de demostración es una plantilla o patrón de diseño , caracterizado por un cierto estilo de inferencia formal, que puede especializarse para producir sistemas formales específicos, es decir, especificando las reglas de inferencia reales para tal sistema. No hay consenso entre los lógicos sobre cuál es la mejor manera de definir el término.

Los cálculos de demostración más conocidos son aquellos cálculos clásicos que todavía se utilizan ampliamente:

• La clase de sistemas de Hilbert , ^[2] cuyo ejemplo más famoso es el sistema de lógica de primer orden de Hilbert-Ackermann de 1928 ;
• El cálculo de deducción natural de Gerhard Gentzen , que es el primer formalismo de la teoría de la prueba estructural y que es la piedra angular de la correspondencia de fórmulas como tipos que relaciona la lógica con la programación funcional ;
• Cálculo secuencial de Gentzen , que es el formalismo más estudiado de la teoría de la prueba estructural.

Muchos otros cálculos de prueba fueron, o podrían haber sido, fundamentales, pero hoy en día no se utilizan ampliamente.

• El cálculo silogístico de Aristóteles , presentado en el Organon , admite sin problemas la formalización. Aún hoy existe cierto interés por los silogismos, realizados bajo la égida de la lógica de términos .
• La notación bidimensional del Begriffsschrift (1879) de Gottlob Frege suele considerarse la introducción del concepto moderno de cuantificador a la lógica.
• El gráfico existencial de C. S. Peirce fácilmente podría haber sido fundamental si la historia hubiera funcionado de manera diferente.

La investigación moderna en lógica está repleta de cálculos de prueba rivales:

• Se han propuesto varios sistemas que reemplazan la sintaxis textual habitual con alguna sintaxis gráfica. Las redes de prueba y el cálculo circunferencial se encuentran entre dichos sistemas.
• Recientemente, muchos lógicos interesados ​​en la teoría de la prueba estructural han propuesto cálculos con inferencia profunda , por ejemplo , la lógica de visualización , las hipersecuentes , el cálculo de estructuras y la implicación agrupada .

• Sistema de prueba proposicional
• Redes de prueba
• Cálculo circular
• Cálculo de estructuras
• Prueba formal
• Método de cuadros analíticos
• Resolución (lógica)