Derivação formal

Em lógica, uma derivação formal (ou prova formal) é uma sequência finita de sentenças onde cada sentença pode ser um axioma ou então pode ser obtida como consequência direta de sentenças anteriores na sequência utilizando-se uma regra de inferência. A última sentença na sequência é um teorema do sistema formal. A noção de teorema não é em geral efetiva, pois pode não haver um método através do qual nós possamos sempre encontrar uma derivação de uma dada sentença ou determinar que não existe nenhuma derivação. O conceito de dedução é uma generalização do conceito de derivação.

O teorema é uma consequência sintática de todas as fórmulas bem formadas (fbf) precedidas na derivação. Para uma fbf fazer parte de uma derivação, ela deve ser resultado da aplicação de uma regra do sistema dedutivo de algum sistema formal nas fbfs anteriores na sequência da derivação.

As derivações formais muitas vezes são construídas com a ajuda de computadores através da demonstração interativa de teoremas. É interessante notar que tais derivações podem ser conferidas automaticamente com o uso do computador. Conferir derivações formais normalmente é uma tarefa trivial, enquanto que encontrar tais derivações (demonstração automática de teoremas) geralmente é bastante difícil.

Background

Linguagem formal

Artigo principal: Linguagem formal

Uma linguagem formal é um conjunto de elementos (símbolos) e um conjunto de métodos (regras) para combinar estes elementos. Derivações formais são expressos em algumas linguagens formais.

Gramática formal

Artigo principal: Gramática formal

Uma gramática formal é uma descrição precisa de uma fbf de uma linguagem formal. Ela pode ser considerada como um conjunto de strings ao longo do alfabeto da linguagem formal que constituem as fbfs. No entanto, ela não descreve sua semântica.

Sistema formal

Artigo principal: Sistema formal

Um sistema formal consiste de uma linguagem formal junto com um sistema dedutivo. O sistema dedutivo pode ser constituído de conjuntos de regras de inferência, um conjunto de axiomas ou ambas. Um sistema formal é usado para derivar uma expressão de uma ou mais outras expressões.

Interpretação formal

Artigo principal: Semântica formal

Uma interpretação de um sistema formal é uma atribuição de significados para os símbolos e valores de verdade para sentenças de um sistema formal. O estudo das interpretações formais é chamado semântica formal. Dar uma interpretação é sinônimo de construir um modelo.

Formalismos que envolvem derivações formais

Podemos utilizar a derivação formal em vários tipos de abordagem.

Dedução Natural

Na dedução natural, uma derivação pode ser representada em forma de árvore. A raiz da árvore é a conclusão, os filhos são as raízes das derivações que geram cada conclusão. O sistema de dedução natural apresenta regras que combinam árvores (finitas) que são geradas a partir de um conjunto finito de premissas e hipóteses até derivar uma certa conclusão.

As folhas da árvore representam hipóteses ou premissas. As folhas abertas representam premissas, enquanto as fechadas representam hipóteses que são consumidas ao longo da derivação. Todas as folhas devem possuir marcas e deve-se evitar o conflito de marcas, ou seja, ter duas fórmulas diferentes com uma mesma marca. A marca, geralmente, é um número natural, identificando as folhas.

Cada passo, ou seja, cada derivação realizada, na árvore, deve ser baseada em uma das regras do sistema.

Método de tableaux

No método de tableaux, a derivação é feita como uma prova por redução ao absurdo. Começamos com a negação da sentença que desejamos demonstrar e se a partir dessa hipótese derivamos uma consequência impossível, então podemos concluir que a hipótese original é impossível. Se a prova não foi bem sucedida, e nenhuma consequência impossível é vislumbrada, então em alguns casos podemos concluir que não existe erro com a hipótese aberta, isto é, a hipótese pode ser verdadeira para alguma interpretação. Algumas vezes tudo o que podemos dizer sobre a derivação é que ainda não chegamos a nenhuma consequência impossível e que não sabemos se isto irá acontecer caso continuemos a prova.

(Ver Method of analytic tableaux (em inglês))

Cálculo de sequentes de Gentzen

(Ver: Sequent (em inglês))

Formalismo axiomático de Hilbert

O matemático David Hilbert junto com Wilhelm Ackermann desenvolveram a teoria formal T $_{P}v$ a qual usa como conectivos primitivos, em sua derivação, os conectivos lógicos $\lor$ e $\lnot$ . A derivação na axiomática de Hilbert consiste de esquemas de axiomas e uma única regra de inferência, o modus ponens.

(Ver: Hilbert systems (em inglês))

Ver também

Bibliografia

Bedregal, Benjamín René Callejas, e Acióly, Benedito Melo (2002), Lógica para a Ciência da Computação, Versão Preliminar, Natal, RN.
F. Miguel Dionísio, Paula Gouveia, João Marcos. Lógica Computacional. Versão preliminar, 2006.