Prova original do teorema da completude de Gödel

Kurt Gödel (1925)

A prova do teorema da completude de Gödel dada por Kurt Gödel em sua dissertação de doutorado de 1929 (e uma versão mais curta da prova, publicada como um artigo em 1930, intitulado "A completude dos axiomas de o cálculo funcional da lógica' (em alemão)) não é fácil de ler hoje; usa conceitos e formalismos que não são mais usados e uma terminologia muitas vezes obscura. A versão abaixo tenta representar fielmente todas as etapas da prova e todas as ideias importantes, enquanto reafirma a prova na linguagem moderna da lógica matemática. Este esboço não deve ser considerado uma prova rigorosa do teorema.

Suposições

Trabalhamos com cálculo de predicados de primeira ordem. Nossas linguagens permitem símbolos de constante, função e relação. As estruturas consistem em domínios (não vazios) e interpretações dos símbolos relevantes como membros constantes, funções ou relações sobre esse domínio.

Assumimos a lógica clássica (em oposição à lógica intuicionista, por exemplo).

Corrigimos algumas axiomatizações (ou seja, um sistema de prova baseado em sintaxe e gerenciável por máquina) do cálculo de predicados: axiomas lógicos e regras de inferência. Qualquer uma das várias axiomatizações equivalentes bem conhecidas serve. A prova original de Gödel assumiu o sistema de prova de Hilbert-Ackermann.

Assumimos sem prova todos os resultados básicos bem conhecidos sobre nosso formalismo de que precisamos, como o teorema da forma normal ou o teorema da solidez.

Axiomatizamos o cálculo de predicados sem igualdade (às vezes chamado de maneira confusa de sem identidade), ou seja, não há axiomas especiais expressando as propriedades da igualdade (objeto) como um símbolo de relação especial. Após a demonstração da forma básica do teorema, será fácil estendê-lo ao caso de cálculo de predicados com igualdade.

Declaração do teorema e sua prova

A seguir, enunciamos duas formas equivalentes do teorema e mostramos sua equivalência.

Depois, provamos o teorema. Isso é feito nas seguintes etapas:

1. Reduzir o teorema a sentenças (formulas sem variáveis livres) em forma prenex, ou seja, com todos os quantificadores (Gerenciamento de contas e Detalhe) no início. Além disso, reduzimos a fórmulas cujo primeiro quantificador é Gerenciamento de contas. Isso é possível porque para cada frase, há um equivalente na forma prenex cujo primeiro quantificador é Gerenciamento de contas.
2. Reduzir o teorema a sentenças do formulário Gerenciamento de contasx₁Gerenciamento de contasx₂...x_k DetalheSim.₁DetalheSim.₂...Sim._m φ (x₁...x_k, Sim.₁...Sim._m). Embora não possamos fazer isso simplesmente rearranjando os quantificadores, mostramos que ainda é suficiente para provar o teorema para frases dessa forma.
3. Finalmente provamos o teorema por frases dessa forma.
   • Isto é feito pela primeira vez observando que uma frase como B ♥x₁Gerenciamento de contasx₂...x_k DetalheSim.₁DetalheSim.₂...Sim._m φ (x₁...x_k, Sim.₁...Sim._m) ou é refutável (sua negação é sempre verdadeira) ou satisfatível, ou seja, há algum modelo em que ele detém (pode até ser sempre verdade, ou seja, uma tautologia); este modelo é simplesmente atribuindo valores de verdade às subproposições de que B é construído. A razão para isso é a plenitude da lógica proposicional, com os quantificadores existenciais que não desempenham nenhum papel.
   • Nós estendemos este resultado a frases mais e mais complexas e longas, D_n (n=1,2...), construído a partir de B, de modo que qualquer um deles é refutável e, portanto, é φ, ou todos eles não são refutáveis e, portanto, cada um detém em algum modelo.
   • Finalmente usamos os modelos em que o D_n hold (em caso todos não são refutáveis) a fim de construir um modelo em que φ detém.

Teorema 1. Toda fórmula válida (verdadeira em todas as estruturas) é demonstrável.

Esta é a forma mais básica do teorema da completude. Nós imediatamente o reafirmamos de uma forma mais conveniente para nossos propósitos: Quando dizemos "todas as estruturas", é importante especificar que as estruturas envolvidas são interpretações clássicas (tarskianas) I, onde I=<U,F> (U é um conjunto não vazio (possivelmente infinito) de objetos, enquanto F é um conjunto de funções de expressões do simbolismo interpretado em U). [Em contraste, as chamadas "lógicas livres" semblante possivelmente conjuntos vazios para U. Para saber mais sobre lógica livre, consulte o trabalho de Karel Lambert.]

Teorema 2. Toda fórmula φ é refutável ou satisfatível em alguma estrutura.

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

Equivalência de ambos os teoremas

Se o Teorema 1 é válido e φ não é satisfatível em nenhuma estrutura, então ¬φ é válido em todas as estruturas e, portanto, demonstrável, portanto φ é refutável e o Teorema 2 detém. Se, por outro lado, o Teorema 2 for válido e φ for válido em todas as estruturas, então ¬φ não é satisfatível em nenhuma estrutura e, portanto, refutável; então ¬¬φ é demonstrável e φ também, assim o Teorema 1 é válido.

Demonstração do teorema 2: primeiro passo

Abordamos a prova do Teorema 2 restringindo sucessivamente a classe de todas as fórmulas φ para as quais precisamos provar que "φ é refutável ou satisfatível". No início, precisamos provar isso para todas as fórmulas φ possíveis em nossa linguagem. No entanto, suponha que para cada fórmula φ exista alguma fórmula ψ retirada de uma classe mais restrita de fórmulas C, tal que "ψ seja refutável ou satisfatível" → "φ é refutável ou satisfatível". Então, uma vez que esta afirmação (expressa na sentença anterior) é provada, será suficiente provar que "φ é refutável ou satisfatível" apenas para φ's pertencentes à classe C. Se φ é comprovadamente equivalente a ψ (i.e., (φ≡ψ) é demonstrável), então é de fato o caso que "ψ é refutável ou satisfatível" → "φ é refutável ou satisfatível" (o teorema da solidez é necessário para mostrar isso).

Existem técnicas padrão para reescrever uma fórmula arbitrária em uma que não use função ou símbolos constantes, ao custo da introdução de quantificadores adicionais; portanto, assumiremos que todas as fórmulas estão livres de tais símbolos. O artigo de Gödel usa uma versão do cálculo de predicados de primeira ordem que não tem nenhuma função ou símbolos constantes para começar.

Em seguida, consideramos uma fórmula genérica φ (que não usa mais funções ou símbolos constantes) e aplicamos o teorema da forma prenex para encontrar uma fórmula ψ na forma normal tal que φ≡ψ (ψ estando na forma normal significa que todos os quantificadores em ψ, se houver algum, são encontrados bem no início de ψ). Segue-se agora que precisamos apenas provar o Teorema 2 para as fórmulas φ na forma normal.

Em seguida, eliminamos todas as variáveis livres de φ quantificando-as existencialmente: se, digamos, x₁...x_n são livres em φ, nós formamos ${displaystyle psi =exists x_{1}...exists x_{n}phi }$. Se Ψ é satisfatível em uma estrutura M, então certamente assim é φ e se Ψ é refutável, então ${displaystyle neg psi =forall x_{1}... x_{n}neg phi }$ é provável, e então assim é ¬φ, assim φ é refutável. Nós vemos que podemos restringir φ para ser um sentença, isto é, uma fórmula sem variáveis livres.

Por último, gostaríamos, por razões de conveniência técnica, que o prefixo de φ (isto é, a cadeia de quantificadores no início de φ, que está em forma normal) começam com um quantificador universal e terminam com um quantificador existencial. Para conseguir isso para um genérico φ (sujeito a restrições que já provamos), tomamos algum símbolo de relação de um lugar F não utilizado em φ, e duas novas variáveis Sim. e zangão.... Se φ = (P) 0, onde (P) significa o prefixo de φ e Φ para o matriz de matriz (a parte restante, sem quantificador de φ) nós formamos ${displaystyle psi =forall y(P)exists z(Phi wedge [F(y)vee neg F(z)]}$. Desde então ${displaystyle forall yexists z(F(y)vee neg F(z)}$ é claramente provável, é fácil ver que ${displaystyle phi =psi }$ é provável.

Reduzindo o teorema a fórmulas de grau 1

Nossa fórmula genérica φ agora é uma sentença, na forma normal, e seu prefixo começa com um quantificador universal e termina com um quantificador existencial. Vamos chamar a classe de todas essas fórmulas de R. Temos que provar que toda fórmula em R é refutável ou satisfatível. Dada nossa fórmula φ, agrupamos sequências de quantificadores de um tipo em blocos:

${displaystyle phi =(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 o grau de $- Sim.$ para ser o número de blocos quantificadores universais, separados por blocos quantificadores existenciais como mostrado acima, no prefixo de $- Sim.$. O seguinte lemma, que Gödel adaptou da prova de Skolem do teorema de Löwenheim–Skolem, permite reduzir nitidamente a complexidade da fórmula genérica $- Sim.$ precisamos provar o teorema para:

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

Comentário: Tomar uma fórmula φ de grau k+1 do formulário ${displaystyle phi =(forall x)(exists y)(forall u)(exists v)(P)psi }$, onde $(P)psi }$ é o restante $- Sim.$ (é assim de grau - Sim.). φ afirma que para cada x há um y tal que... (algo). Teria sido bom ter um predicado Q ' para que para cada x, Q'(x,y) seria verdade se e somente se y é o necessário fazer (algo) verdadeiro. Então poderíamos ter escrito uma fórmula de grau k, que é equivalente a φ, ou seja, $(forall x')(forall x)(forall y)(forall u)(exists v)(exists y')(P)Q'(x',y')wedge (Q'(x,y)rightarrow psi)}$. Esta fórmula é de fato equivalente a φ porque afirma que para cada x, se há um y que satisfaz Q'(x,y), então (algo) detém, e além disso, sabemos que há tal y, porque para cada x ', há um y' que satisfaz Q'(x',y'). Portanto φ segue desta fórmula. Também é fácil mostrar que se a fórmula é falsa, então assim é φ. Infelizmente., em geral não há tal predicado Q'. No entanto, essa ideia pode ser entendida como uma base para a seguinte prova do Lemma.

Prova. Seja φ uma fórmula de grau k+1; então podemos escrevê-lo como

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

Onde? (P) é o restante do prefixo de $- Sim.$ (é assim de grau - Sim.) e $- Sim.$ é a matriz sem quantificador de $- Sim.$. x, Sim., u e v denota aqui tuplas de variáveis em vez de variáveis individuais; por exemplo. $(forall x)}$ realmente significa ${displaystyle forall x_{1}forall x_{2}... x_{n}}$ Onde? $Não. x_{1}...x_{n}}$ são algumas variáveis distintas.

