En lógica matemática , se construye un cálculo de prueba o un sistema de prueba para probar declaraciones.
Descripción general
Un sistema de prueba incluye los componentes: [1]
- Lenguaje: Conjunto 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.
Por lo general, un cálculo de prueba dado abarca más de un sistema formal particular, ya que muchos cálculos de prueba están subdeterminados y pueden usarse para lógicas radicalmente diferentes. Por ejemplo, un caso paradigmático es el cálculo secuencial , que se puede utilizar para expresar las relaciones consecuencia tanto de la lógica intuicionista y lógica relevante . 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 estar especializado 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 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 , cuyo ejemplo más famoso es el sistema de Hilbert-Ackermann de lógica de primer orden de 1928 ;
- El cálculo de la 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, seminales, pero no se usan ampliamente en la actualidad.
- El cálculo silogístico de Aristóteles , presentado en el Organon , admite fácilmente la formalización. Todavía hay cierto interés moderno en la silogística, realizada bajo la égida de la lógica del término .
- Se suele considerar que la notación bidimensional de Gottlob Frege de la 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 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. 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 , las hipersecuentes , el cálculo de estructuras y la implicación agrupada .
Ver también
- Sistema de prueba de proposiciones
- Redes de prueba
- Cálculo circulante
- Cálculo de estructuras
- Prueba formal
- Método de cuadros analíticos
- Resolución (lógica)
Referencias
- ^ Anita Wasilewska. "Sistemas de pruebas generales" (PDF) .