Teorema da completude de Gödel

Origem: Wikipédia, a enciclopédia livre.
Ir para: navegação, pesquisa
Question book.svg
Este artigo não cita fontes confiáveis e independentes. (desde Outubro de 2013). Por favor, adicione referências e insira-as corretamente no texto ou no rodapé. Conteúdo sem fontes poderá ser removido.
Encontre fontes: Google (notícias, livros e acadêmico)

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 derivar 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.

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]

"\varphi \,\! é refutável" significa por definição que "\lnot\varphi \,\! é demonstrável".

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

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

Na prática, consideramos uma fórmula \varphi \,\! e aplicamos o teorema da forma prenexa para obter uma fórmula \psi \,\!, na forma normal tal que \varphi \approx \psi \,\!. Desta forma, precisamos apenas verificar o Teorema 2 para fórmulas \varphi \,\! 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 \psi \,\! como o bloco que todos os quantificadores que aparecem na porção mais à esquerda de \psi \,\! e a matriz de \psi \,\! como sendo a fórmula livre de quantificadores que aparece à direita do prefixo de \psi \,\!.

Em seguida, eliminamos todas as variáveis livres em \varphi \,\! quantificando-as existencialmente. Assim, se \{x_1, ..., x_n\} \,\! representa o conjunto de todas as variáveis livres de \varphi \,\!, formamos uma nova fórmula \psi=\exists x_1 ... \exists x_n \varphi. Note que neste caso \varphi \not\approx \psi \,\!, 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 \varphi \,\! 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 \varphi \,\! genérica, tomamos um símbolo de predicado unário F novo em \varphi \,\! juntamente com duas variáveis, também novas, y e z para construir: \psi = \forall y (P) \exists z ( \Phi \wedge [ F(y) \vee \neg F(z) ] ), onde (P) \,\! representa o prefixo de \varphi \,\! e \Phi \,\! representa a matriz de \varphi \,\!, uma vez que \forall y \exists z ( F(y) \vee \neg F(z) ) é obviamente demonstrável.

Reduzindo o teorema a fórmulas de grau 1[editar | editar código-fonte]


Neste ponto, nossa fórmula genérica \varphi \,\! 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 \varphi \,\!, agruparemos os quantificadores de mesmo tipo de seu prefixo em blocos, da seguinte maneira:

\varphi = (\forall x_1 ... \forall x_{k_1})(\exists x_{k_1+1} ... \exists x_{k_2}).......(\forall x_{k_{n-2}+1} ... \forall x_{k_{n-1}})(\exists x_{k_{n-1}+1} ... \exists x_{k_n}) (\Phi)

Definimos grau de uma fórmula \varphi \,\! como o número de blocos de quantificadores universais, separados por blocos de quantificadores existenciais, no prefixo de \varphi \,\!. O lema seguinte nos permite reduzir a complexidade da fórmula genérica \varphi \,\! 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:

\varphi = (\forall x)(\exists y)(\forall u)(\exist v) (P) \psi

onde (P) \,\! representa o restante do prefixo de \varphi (que é consequentemente de grau k-1) e \psi \,\! é a matriz de \varphi \,\!. Aqui, as letras x, y, u e v denotam tuplas de variáveis ao invés de variáveis propriamente ditas; por exemplo: (\forall x) significa \forall x_1 \forall x_2 ... \forall x_n, onde x_1 ... x_n \,\! 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

\Phi = (\forall x')(\exists y') Q(x',y') \wedge (\forall x)(\forall y)( Q(x,y) \rightarrow (\forall u)(\exist v)(P)\psi )

Claramente, \Phi \rightarrow \phi é demonstrável.

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

( Q(x,y) \rightarrow (\forall u )(\exists v)(P) \psi) \equiv (\forall u)(\exists v)(P) ( Q(x,y) \rightarrow \psi )

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