Seja agora x' e y' tuplas de variáveis não utilizadas anteriormente com o mesmo comprimento que x e y respectivamente, e seja Q um símbolo de relação não utilizado anteriormente que receba tantos argumentos quanto a soma dos comprimentos de x e y; consideramos 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, $Não. Phi rightarrow phi }$ é provável.

Agora desde a cadeia de quantificadores $(forall u)(exists v)(P)}$ não contém variáveis de x ou Sim., a seguinte equivalência é facilmente provável com a ajuda de qualquer formalismo que estamos usando:

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

E como essas duas fórmulas são equivalentes, se substituirmos a primeira pela segunda dentro de Φ, obtemos a fórmula Φ' tal que Φ≡Φ':

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

Agora Φ' tem o formulário $(S)rho wedge (S')rho '}$, onde (S) e (S) são algumas cordas de quantificador, ρ e ρ' são sem quantificador, e, mais além, nenhuma variável (S) ocorre em ρ' e nenhuma variável de (S) ocorre em ρ. Sob tais condições, cada fórmula do formulário $(T)(rho wedge rho ')}$, onde (T) é uma cadeia de quantificadores contendo todos os quantificadores em (S) e (S') intercalados entre si de qualquer forma, mas manter a ordem relativa dentro (S) e (S'), será equivalente à fórmula original Φ'(este é mais um resultado básico no cálculo de predicado de primeira ordem em que confiamos). Para wit, formamos Ψ da seguinte forma:

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

