Prueba formal
En lógica, una derivación formal (o prueba formal) es una secuencia finita de sentencias donde cada sentencia puede ser un axioma o puede ser obtenida como consecuencia directa de las sentencias anteriores en la secuencia utilizándose una regla de inferencia. La última frase siguiente es un teorema del sistema formal. La noción del teorema no es efectiva en general, porque no puede haber un método mediante el cual siempre podemos encontrar una derivación de una resolución dictada o determinar que no hay derivación. El concepto de deducción es una generalización del concepto de derivación.
El teorema es una consecuencia sintáctica de todas las fórmulas bien formadas (fbf) precedidas en la derivación. Para una parte fbf de una unión, ella debe ser el resultado de aplicar una regla de sistema deductivo de cualquier sistema formal previa en fbfs siguiente derivación.
Las derivaciones formales muchas veces se construye con la ayuda de ordenadores a través de la demostración interactiva de teoremas. Resulta interesante notar que estas derivaciones pueden ser conferidas automáticamente con el uso del ordenador. Conferir derivaciones formales suele ser una tarea trivial, mientras que encontrar tales derivaciones (demostración automática de teoremas) suele ser bastante difícil.
Un lenguaje formal es un conjunto de elementos (símbolos) es un conjunto de métodos (reglas) para la combinación de estos elementos. Las derivaciones formales se expresan en un lenguaje formal.
Una gramática formal es una descripción exacta de un fbf de un lenguaje formal. Puede ser considerada como un conjunto de cadenas sobre el alfabeto que constituyen las fbfs Sin embargo, no describe su semántica.
Un sistema formal consiste en un lenguaje formal junto con un sistema deductivo. El sistema deductivo puede estar constituido de conjuntos de reglas de inferencia, un conjunto de axiomas o ambos. Un sistema formal es utilizado para derivar una expresión de uno o varias expresiones.
Una interpretación de un sistema formal es una atribución de significados a los símbolos y valores de verdad de las oraciones de un semántica formal. El estudio de las interpretaciones formales se llama semántica formal. Dar una interpretación es sinónimo de construir un modelo.
Podemos utilizar la derivación formal de los distintos tipos de enfoque.
En la deducción natural, una derivación puede ser representada como un árbol. La raíz del árbol es la conclusión, los hijos son las raíces de las derivaciones que generan cada conclusión. El sistema natural presenta reglas de deducción que combinan árboles (finitas) que son generadas a partir de un conjunto finito de supuestos y ciertas suposiciones hasta derivar una conclusión.
Las hojas del árbol representan hipótesis o premisas. Las hojas de cálculo representan premisas, mientras que las cerradas representan hipótesis que son consumidas a lo largo de la derivación. Todas las hojas deben poseer marcas y se deben evitar el conflicto de marcas, es decir, tener dos fórmulas diferentes con la misma marca. La marca, generalmente, es un número natural, identificando las hojas.
Cada paso, o sea, cada derivación, en el árbol, deben basarse en un sistema de reglas.
En el método de tableaux, la derivación se realiza como prueba por reducción al absurdo. Comenzamos con la negación de la sentencia que deseamos demostrar y a partir de esa suposición derivamos una consecuencia imposible, entonces podemos concluir que la hipótesis original es imposible. Si la prueba no fue bien sucedida, y no se vislumbra ninguna consecuencia imposible, entonces en algunos casos se puede concluir que no hay error con la hipótesis abierta, es decir, la hipótesis puede ser cierta para cualquier interpretación. A veces todo lo que podemos decir sobre la derivación es que no llegamos a ninguna consecuencia imposible y que no sabemos si esto ocurrirá en caso de que continuemos con la prueba.
(Ver: Method of analytic tableaux (en inglés))
(Ver: Sequent (en inglés))
El matemático David Hilbert junto con Wilhelm Ackermann desarrollaron la teoría formal T el que usa como conectivos primitivos, en su derivación, los conectivos lógicos y . La derivación en la axiomática de Hilbert consiste en planes de axiomas y una única regla de inferencia, el modus ponendo ponens.
(Ver: Hilbert Systems (en inglés))