Cálculo de prueba

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

Descripción general

Un sistema de prueba incluye los 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 supone que las fórmulas en L son válidas. 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 prueba determinado abarca más de un sistema formal particular, ya que muchos cálculos de prueba están infradeterminados y pueden usarse para lógicas radicalmente diferentes. Por ejemplo, un caso paradigmático es el cálculo secuente , que puede usarse para expresar las relaciones de consecuencia tanto de la lógica intuicionista como de la lógica de relevancia . Así, en términos generales, un cálculo de prueba 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, concretamente especificando las reglas de inferencia reales para dicho sistema. No hay consenso entre los lógicos sobre cuál es la mejor manera de definir el término.

Ejemplos de cálculos de prueba.

Los cálculos de prueba más conocidos son los 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 ;
• El 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 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, llevados a cabo bajo los auspicios de la lógica de términos .
• Generalmente se considera que la notación bidimensional de Gottlob Frege del Begriffsschrift (1879) introduce el concepto moderno de cuantificador en la lógica.
• El gráfico existencial de CS Peirce fácilmente 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 prueba rivales:

• Se han propuesto varios sistemas que reemplazan la sintaxis textual habitual con alguna sintaxis gráfica. Entre estos sistemas se encuentran las redes de prueba y el cálculo circular .
• 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 , los hipersecuentes , el cálculo de estructuras y la implicación agrupada .

Ver también

• 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)

Referencias

1. Anita Wasilewska. «Sistemas de prueba generales» (PDF) .
2. "Definición: Sistema de prueba - ProofWiki". pruebawiki.org . Consultado el 16 de octubre de 2023 .