nós temos $Não. Phi 'equiv Psi }$.

Agora! $- Sim.$ é uma fórmula de grau k e, portanto, por suposição refutável ou satisfatível. Se $- Sim.$ é satisfatível em uma estrutura M, então, considerando $Não. Psi equiv Phi 'equiv Phi wedge Phi rightarrow phi }$, vemos que $- Sim.$ também é satisfatível. Se $- Sim.$ é refutável, então assim é $Não. Não.$, que é equivalente a ele; assim ${displaystyle neg Phi }$ é provável. Agora podemos substituir todas as ocorrências de Q dentro da fórmula provável ${displaystyle neg Phi }$ por alguma outra fórmula dependente das mesmas variáveis, e ainda teremos uma fórmula provável. (Este é mais um resultado básico do cálculo de predicado de primeira ordem. Dependendo do formalismo particular adotado para o cálculo, pode ser visto como uma simples aplicação de uma regra de "substituição funcional" de inferência, como no artigo de Gödel, ou pode ser provado considerando a prova formal de ${displaystyle neg Phi }$, substituindo nele todas as ocorrências de Q por alguma outra fórmula com as mesmas variáveis livres, e observando que todos os axiomas lógicos na prova formal permanecem axiomas lógicos após a substituição, e todas as regras de inferência ainda se aplicam da mesma forma.)

