Prueba formal - Formal proof

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 sigue de las oraciones precedentes en la secuencia. por una regla de inferencia . Se diferencia de un argumento de lenguaje natural en que es riguroso, inequívoco y verificable mecánicamente. 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 por el cual siempre podamos encontrar una prueba de una oración dada o determinar que no existe ninguna. Los conceptos de prueba al estilo de Fitch , cálculo secuencial y deducción natural son generalizaciones del concepto de prueba.

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 comprobador de teoremas automatizado ). 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 automatizada de teoremas ) suele ser computacionalmente intratable y / o solo semidecidible , dependiendo del sistema formal en uso.

Fondo

Lenguaje formal

Un lenguaje formal es un conjunto de secuencias finitas de símbolos . Tal lenguaje puede definirse sin 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.

Gramática formal

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

Sistemas formales

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. Se utiliza un sistema formal para derivar una expresión de una o más expresiones.

Interpretaciones

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 .

Ver también

Referencias

enlaces externos