Teorema da completude de Gödel

Este artigo ou secção contém uma lista de referências no fim do texto, mas as suas fontes não são claras porque não são citadas no corpo do artigo, o que compromete a confiabilidade das informações. Ajude a melhorar este artigo inserindo citações no corpo do artigo. (Outubro de 2013)

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 | 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 ideias 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 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 | editar código-fonte]

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 | editar código-fonte]

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

Note a equivalência entre os teoremas: se assumirmos que Teorema 1 vale, e ${\displaystyle \varphi \,\!}$ não é satisfeita por nenhum modelo, então, ${\displaystyle \lnot \varphi \,\!}$ é universalmente válida e consequentemente demonstrável. Por definição, segue que ${\displaystyle \varphi \,\!}$ é refutável, logo, o Teorema 2 vale. Por outro lado, se assumirmos que o Teorema 2 é verdadeiro e que ${\displaystyle \varphi \,\!}$ é universalmente válida, então ${\displaystyle \lnot \varphi \,\!}$ é insatisfatível, e consequentemente refutável; portanto, ${\displaystyle \lnot \lnot \varphi \,\!}$, e consequentemente ${\displaystyle \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 ${\displaystyle \varphi \,\!}$ possíveis para um conjunto para as quais precisamos verificar que "${\displaystyle \varphi \,\!}$ é refutável ou satisfatível". Assim, suponhamos que exista, para cada fórmula ${\displaystyle \varphi \,\!}$, alguma fórmula ${\displaystyle \psi \,\!}$ retirada de um classe de fórmulas mais restrita C, tal que "${\displaystyle \psi \,\!}$ é refutável ou satisfatível" implica "${\displaystyle \varphi \,\!}$ é refutável ou satisfatível". Uma vez que isto tenha sido verificado, será suficiente verificar que "${\displaystyle \varphi \,\!}$ é refutável ou satisfatível" fazê-lo para todo ${\displaystyle \varphi \,\!}$ pertencente à classe C. Note que: se temos que a equivalência ${\displaystyle \varphi \approx \psi \,\!}$ é demonstrável, então é realmente o caso que "${\displaystyle \psi \,\!}$ é refutável ou satisfatível" implica "${\displaystyle \varphi \,\!}$ é refutável ou satisfatível".

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

Em seguida, eliminamos todas as variáveis livres em ${\displaystyle \varphi \,\!}$ quantificando-as existencialmente. Assim, se ${\displaystyle \{x_{1},...,x_{n}\}\,\!}$ representa o conjunto de todas as variáveis livres de ${\displaystyle \varphi \,\!}$, formamos uma nova fórmula ${\displaystyle \psi =\exists x_{1}...\exists x_{n}\varphi }$. Note que neste caso ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \varphi \,\!}$ genérica, tomamos um símbolo de predicado unário F novo em ${\displaystyle \varphi \,\!}$ juntamente com duas variáveis, também novas, y e z para construir: ${\displaystyle \psi =\forall y(P)\exists z(\Phi \wedge [F(y)\vee \neg F(z)])}$, onde ${\displaystyle (P)\,\!}$ representa o prefixo de ${\displaystyle \varphi \,\!}$ e ${\displaystyle \Phi \,\!}$ representa a matriz de ${\displaystyle \varphi \,\!}$, uma vez que ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \varphi \,\!}$, agruparemos os quantificadores de mesmo tipo de seu prefixo em blocos, da seguinte maneira:

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

${\displaystyle \varphi =(\forall x)(\exists y)(\forall u)(\exists v)(P)\psi }$

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

