# 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

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

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

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.

"$\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 que nossas fórmulas estão na forma normal prenexa, podemos definir o prefixo de $\psi \,\!$ como o bloco no qual 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

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)(\exists 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)(\exists 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')(\exists 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

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_{1}^{n}...a_{k}^{n})$.
Seja a fórmula $B_{n}=\varphi (z_{a_{1}^{n}}...z_{a_{k}^{n}},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_{1}^{n}}...z_{a_{k}^{n}})(\exists y_{1}...y_{m})\varphi (z_{a_{1}^{n}}...z_{a_{k}^{n}},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_{1}^{n}}...{a_{k}^{n}})<(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_{k}^{1}},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_{1}^{n}...a_{k}^{n},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
### 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 $\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

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_{k}^{i}\,\!$ como acima; então definimos $D_{k}\,\!$ como o fecho de $B_{1}^{1}...B_{k}^{1},...,B_{1}^{k}...B_{k}^{k}\,\!$. O restante da prova procede como anteriormente.