Teorema da completude de Gödel
Origem: Wikipédia, a enciclopédia livre.
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 formula logicamente válida pode ser demonstrada no cálculo de predicados de primeira ordem, isto é, existe uma derivação formal para esta formula. 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 formula é 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 dereivar todas as formulas logicamente válidas.
O resultado dual à completude é a correção. O fato de que a 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.
Índice |
[editar] Demonstração
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.
[editar] Definições e pressupostos
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.
[editar] Teorema 1. Toda fórmula bem-formada universalmente válida é demonstrável
Esta é a forma mais básica do teorema da completude. Em seguida enunciaremos este teorema uma forma mais geral e conveniente nosso objetivos:
[editar] Teorema 2. Toda fórmula bem-formada φ é refutável ou satisfeita por um modelo.
" é 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 checar 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 em " é 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 em " é 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 nossas fórmulas estão na forma normal prenexa, podemos definir o prefixo de como o bloco que 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 é óbviamente demonstrável.
[editar] Reduzindo o teorema a fórmulas de grau 1:
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 é óbviamente , 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.
[editar] Demonstração do teorema para fórmulas bem-formadas de grau 1
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.
[editar] Extensões
[editar] Extensão para o cálculo de predicados de primeira ordem com igualdade
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.
[editar] Extensão para um conjunto contável de fórmulas
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.