${\displaystyle \Phi =(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(Q(x,y)\rightarrow (\forall u)(\exists v)(P)\psi )}$

Claramente, ${\displaystyle \Phi \rightarrow \phi }$ é demonstrável.

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

${\displaystyle (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 ${\displaystyle \Phi \,\!}$, iremos obter a fórmula ${\displaystyle \Phi '\,\!}$, para qual vale ${\displaystyle \Phi \approx \Phi '\,\!}$:

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

${\displaystyle \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 ${\displaystyle \Phi '\approx \Psi }$.

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

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

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

${\displaystyle \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 ${\displaystyle \varphi \,\!}$, apenas com x' e y' no lugar de x e y. Seque que ${\displaystyle \neg \varphi \,\!}$ é demonstrável, e ${\displaystyle \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 ${\displaystyle \varphi \,\!}$ contidas em R com grau 1. Uma vez que ${\displaystyle \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:

${\displaystyle (\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: ${\displaystyle (x_{1}...x_{k})<(y_{1}...y_{k})\,\!}$ deve ser o caso se ${\displaystyle \Sigma _{k}(x_{1}...x_{k})<\Sigma _{k}(y_{1}...y_{k})\,\!}$ é o caso ou ${\displaystyle \Sigma _{k}(x_{1}...x_{k})=\Sigma _{k}(y_{1}...y_{k})\,\!}$ é o caso e ${\displaystyle (x_{1}...x_{k})\,\!}$ precede ${\displaystyle (y_{1}...y_{k})\,\!}$ na ordem lexicográfica usual, onde ${\displaystyle \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 ${\displaystyle (a_{1}^{n}...a_{k}^{n})}$.

Seja a fórmula ${\displaystyle 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 ${\displaystyle D_{n}\,\!}$ definida por

${\displaystyle (\exists z_{1}...z_{nm+1})(B_{1}\wedge B_{2}...\wedge B_{n})\,\!}$

Lema: Para todo n, temos ${\displaystyle \varphi \rightarrow D_{n}\,\!}$.

Desmonstração: Por indução sobre n; temos que ${\displaystyle 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 ${\displaystyle (\forall k)({a_{1}^{n}}...{a_{k}^{n}})<(n-1)m+2}$. Cada parte da conjunção aqui segue obviamente de ${\displaystyle \varphi \,\!}$.

Assim, no caso base, ${\displaystyle 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 ${\displaystyle \varphi \,\!}$. Desta forma vale o Lema acima.

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

Esta atribuição geral deve tornar todo ${\displaystyle B_{k}\,\!}$ e todo ${\displaystyle D_{k}\,\!}$ verdadeiras, uma vez que se pelo menos um ${\displaystyle B_{k}\,\!}$ for falso, ${\displaystyle 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 ${\displaystyle E_{h}\,\!}$ aparecendo em ${\displaystyle D_{k}\,\!}$, existem infitos n's esta atribuição ao satisfazer ${\displaystyle D_{n}\,\!}$ valida a atribuição geral.

Por fim, a partir desta atribuição geral que torna as fórmulas ${\displaystyle D_{k}\,\!}$ em valores de verdadeiras, construímos uma interpretação dos predicados da linguagem que também torna ${\displaystyle \phi \,\!}$ verdadeira. O universo de quantificação será os números naturais. Cada predicádo i-ário ${\displaystyle \Psi \,\!}$ deve ser verdadeiro para os naturais ${\displaystyle (u_{1}...u_{i})\,\!}$ precisamente quando a proposição ${\displaystyle \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 ${\displaystyle \Psi \,\!}$ em ${\displaystyle D_{k}\,\!}$).

Neste modelo, cada fórmula ${\displaystyle (\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 ${\displaystyle \varphi \,\!}$ é verdadeira neste modelo, pois ${\displaystyle a^{n}\,\!}$ toma como valores possívels todas as k-uplas de números naturais. Desta forma ${\displaystyle \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 ${\displaystyle \varphi \,\!}$ contendo alguma instância deste predicado pela seguinte fórmula:

${\displaystyle (\forall x)Eq(x,x)\wedge (\forall x,y,z)[Eq(x,y)\rightarrow (Eq(x,z)\rightarrow Eq(y,z))]}$ ${\displaystyle \wedge (\forall x,y,z)[Eq(x,y)\rightarrow (Eq(z,x)\rightarrow Eq(z,y))]}$ ${\displaystyle \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}))]}$ ${\displaystyle \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}))]}$ ${\displaystyle \wedge \varphi '}$

Aqui, ${\displaystyle A...Z<\,\!}$ denota o predicado aparecendo em ${\displaystyle \varphi \,\!}$ (com suas respectivas aridades ${\displaystyle k...m\,\!}$), and ${\displaystyle \varphi '\,\!}$ é a fórmula ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \varphi ^{i}\,\!}$ de grau 1, podemos definir ${\displaystyle B_{k}^{i}\,\!}$ como acima; então definimos ${\displaystyle D_{k}\,\!}$ como o fecho de ${\displaystyle B_{1}^{1}...B_{k}^{1},...,B_{1}^{k}...B_{k}^{k}\,\!}$. O restante da prova procede como anteriormente.

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

• Kurt Gödel
• Lógica de primeira ordem
• Completude (lógica)
• Teorema da Incompletude de Gödel

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

• Original proof of Gödel's completeness theorem
• Gödel's completeness theorem