Godel: Conceitos e formalismo de difícil compreensão

Demonstração[editar | editar código-fonte]

A demonstração original do Teorema da completude de Gödel utiliza conceitos e formalismo de difícil compreensão. A versão abaixo propõe uma abordagem moderna deste teorema, que se mantém, não obstante, fiel a todos os passos e idéias importantes originais. Este esboço não deve ser considerado uma demonstração rigorosa do teorema.

Definições e pressupostos[editar | editar código-fonte]

Estamos trabalhando com cálculo de predicados de primeira ordem, logo nossa linguagem provê símbolos de constantes, símbolos de funções e símbolos de relações ou predicados. Estruturas, ou modelos, consistem em domínios (ou conjuntos universo) não-vazios e interpretações dos símbolos de constantes, de funções, e predicados relevantes dentro sobre estes domínios.

Fixaremos uma axiomatização do calculo de predicados: axiomas lógicos e regras de intefência. Qualquer um das várias axiomatizações fará este papel; Assumimos sem demonstrar todos os resultados comumente conhecidos, como por exemplo o teorema da forma normal ou o teorema da correção

Consideraremos na realidade, que todas as fórmulas envolvidas nesta demonstração são desprovidas de símbolos de funções e de constantes. Este formato de fórmulas pode ser obtido aplicando-se técnicas de reescrita de fórmulas ao acrescentar alguns quantificadores. Este mesmo formalismo foi adotado por Gödel em sua dissertação original.

Teorema 1. Toda fórmula bem-formada universalmente válida é demonstrável[editar | editar código-fonte]

Esta é a forma mais básica do teorema da completude. Em seguida enunciaremos este teorema uma forma mais geral e conveniente nosso objetivos:

Teorema 2. Toda fórmula bem-formada φ é refutável ou satisfeita por um modelo.[editar | editar código-fonte]

"[pic 1] é refutável" significa por definição que "[pic 2] é demonstrável".

Note a equivalência entre os teoremas: se assumirmos que Teorema 1 vale, e [pic 3] não é satisfeita por nenhum modelo, então, [pic 4] é universalmente válida e consequentemente demonstrável. Por definição, segue que [pic 5] é refutável, logo, o Teorema 2 vale. Por outro lado, se assumirmos que o Teorema 2 é verdadeiro e que [pic 6] é universalmente válida, então [pic 7] é insatisfatível, e consequentemente refutável; portanto, [pic 8], e consequentemente [pic 9], é demonstrável. Assim, o Teorema 1 também é verdadeiro.

Iniciamos a prova do Teorema 2 restringindo sucessivamente a classe de todas as fórmulas [pic 10] possíveis para um conjunto para as quais precisamos verificar que "[pic 11] é refutável ou satisfatível". Assim, suponhamos que exista, para cada fórmula [pic 12], alguma fórmula [pic 13] retirada de um classe de fórmulas mais restrita C, tal que "[pic 14] é refutável ou satisfatível" implica "[pic 15] é refutável ou satisfatível". Uma vez que isto tenha sido verificado, será suficiente verificar que "[pic 16] é refutável ou satisfatível" fazê-lo para todo [pic 17] pertencente à classeC. Note que: se temos que a equivalência [pic 18] é demonstrável, então é realmente o caso que "[pic 19] é refutável ou satisfatível" implica "[pic 20] é refutável ou satisfatível".

Na prática, consideramos uma fórmula [pic 21] e aplicamos o teorema da forma prenexa para obter uma fórmula [pic 22], na forma normal tal que [pic 23]. Desta forma, precisamos apenas verificar o Teorema 2 para fórmulas [pic 24] que estejam nesta forma normal. Este mecanismo reduz a complexidade das fórmulas, sem que altere o resultado final da demonstração.

Uma vez nossas fórmulas estão na forma normal prenexa, podemos definir o prefixo de [pic 25] como o bloco que todos os quantificadores que aparecem na porção mais à esquerda de [pic 26] e a matriz de [pic 27] como sendo a fórmula livre de quantificadores que aparece à direita do prefixo de [pic 28].

Em seguida, eliminamos todas as variáveis livres em [pic 29] quantificando-as existencialmente. Assim, se [pic 30] representa o conjunto de todas as variáveis livres de [pic 31], formamos uma nova fórmula [pic 32]. Note que neste caso [pic 33], contudo estas duas fórmulas são refutáveis nas mesmas condições, o que não altera portanto o resultado desejado.

Por fim, gostaríamos, por motivos de conveniência técnica, que o prefixo da fórmula [pic 34] possuísse necessariamente um quantificador universal no início e um quantificador existencial no fim. Para conseguir isto sem alterar o sentido lógico de uma fórmula [pic 35] genérica, tomamos um símbolo de predicado unário F novo em [pic 36] juntamente com duas variáveis, também novas, y e z para construir: [pic 37], onde [pic 38] representa o prefixo de [pic 39] e [pic 40] representa a matriz de [pic 41], uma vez que [pic 42] é obviamente demonstrável.