En lógica y matemáticas , una prueba formal o derivación es una secuencia finita de oraciones (conocidas como fórmulas bien formadas cuando se relacionan con el lenguaje formal ), cada una de las cuales es un axioma , una suposición, o se sigue de las oraciones anteriores en la secuencia, de acuerdo con la regla de inferencia . Se diferencia de un argumento en lenguaje natural en que es riguroso, inequívoco y verificable mecánicamente. [1] Si el conjunto de suposiciones está vacío, entonces la última oración en una prueba formal se llama teorema del sistema formal . La noción de teorema es generalmente efectiva , pero puede que no haya un método por el cual podamos encontrar de manera confiable una prueba de una oración dada o determinar que no existe ninguna. Los conceptos de prueba de estilo Fitch , cálculo secuencial y deducción natural son generalizaciones del concepto de prueba. [2] [3]
El teorema es una consecuencia sintáctica de todas las fórmulas bien formadas que lo preceden en la demostración. Para que una fórmula bien formada sea considerada parte de una demostración, debe ser el resultado de aplicar una regla del aparato deductivo (de algún sistema formal) a las fórmulas bien formadas anteriores en la secuencia de demostración.
Las pruebas formales se construyen a menudo con la ayuda de computadoras en la demostración interactiva de teoremas (por ejemplo, mediante el uso de un verificador de pruebas y un demostrador automático de teoremas ). [4] Significativamente, estas pruebas se pueden verificar automáticamente, también por computadora. La verificación de pruebas formales suele ser simple, mientras que el problema de encontrar pruebas (demostración automática de teoremas) suele ser computacionalmente intratable y/o solo semidecidible , dependiendo del sistema formal en uso.
Un lenguaje formal es un conjunto de secuencias finitas de símbolos . Un lenguaje de este tipo puede definirse sin referencia a ningún significado de ninguna de sus expresiones; puede existir antes de que se le asigne ninguna interpretación , es decir, antes de que tenga algún significado. En algunos lenguajes formales se expresan pruebas formales.
Una gramática formal (también llamada reglas de formación ) es una descripción precisa de las fórmulas bien formadas de un lenguaje formal. Es sinónimo del conjunto de cadenas sobre el alfabeto del lenguaje formal que constituyen las fórmulas bien formadas. Sin embargo, no describe su semántica (es decir, lo que significan).
Un sistema formal (también llamado cálculo lógico o sistema lógico ) consiste en un lenguaje formal junto con un aparato deductivo (también llamado sistema deductivo ). El aparato deductivo puede consistir en un conjunto de reglas de transformación (también llamadas reglas de inferencia ) o un conjunto de axiomas , o tener ambos. Un sistema formal se utiliza para derivar una expresión a partir de una o más expresiones diferentes.
La interpretación de un sistema formal es la asignación de significados a los símbolos y valores de verdad a las oraciones de un sistema formal. El estudio de las interpretaciones se denomina semántica formal . Dar una interpretación es sinónimo de construir un modelo .