\Phi' = (\forall x')(\exist y') Q(x',y') \wedge (\forall x)(\forall y) (\forall u)(\exists v)(P) ( Q(x,y) \rightarrow \psi )

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

\Psi = (\forall x')(\forall x)(\forall y) (\forall u)(\exists y')(\exists v)(P)Q(x',y') \wedge (Q(x,y) \rightarrow \psi )

e teremos \Phi' \approx \Psi.

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

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

Podemos agora substituir todas as ocorrêcias de Q dentro da fórmula demonstrável \neg \Phi \,\! 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 \neg \Phi \,\! pela fórmula (\forall u)(\exists v)(P)\psi(x,y|x',y'). Obteremos:

\neg ( (\forall x')(\exists y') (\forall u)(\exists v)(P)\psi(x,y|x',y') \wedge (\forall x)(\forall y) ( (\forall u)(\exists v)(P)\psi \rightarrow (\forall u)(\exists v)(P) \psi ) )

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 \varphi \,\!, apenas com x' e y' no lugar de x e y. Seque que \neg \varphi \,\! é demonstrável, e \varphi \,\! é rafutável.

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

Demonstração do teorema para fórmulas bem-formadas de grau 1[editar | editar código-fonte]


Como demonstrado pelo Lema acima, basta agora varificar o Teorema 2 para fórmulas \varphi \,\! contidas em R com grau 1. Uma vez que \varphi \,\! 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:

 (\forall x_1...x_k)(\exists y_1...y_m) \varphi(x_1...x_k, y_1...y_m) .

Definiremos agora uma ordenação das k-uplas de números naturais da seguinte maneira:  (x_1...x_k) < (y_1...y_k) \,\! deve ser o caso se  \Sigma_k (x_1...x_k) < \Sigma_k (y_1...y_k) \,\! é o caso ou  \Sigma_k (x_1...x_k) = \Sigma_k (y_1...y_k) \,\! é o caso e  (x_1...x_k) \,\! precede  (y_1...y_k) \,\! na ordem lexicográfica usual, onde  \Sigma_k (x_1...x_k) \,\! significa o somatório de todos os elementos da k-upla. Denotamos a n-ésima k-upla nesta ordem por  (a^n_1...a^n_k) .

Seja a fórmula  B_n = \varphi(z_{a^n_1}...z_{a^n_k}, z_{(n-1)m+2}, z_{(n-1)m+3}...z_{nm+1}) \,\! e seja D_n \,\! definida por

 (\exists z_1...z_{nm+1}) (B_1 \wedge B_2 ... \wedge B_n) \,\!

Lema: Para todo n, temos  \varphi \rightarrow D_n \,\!.

Desmonstração: Por indução sobre n; temos que  D_k \approx D_{k-1} \wedge (\exists z_1...z_{nm+1}) B_n \equiv D_{k-1} \wedge (\exists z_{a^n_1}...z_{a^n_k})(\exists y_1...y_m) \varphi(z_{a^n_1}...z_{a^n_k}, y_1...y_m) , onde a equivalência segue por substituição de variáveis, uma vez que a ordem das k-uplas é tal que (\forall k)({a^n_1}...{a^n_k}) < (n-1)m + 2. Cada parte da conjunção aqui segue obviamente de \varphi \,\!.

Assim, no caso base,  D_1 \approx (\exists z_1...z_{m+1}) \varphi(z_{a^1_1}...z_{a^1_k}, z_2, z_3...z_{m+1}) \approx (\exists z_1...z_{m+1}) \varphi(z_1...z_1, z_2, z_3...z_{m+1}) é obviamente um corolário de \varphi \,\!. Desta forma vale o Lema acima.

Por outro lado, se  D_n \,\! é refutável para um dado n, segue que \varphi \,\! também é refutável. Suponhamos agora que  D_n \,\! é satisfatível para um dado n. Então, para cada n existe alguma forma de atribuir um valor de verdade às sub-proposições E_h \,\! distintas em  B_k \,\! (ordenados por sua primeira aparição em  D_n \,\!; "distintos" aqui significa símbolos de predicados distintos ou variáveis ligadas distintas), de forma que  B_k \,\! 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 E_h \,\! aparecem sempre na mesma ordem em todos as  D_n \,\!, 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 E_1 \,\! ou temos que um número infinito delas tornam E_1 \,\! verdadeira, ou um número infinito torna E_1 \,\! falsas e somente uma quantidade finita de valorações tornam E_1 \,\! verdadeira. No primeiro caso, escolhemos E_1 \,\! de forma a ser verdadeira em geral, no segundo caso, escolhemos E_1 \,\! de forma a ser falta em geral. Assim, para os infinitos n's para os quais E_1 \,\! a E_{n-1} \,\! recebam os mesmos valores de verdade, escolhemos uma atribuição geral para E_h \,\! com o mesmo comportamento.

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

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

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

Extensões[editar | editar código-fonte]

Extensão para o cálculo de predicados de primeira ordem com igualdade[editar | editar código-fonte]

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 \varphi \,\! contendo alguma instância deste predicado pela seguinte fórmula:

 (\forall x) Eq(x, x) \wedge (\forall x,y,z) [Eq(x, y) \rightarrow (Eq(x, z) \rightarrow Eq(y, z))]  \wedge (\forall x,y,z) [Eq(x, y) \rightarrow (Eq(z, x) \rightarrow Eq(z, y))]  \wedge (\forall x_1...x_k, y_1...x_k) [(Eq(x_1, y_1) \wedge ... \wedge Eq(x_k, y_k)) \rightarrow (A(x_1...x_k) \equiv A(y_1...y_k))]  \wedge  ... \wedge (\forall x_1...x_m, y_1...x_m) [(Eq(x_1, y_1) \wedge ... \wedge Eq(x_m, y_m)) \rightarrow (Z(x_1...x_m) \equiv Z(y_1...y_m))]  \wedge \varphi'

Aqui, A ... Z< \,\! denota o predicado aparecendo em \varphi \,\! (com suas respectivas aridades k ... m \,\!), and \varphi' \,\! é a fórmula \varphi \,\! 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 \varphi \,\! 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 \varphi \,\! original.

Extensão para um conjunto contável de fórmulas[editar | editar código-fonte]

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  \varphi^i \,\! de grau 1, podemos definir  B^i_k \,\! como acima; então definimos  D_k \,\! como o fecho de  B^1_1...B^1_k, ..., B^k_1...B^k_k \,\!. O restante da prova procede como anteriormente.

Ver também[editar | editar código-fonte]

Referências[editar | editar código-fonte]