cálculo de demostración

En lógica matemática , un cálculo de demostración o un sistema de demostración se construye para probar enunciados .

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

• Lenguaje formal : El conjunto L de fórmulas admitidas por el sistema, por ejemplo, lógica proposicional o lógica de primer orden .
• Reglas de inferencia : Lista de reglas que se pueden emplear para demostrar teoremas a partir de axiomas y teoremas.
• Axiomas : Se asume que las fórmulas en L son válidas. Todos los teoremas se derivan de los 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 abarca más de un sistema formal particular, ya que muchos cálculos de demostración están subdeterminados y pueden utilizarse para lógicas radicalmente diferentes. Por ejemplo, un caso paradigmático es el cálculo de secuentes , que puede utilizarse para expresar las relaciones de consecuencia tanto de la lógica intuicionista como de la lógica de relevancia . Así pues, en términos generales, un cálculo de demostración es una plantilla o patrón de diseño , caracterizado por un estilo determinado de inferencia formal, que puede especializarse para producir sistemas formales específicos, concretamente especificando las reglas de inferencia reales para dicho sistema. No existe consenso entre los lógicos sobre 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 demostración estructural , y que es la piedra angular de la correspondencia fórmulas-como-tipos que relaciona la lógica con la programación funcional ;
• El cálculo de secuencias de Gentzen , que es el formalismo más estudiado de la teoría de la demostración estructural.

Muchos otros cálculos de demostración fueron, o podrían haber sido, fundamentales, pero no se utilizan ampliamente en la actualidad.

• El cálculo silogístico de Aristóteles , presentado en el Organon , admite fácilmente la formalización. Todavía existe cierto interés moderno en los silogismos , que se desarrollan bajo el amparo de la lógica de términos .
• La notación bidimensional del Begriffsschrift de Gottlob Frege (1879) se considera generalmente como la que introdujo el concepto moderno de cuantificador en la lógica.
• El gráfico existencial de C.S. Peirce bien podría haber sido fundamental si la historia se hubiera desarrollado de otra manera.

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

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

• Método de cuadros analíticos
• Procedimiento de prueba
• Sistema de prueba proposicional
• Resolución (lógica)