En lógica y matemáticas , una prueba o derivación formal es una secuencia finita de oraciones (llamadas fórmulas bien formadas en el caso de un lenguaje formal ), cada una de las cuales es un axioma , una suposición, o se deriva de las oraciones anteriores en la secuencia. por una regla de inferencia . Se diferencia de un argumento en lenguaje natural en que es riguroso, inequívoco y mecánicamente verificable. [1] Si el conjunto de supuestos está vacío, entonces la última oración de una demostración formal se llama teorema del sistema formal . La noción de teorema no es en general efectiva , por lo tanto, puede que no exista un método mediante el cual siempre podamos encontrar una prueba de una oración determinada o determinar que no existe ninguna. Los conceptos de prueba estilo Fitch , cálculo secuente 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 califique como parte de una prueba, 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 prueba.
Las demostraciones formales a menudo se construyen 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 de teoremas automatizado ). [4] Cabe destacar que estas pruebas pueden comprobarse automáticamente, también por ordenador. Verificar pruebas formales suele ser sencillo, mientras que el problema de encontrar pruebas (demostración automática de teoremas) suele ser computacionalmente intratable y/o sólo semidecidible , dependiendo del sistema formal utilizado.
Un lenguaje formal es un conjunto de secuencias finitas de símbolos . Un lenguaje así puede definirse sin hacer referencia a ningún significado de cualquiera de sus expresiones; puede existir antes de que se le asigne cualquier interpretación , es decir, antes de que tenga algún significado. Las pruebas formales se expresan en algunos lenguajes 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 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 ) consta de 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. Se utiliza un sistema formal para derivar una expresión a partir de una o más expresiones.
Una 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 llama semántica formal . Dar una interpretación es sinónimo de construir un modelo .