Teorema da completude de Gödel

O Teorema da completude de Gödel é um importante teorema da lógica matemática, demonstrado originalmente por Kurt Gödel, em 1929. Ele defende, em sua forma mais usual, que toda fórmula logicamente válida pode ser demonstrada no cálculo de predicados de primeira ordem, isto é, existe uma derivação formal para esta fórmula. Tal derivação é uma lista finita de passos em que cada passo é obtido através de um axioma, ou de regras de inferência básicas aplicadas a passos anteriores.

Uma fórmula é dita logicamente válida se for verdadeira em todos os modelos da linguagem subjacente. Modelo, neste contexto, define um conjunto universo a ser considerado e as devidas interpretações das funções e predicados de primeira ordem.

Em outras palavras, o Teorema da Completude de Gödel diz que as regras de inferência da lógica de primeira ordem são completas no sentido de que nenhuma nova regra de inferência é necessária para derivar todas as fórmulas logicamente válidas.

O resultado dual à completude é a correção. O fato de que o cálculo de predicados de primeira ordem é correto, ou seja, que somente sentenças logicamente válidas podem ser derivadas na lógica de primeira ordem, é garantido pelo Teorema da correção.

Demonstração editar

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 ideias importantes originais. Este esboço não deve ser considerado uma demonstração rigorosa do teorema.

Definições e pressupostos editar

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 cálculo de predicados: axiomas lógicos e regras de inferência. Qualquer uma 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

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

Teorema 2. Toda fórmula bem-formada φ é refutável ou satisfeita por um modelo. editar

"  é refutável" significa por definição que "  é demonstrável".

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

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

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

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

Em seguida, eliminamos todas as variáveis livres em   quantificando-as existencialmente. Assim, se   representa o conjunto de todas as variáveis livres de  , formamos uma nova fórmula  . Note que neste caso  , 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   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   genérica, tomamos um símbolo de predicado unário F novo em   juntamente com duas variáveis, também novas, y e z para construir:  , onde   representa o prefixo de   e   representa a matriz de  , uma vez que   é obviamente demonstrável.

Reduzindo o teorema a fórmulas de grau 1 editar


Neste ponto, nossa fórmula genérica   já é uma sentença (não possui variáveis livres), está na forma normal e seu prefixo se inicia com um quantificador universal e termina com um quantificador existencial. Denominaremos classe R a classe que contém todas as fórmulas deste tipo. Desta forma, nosso problema se resume a verificar que toda e qualquer fórmula em R é refutável ou satisfatível. Dada nossa fórmula  , agruparemos os quantificadores de mesmo tipo de seu prefixo em blocos, da seguinte maneira:

 

Definimos grau de uma fórmula   como o número de blocos de quantificadores universais, separados por blocos de quantificadores existenciais, no prefixo de  . O lema seguinte nos permite reduzir a complexidade da fórmula genérica   de maneira considerável.

Lema. Seja k>=1. Se toda fórmula em R de grau k é refutável ou satisfatível, então toda fórmula em R de grau k+1 também o será.

Demonstração. Seja φ uma fórmula de grau k+1. Podemos escrevê-la da seguinte forma:

 

onde   representa o restante do prefixo de   (que é consequentemente de grau k-1) e   é a matriz de  . Aqui, as letras x, y, u e v denotam tuplas de variáveis ao invés de variáveis propriamente ditas; por exemplo:   significa  , onde   são variáveis distintas.

Sejam agora x'' and y' duas tuplas de variáveis novas de mesmo comprimento que x and y respectivamente. Seja Q um novo símbolo de predicado que tem aridade igual à soma dos comprimentos de x e y. Considere a fórmula

 

Claramente,   é demonstrável.

Note que devido ao fato dos quantificadores   não conterem as variáveis contidas nas tuplas x ou y, a equivalência seguinte é facilmente demonstrável:

 

E como estas duas fórmulas são equivalentes, se substituirmos a primeira pela segunda no lugar de  , iremos obter a fórmula  , para qual vale  :

 

Desta forma,   é da forma  , onde   e   são sequências de quantificadores,   e   são livres de quantificadores, e, além disto, nenhuma variável quantificada por   ocorre em   e nenhuma variável quantificada por   ocorre em  . Nestas condições, toda e qualquer fórmula na forma  , sendo   a sequência de todos os quantificadores de   e   misturados de maneira arbitrária, porém mantendo a ordem relativa dentro de   e  , será equivalente à fórmula   original. Assim, definimos   como:

 

e teremos  .

Temos agora que   é uma fórmula de grau k e consequentemente é refutável ou satisfatível (pela hipótese de indução). Se   é satisfeita num dado modelo M, então, considerando  , concluímos que   também será satisfeita em M.

Por outro lado, se   é refutável, então   também será refutável, pois são equivalentes, e assim   is demonstrável.

Podemos agora substituir todas as ocorrêcias de Q dentro da fórmula demonstrável   por alguma uma outra fórmula dependete das mesmas variáveis. Esta substituição irá gerar uma outra fórmula demonstrável.