Neste caso particular, substituimos Q(x',y') em ${displaystyle neg Phi }$ com a fórmula $(forall u)(exists v)(P)psi (x,y|x',y')}$. Aqui (x,y|x',y') significa que em vez de Ψ estamos escrevendo uma fórmula diferente, na qual x e y são substituídos por x' e y'. $(forall u)(exists v)(P)psi }$.

${displaystyle neg Phi }$ então se torna

${displaystyle neg ((forall x')(exists y')(forall u)(exists v)(P)psi (x,y|x',y')wedge (forall x)(forall y)(forall u)(forall u)(forall v)psi rightarrow (forall u)(psi v)})(P)})$

e esta fórmula é provável; desde a parte sob negação e após a $- Sim.$ sinal é obviamente provável, e a parte sob negação e antes $- Sim.$ sinal é obviamente φ, apenas com x e Sim. substituído por x ' e Sim. ', vemos que ${displaystyle neg phi }$ é provável, e φ é refutável. Provamos que φ é satisfatível ou refutável, e isto conclui a prova da Lemma.

Observe que não poderíamos ter usado $(forall u)(exists v)(P)psi (x,y|x',y')}$ em vez de Q(x',y') do início, porque $- Sim.$ não teria sido uma fórmula bem formada nesse caso. É por isso que não podemos usar ingênuamente o argumento que aparece no comentário que precede a prova.

Comentário: A prova até agora parece ter o seguinte erro principal: Φ, δ', e Ψ são conhecidos por ser de grau k, que é assumido para a indução em k, apenas sob a suposição de que Q é de grau 0. O passo acima que substitui Q(x',y') em ${displaystyle urcorner }$ δ com ($- Sim.$(${displaystyle exists }$v)(P)ψ(x,y|x',y') faz Q a ser de grau k, violando esta suposição para k > 0, invalidando assim a etapa de indução do grau k ao grau k+1.

