# Teorema Löwenheim–Skolem

O teorema de Löwenheim–Skolem da lógica matemática afirma que, dado um conjunto de expressões Γ da lógica de primeira ordem, se houver uma estrutura que é modelo de Γ e possui cardinalidade infinita, então para todo número cardinal infinito k, existe uma estrutura A de cardinalidade k que também é modelo de Γ. Isso nos leva à questão da Lógica de predicados não ser capaz de controlar a cardinalidade de seus modelos infinitos, além de que nenhum conjunto de expressões de primeira ordem que possua um modelo de cardinalidade infinita possui um único modelo.
O teorema de Löwenheim–Skolem, junto com o teorema da Compacidade, é uma peça importante na constatação do Teorema de Lindstrom, para caracterizar a Lógica de primeira ordem. Em geral, O teorema de Löwenheim–Skolem não se aplica a áreas mais complexas da Lógica, tal como para a Lógica de Segunda Ordem.

## Background

Uma assinatura (lógica) consiste num conjunto possivelmente vazio de símbolos de funções, cada qual com sua respectiva aridade, um conjunto possivelmente vazio de símbolos de relações, cada uma com sua respectiva aridade, e de um conjunto, que também pode ser vazio, de símbolos de constantes. Na lógica de primeira ordem, a noção de assinatura está associada à noção de estrutura matemática.
Um teorema da lógica de primeira-ordem consiste num conjunto de sentenças em uma determinada linguagem. Teorias são comumente especificadas a partir de um conjunto de axiomas, ou retirando sua base através de um conjunto de sentenças que satisfazem uma determinada estrutura.
Dada uma assinatura L e uma estrutura A, uma interpretação de L em A consiste na associação de cada símbolo de função n-ária de L a uma função de A de aridade n, cada símbolo de relação n-ária R de L a uma relação n-ária da estrutura A e cada símbolo de constante a um elemento destacado de A. Essa associação tem o intuito de dar significado aos símbolos de L, tal que ao utilizar um dado símbolo de função de L, por exemplo, está sendo feita uma referência à função associada de A.
Seja L uma assinatura. Dadas duas L-estrutura A e B, dizer que B está contida em A (B é subestrutura de A), significa que as seguintes exigências são cumpridas:
* Primeira Exigência: O domínio de B está contido no domínio de A;
* Segunda Exigência: Existe um homomosrfismo Imersor entre A e B (as funções, relações e destaques são preservados).
Uma subestrutura elementar B de A é tal que satisfaz exatamente as mesmas sentenças que a estrutura original A (dizemos que A é uma extensão elementar de B).

## Definição Precisa

A versão atual do Teorema de Löwenheim–Skolem é mais geral e mais abrangente que a breve explicação passada na introdução desse artigo.
O teorema estabelece que para toda assinatura L, para toda estrutura infinita A e para todo número cardinal infinito k ≠ |A|, existe uma L-estrutura B, tal que |B| = k e:
* se k < |A| então B é uma subestrutura elementar de A;
* se k > |A| então B é uma extensão elementar de A.
O teorema se divide em duas partes. A sessão que estabelece que existem subestruturas elementares com cardinalidades infinitas inferiores é conhecida como Top-down Löwenheim–Skolem Theorem. A sessão que estabelece que a estrutura em questão possui extensões elementares de maiores cardinalidades é conhecida como Bottom-up Löwenheim–Skolem Theorem.

## Prova do Teorema
### Sessão Top-down

Para cada fórmula de primeira-ordem $\sigma \,$ $\varphi (y,x_{1},\ldots ,x_{n})\,,$ o axioma da escolha afirma a existência de uma função
    $f_{\varphi }:M^{n}\to M$
tal que, para todo $a_{1},\ldots ,a_{n}\in M$, ou
    $M\models \varphi (f_{\varphi }(a_{1},\dots ,a_{n}),a_{1},\dots ,a_{n})$
ou
    $M\models \neg \exists y\varphi (y,a_{1},\dots ,a_{n})\,.$
Aplicando mais uma vez o axioma da escolha, obtemos uma função das fórmula de primeira ordem $\varphi$ para tais funções $f_{\varphi }\,.$
A família de funções $f_{\varphi }$ dá origem ao operador de pré-encerramento $F\,$ no conjunto das partes de $M\,$
    $F(A)=\{b\in M\mid b=f_{\varphi }(a_{1},\dots ,a_{n});\,\varphi \in \sigma ;\,a_{1},\dots ,a_{n}\in A\}$
para $A\subseteq M\,.$
Iterando várias vezes resulta n
Iterando $F\,$ várias vezes resulta em um operador de encerramento $F^{\omega }\,.$ Tomando um subconjunto arbitrário $A\subseteq M$ tal que $\left\vert A\right\vert =\kappa$, e tendo definido $N=F^{\omega }(A)\,,$ também é possível perceber que $\left\vert N\right\vert =\kappa \,.$ $N\,$ é uma subestrutura elementar de $M\,$ através do teste de Tarski–Vaught.
A técnica utilizada nessa prova é atribuída a Skolem, que introduziu símbolos de funções para as Funções de Skolem $f_{\varphi }$ na linguagem. Também é possível definir $f_{\varphi }$ como função parcial de forma que $f_{\varphi }$ é definido se e somente se $M\models \exists y\varphi (y,a_{1},\dots ,a_{n})\,.$ O único ponto importante é que $F\,$ é um operador de pré-encerramento tal que $F(A)\,$ contém uma solução para cada fórmula com parâmetros em $A\,$ que possui solução em $M\,$ e
    $\left\vert F(A)\right\vert \leq \left\vert A\right\vert +\left\vert \sigma \right\vert +\aleph _{0}\,.$

### Sessão Bottom-Up

De início, a extensão da assinatura L é feita adicionando-se um novo símbolo de constante em L para cada elemento de A. A teoria completa de A para a assinatura estendida L´ é chamada Diagrama Completo de A. Em seguida, são adicionadas as sentenças do tipo c1 ≠ c2 para cada dois símbolos de constante distintos de L. Utilizando o teorema da compaccidade, a teoria resultante é facilmente provada consistente. Visto que os modelos de L´ devem ter cardinalidade no mínimo k, a sessão top-down desse teorema garante que exista um modelo B de cardinalidade k, extensão elementar de A.