Neste caso particular, substituiremos as ocorrências de Q em   pela fórmula  . Obteremos:

 

e, como vimos, esta fórmula é demonstrável. Vemos aqui que a parte desta fórmula sob o escopo da negação e após a conjunção é obviamente demonstrável, e que a parte desta fórmula sob o escopo da negação e antes da conjunção é obviamente  , apenas com x' e y' no lugar de x e y. Seque que   é demonstrável, e   é rafutável.

Concluímos assim a demonstração do Lema.

Demonstração do teorema para fórmulas bem-formadas de grau 1 editar


Como demonstrado pelo Lema acima, basta agora varificar o Teorema 2 para fórmulas   contidas em R com grau 1. Uma vez que   não pode ser uma fórmula de grau 0, já que as fórmulas em R não têm símbolos de constantes ou de funções, terá a fomra:

 .

Definiremos agora uma ordenação das k-uplas de números naturais da seguinte maneira:   deve ser o caso se   é o caso ou   é o caso e   precede   na ordem lexicográfica usual, onde   significa o somatório de todos os elementos da k-upla. Denotamos a n-ésima k-upla nesta ordem por  .

Seja a fórmula   e seja   definida por

 

Lema: Para todo n, temos  .

Desmonstração: Por indução sobre n; temos que  , onde a equivalência segue por substituição de variáveis, uma vez que a ordem das k-uplas é tal que  . Cada parte da conjunção aqui segue obviamente de  .

Assim, no caso base,   é obviamente um corolário de  . Desta forma vale o Lema acima.

Por outro lado, se   é refutável para um dado n, segue que   também é refutável. Suponhamos agora que   é satisfatível para um dado n. Então, para cada n existe alguma forma de atribuir um valor de verdade às sub-proposições   distintas em   (ordenados por sua primeira aparição em  ; "distintos" aqui significa símbolos de predicados distintos ou variáveis ligadas distintas), de forma que   assumirá um valor verdadeiro quando cada uma de suas sub-proposições também o fizerem. Este resultado segue do Teorema da Completude da lógica proposicional.

Uma vez que as   aparecem sempre na mesma ordem em todos as  , podemos definir indutivamente uma atribuição geral para esta usando uma esécie de "voto majoritário": Uma vez que há infinitas atribuições que afétam   ou temos que um número infinito delas tornam   verdadeira, ou um número infinito torna   falsas e somente uma quantidade finita de valorações tornam   verdadeira. No primeiro caso, escolhemos   de forma a ser verdadeira em geral, no segundo caso, escolhemos   de forma a ser falta em geral. Assim, para os infinitos n's para os quais   a   recebam os mesmos valores de verdade, escolhemos uma atribuição geral para   com o mesmo comportamento.

Esta atribuição geral deve tornar todo   e todo   verdadeiras, uma vez que se pelo menos um   for falso,   também o será para todo n > k, porém isto contradiz o fato que para uma coleção finita de atribuições gerais   aparecendo em  , existem infitos n's esta atribuição ao satisfazer   valida a atribuição geral.

Por fim, a partir desta atribuição geral que torna as fórmulas   em valores de verdadeiras, construímos uma interpretação dos predicados da linguagem que também torna   verdadeira. O universo de quantificação será os números naturais. Cada predicádo i-ário   deve ser verdadeiro para os naturais   precisamente quando a proposição   for verdadeira na atribuição geral, ou não recebe um valor de verdade nesta atribuição (caso não existam instâncias de   em  ).

Neste modelo, cada fórmula   é válida por construção. Mas isto implica que a própria fórmula   é verdadeira neste modelo, pois   toma como valores possívels todas as k-uplas de números naturais. Desta forma   também é satisfatível.

Extensões editar

Extensão para o cálculo de predicados de primeira ordem com igualdade editar

Gödel reduziu uma fórmula contendo instâncias do predicado de igualdade a fórmulas que não o continham em uma linguagem estendida. Seu método envolveu a substitução de uma fórmula   contendo alguma instância deste predicado pela seguinte fórmula:

         

Aqui,   denota o predicado aparecendo em   (com suas respectivas aridades  ), and   é a fórmula   com todas as ocorrências da igualdade substituídas pelo novo predicado Eq.

Se esta nova fórmula for refutável, então a fórmula   original já era refutável; o mesmo vale para a satisfatibilidade desta nova fórmula, uma vez que podemos tomar o quociente de um modelo satisfatório da nova fórmula através da relação de equivalência Eq. Este quociente é bem-feinido em relação aos outros predicados, e portanto, irá satisfazer a fórmula   original.

Extensão para um conjunto contável de fórmulas editar

Gödel também considerou o caso onde existe um número infinito, porém contável, de fórmulas na coleção. Utilizando-se das mesmas reduções acima apresentas, ele considerou apenas os cados aonde cada fórmula é de grau 1 e não contém igualdade. Para uma coleção contável de fórmulas   de grau 1, podemos definir   como acima; então definimos   como o fecho de  . O restante da prova procede como anteriormente.

Ver também editar

Referências editar