Este argumento em mais detalhes:

Uma parte importante da prova é a indução no grau da fórmula sentencial arbitrária (significativa) φ, para mostrar que para todo inteiro k ≥ 1, se o teorema é válido para uma fórmula φ de grau k, então ele é válido para um de grau k+1, isto é, se toda fórmula sentencial válida de grau k é demonstrável (o que é equivalente a toda fórmula sentencial de grau k ser refutável ou satisfatível), então toda fórmula de grau k+1 é demonstrável (se esse equivalente para fórmulas sentenciais de grau k+1). Para fazer isso, a prova constrói fórmulas Φ ≡ Φ' ≡ Ψ, cada um contendo a relação Q e implicando um φ arbitrário de grau k+1, cada um dos quais três é de grau k se e somente se Q é de grau 0, o que a prova assume, de modo que pela hipótese de indução que o teorema vale para toda fórmula sentencial de grau k, as três fórmulas são refutáveis ou satisfazíveis. Então, se qualquer um dos três for satisfatível, φ também é satisfatível (pela estrutura detalhada das fórmulas). Se qualquer um for refutável, então ¬Φ é demonstrável. No entanto, sem ter provado o teorema para fórmulas de grau k+1, a prova então substitui Q em ¬Φ por uma fórmula de grau k, violando assim a suposição de indução de que Q é de grau 0, mas a prova, no entanto, conclui que, porque da hipótese de indução, se Φ não é satisfatível, então é refutável, então ¬Φ é demonstrável, então (por causa da estrutura detalhada de Φ) ¬φ é demonstrável, então φ é refutável, então se o teorema é verdadeiro para todos fórmulas sentenciais de grau k, é verdadeiro para todo grau k+1, portanto é verdadeiro para todo k se puder ser demonstrado que é verdadeiro para k = 1, o que supostamente é feito na próxima seção da prova. A violação da prova da suposição essencial de que Q é de grau 0 invalida o argumento de indução, portanto, invalida a prova. Este aparente erro está no argumento original de Gödel, conforme apresentado nas Collected Works of Kurt Gödel, vol. 3, ed. por Solomon Feferman et al., Oxford University Press, 1995.

Referências: Aristóteles para a lógica básica, Mathematical Logic de Joseph Shoenfield para a teoria da prova, Set Theory de Thomas Jech para a teoria dos modelos

Provando o teorema para fórmulas de grau 1

Como mostra o Lema acima, só precisamos provar nosso teorema para fórmulas φ em R de grau 1. φ não pode ser de grau 0, pois fórmulas em R não tem variáveis livres e não usa símbolos constantes. Assim, a fórmula φ tem a forma geral:

$(forall x_{1}...x_{k})(exists y_{1}...y_{m})phi (x_{1}...x_{k},y_{1}...y_{m}).}$

Agora nós definemos um ordenamento dos k-tuples de números naturais como segue: $(x_{1}...x_{k})<(y_{1}...y_{k}) ?$ deve segurar se ou $Não. Sigma _{k}(x_{1}...x_{k})< Sigma _{k}(y_{1}...y_{k}) ?$ou $Não. Sigma _{k}(x_{1}...x_{k})= Sigma _{k}(y_{1}...y_{k}) ?$e $(x_{1}...x_{k})}$ precede $(y_{1}...y_{k})}$ em ordem lexicográfica. Aqui. $Não. Sigma _{k}(x_{1}...x_{k}) ?$ denota a soma dos termos do tupla.] Denota o nono tupla nesta ordem por $(a_{1}^{n}...a_{k}^{n}) ?$.

Defina a fórmula $Não. B_{n}}$ como ${displaystyle phi (z_{a_{1}^{n}}...z_{a_{k}^{n}},z_{(n-1)m+2},z_{(n-1)m+3}...z_{nm+1})}$. Em seguida, coloque $Não. D_{n}}$ como

$(exists z_{1}...z_{nm+1})(B_{1}wedge B_{2}...wedge B_{n}).}$

Lemma: Para cada n, φ${displaystyle rightarrow D_{n}}$.

Prova: Por indução em n; temos $Não. D_{k}Leftarrow D_{k-1}wedge (forall z_{1}...z_{(n-1)m+1})(exists z_{(n-1)m+2}...z_{nm+1})B_{n}Leftarrow D_{k-1}wedge (forall z_{a_{1}^{n}}...z_{a_{k}^{n}})(exists y_{1}...y_{m})phi (z_{a_{1}^{n}}...z_{a_{k}^{n}},y_{1}...y_{m}) ?$, onde a última implicação detém por substituição variável, uma vez que a ordenação das tuplas é tal que $(forall k)({a_{1}^{n}}...{a_{k}^{n}})<(n-1)m+2}$. Mas a última fórmula é equivalente a $Não. D_{k-1}wedge }$φ.

Para o caso base, $Não. D_{1}equiv (exists z_{1}...z_{m+1})phi (z_{a_{1}^{1}}...z_{a_{k}^{1}},z_{2},z_{3}...z_{m+1})equiv (exists z_{1}...z_{m+1})phi (z_{1}...z_{1},z_{2},z_{3}...z_{m+1}) ?$ é obviamente um corolário de φ também. Então... Lemma está provado.

Agora, se $Não. D_{n}}$ é refutável para alguns n, segue que φ é refutável. Por outro lado, suponha que $Não. D_{n}}$ não é refutável para qualquer n. Então para cada n há alguma forma de atribuir valores de verdade às subproposições distintas ${displaystyle E_{h}}$ (ordenado por sua primeira aparição em $Não. D_{n}}$; "distinto" aqui significa predicados distintos, ou variáveis limitadas distintas) em $Não. B_{k}}$, tal que $Não. D_{n}}$ será verdade quando cada proposição é avaliada desta forma. Isto segue da plenitude da lógica proposicional subjacente.

Vamos agora mostrar que há uma tal atribuição de valores da verdade para ${displaystyle E_{h}}$, para que tudo $Não. D_{n}}$ será verdade: O ${displaystyle E_{h}}$ aparecem na mesma ordem em cada $Não. D_{n}}$; definiremos indutivamente uma atribuição geral a eles por uma espécie de "voto de maioria": Uma vez que há infinitamente muitas tarefas (um para cada um $Não. D_{n}}$) afectação $Não. E_{1}}$, ou infinitamente muitos fazem $Não. E_{1}}$ verdadeiro, ou infinitamente muitos fazem isso falso e apenas finitamente muitos fazem isso verdadeiro. No caso anterior, escolhemos $Não. E_{1}}$ para ser verdade em geral; neste último tomamos-o para ser falso em geral. Então, do infinito muitos n para os quais $Não. E_{1}}$ através de $Não. E_{h-1}}$ são atribuídos o mesmo valor da verdade como na atribuição geral, nós escolhemos uma atribuição geral para ${displaystyle E_{h}}$ da mesma forma.

Esta atribuição geral deve levar a cada um dos $Não. B_{k}}$ e $Não. D_{k}}$ ser verdade, desde se um dos $Não. B_{k}}$ foram falsos sob a atribuição geral, $Não. D_{n}}$ também seria falso para cada ). Mas isso contradiz o fato de que para a coleção finita de geral ${displaystyle E_{h}}$ atribuições aparecendo em $Não. D_{k}}$, há infinitamente muitos n onde a designação $Não. D_{n}}$ verdadeiro corresponde à missão geral.

A partir desta atribuição geral, que faz todo o $Não. D_{k}}$ verdade, nós construímos uma interpretação dos predicados da linguagem que faz φ verdadeiro. O universo do modelo será o número natural. Cada predicado i-ary $- Sim.$ deve ser verdade dos naturais $(u_{1}...u_{i})}$ precisamente quando a proposição ${displaystyle Psi (z_{u_{1}}...z_{u_{i}}) ?$ ou é verdadeiro na atribuição geral, ou não atribuído por ele (porque nunca aparece em nenhum dos $Não. D_{k}}$).

Neste modelo, cada uma das fórmulas $(exists y_{1}...y_{m})phi (a_{1}^{n}...a_{k}^{n},y_{1}...y_{m}) ?$ é verdade pela construção. Mas isso implica que o próprio φ é verdadeiro no modelo, uma vez que ${displaystyle a^{n}}$ gama sobre todos os possíveis k-tuples de números naturais. Então φ é satisfatível, e nós somos feitos.

Explicação intuitiva

Podemos escrever cada B_i como Φ(x₁...x_k,y₁...y_m) para alguns x-s, que podemos chamar de "primeiros argumentos" e y-s que podemos chamar de "últimos argumentos".

Pegue B₁ por exemplo. Seus "últimos argumentos" são z₂,z₃...z_m+1, e para cada combinação possível de k dessas variáveis existe algum j então que eles aparecem como "primeiros argumentos" em B_j. Assim, para n₁ grande o suficiente, D_n1 tem a propriedade de que os "últimos argumentos" de B₁ aparecem, em todas as combinações possíveis de k deles, como "primeiros argumentos" em outros B_j-s dentro de D_n. Para cada B_i existe um D_ni com a propriedade correspondente.

Portanto, em um modelo que satisfaça todos os D_n-s, existem objetos correspondentes a z₁, z₂... e cada combinação de k deles aparece como "primeiros argumentos" em algum B_j, significando que para cada k desses objetos z_p1...z_{pk< /sub> existem zq1...zqm, o que torna Φ (zp1...zpk,zq1...zqm) satisfeito. Tomando um submodelo com apenas esses objetos z1, z2..., temos um modelo que satisfaz φ.}

Extensões

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

Gödel reduziu uma fórmula contendo instâncias do predicado de igualdade a outras sem ele em uma linguagem estendida. Seu método envolve a substituição de uma fórmula φ contendo algumas instâncias de igualdade pela fórmula

$(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)]}$
$- Sim.$
$(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})]}$
$- Sim.$
$- Sim.$

Aqui. $Não. AZ$ denote os predicados que aparecem em φ (com $Não.$ suas respectivas aridades), e φ' é a fórmula φ com todas as ocorrências de igualdade substituídas pelo novo predicado Eq. Se esta nova fórmula é refutável, o original φ também foi; o mesmo é verdade de satisfação, uma vez que podemos tomar um quociente de modelo satisfatório da nova fórmula pela relação de equivalência que representa a Eq. Este quociente é bem definido em relação aos outros predicados, e, portanto, irá satisfazer a fórmula original φ.

Extensão para conjuntos contáveis de fórmulas

Gödel também considerou o caso em que há uma coleção contável infinita de fórmulas. Usando as mesmas reduções acima, ele foi capaz de considerar apenas os casos em que cada fórmula é de grau 1 e não contém usos de igualdade. Para uma coleção contável de fórmulas ${displaystyle phi ^{i}}$ de grau 1, podemos definir $Não. B_{k}^{i}}$ como acima; então definir $Não. D_{k}}$ para ser o fechamento de $Não. B_{1}^{1}... B_{k}^{1},...,B_{1}^{k}... B_{k}^{k}}$. O restante da prova então passou como antes.

Extensão para conjuntos arbitrários de fórmulas

Quando existe uma coleção incontável e infinita de fórmulas, o Axioma da Escolha (ou pelo menos alguma forma fraca dele) é necessário. Usando o AC completo, pode-se ordenar bem as fórmulas e provar o caso incontável com o mesmo argumento do contável, exceto com indução transfinita. Outras abordagens podem ser usadas para provar que o teorema da completude neste caso é equivalente ao teorema do ideal primo booleano, uma forma fraca de AC.