# Tipo (teoria do modelo)

Na teoria do modelo e áreas relacionadas da matemática, um tipo é um objeto que, falando livremente, descreve como um elemento (real ou possível) ou elementos em uma estrutura matemática podem se comportar. Mais precisamente, é um conjunto de fórmulas de primeira ordem em uma linguagem L com variáveis livres x1, x2, ..., x$_n$ que são verdadeiras de uma sequência de elementos de uma L-estrutura ${\mathcal {M}}$. Dependendo do contexto, os tipos podem ser completos ou parciais e podem utilizar um conjunto fixo de constantes, A, da estrutura ${\mathcal {M}}$. A questão de quais tipos representam elementos reais de ${\mathcal {M}}$ nos leva às ideias de modelos saturados e tipos de omissão.

## Definição formal

Considere a estrutura ${\mathcal {M}}$ para uma linguagem L. Seja M o universo da estrutura. Para cada A ⊆ M, seja L(A) a linguagem obtida de L a partir da adição de uma constante c$_a$ para cada a ∈ A. Em outras palavras,
Um 1-tipo (de ${\mathcal {M}}$) sobre A é um conjunto de p(x) fórmulas em L(A) com, no máximo, uma variável livre x (portanto 1-tipo) de modo que para cada subconjunto finito p$_0$(x) ⊆ p(x) existe algum b ∈ M, dependendo do p$_0$(x), com ${\mathcal {M}}\models p_{0}(b)$ (isto é. todas as fórmulas em p$_0$(x) são verdadeiras em ${\mathcal {M}}$ quando x é substituído por b).
Similarmente, um n-tipo (de ${\mathcal {M}}$) sobre A é definido como sendo um conjunto de p(x$_1$,…,x$_n$) = p(x) de fórmulas em L(A), cada um tendo suas variáveis livres ocorrendo apenas entre as n variáveis livres dadas (x$_1$,…,x$_n$), desta forma, para cada subconjunto finito p$_0$(x) ⊆ p(x) existem alguns elementos b$_1$,…,b$_n$ ∈ M com ${\mathcal {M}}\models p_{0}(b_{1},\ldots ,b_{n})$.
Tipo completo refere-se aos tipos que são maximais com respeito a inclusão, isto é, se p(x) é um tipo completo, então para cada $\phi ({\boldsymbol {x}})\in L(A,{\boldsymbol {x}})$ e $\phi ({\boldsymbol {x}})\in p({\boldsymbol {x}})$ or $\lnot \phi ({\boldsymbol {x}})\in p({\boldsymbol {x}})$. Qualquer tipo não-completo é chamado de tipo parcial. Assim, a palavra tipo, em geral, refere-se a qualquer n-tipo, parcial ou completo, sobre qualquer conjunto de parâmetros escolhidos (até mesmo o conjunto vazio).
Um n-tipo p(x) é dito como sendo realizado em ${\mathcal {M}}$ se houver um elemento b ∈ M$^n$ de modo que ${\mathcal {M}}\models p({\boldsymbol {b}})$. A existência de uma tal realização é garantida, para qualquer tipo, através do Teorema da Compacidade, embora a realização possa acontecer em alguma extensão elementar de ${\mathcal {M}}$, ao invés de no próprio ${\mathcal {M}}$. Se um tipo completo é realizado por b em ${\mathcal {M}}$, então o tipo é designado como $tp_{n}^{\mathcal {M}}({\boldsymbol {b}}/A)$ e referido como o tipo completo de b sobre A.
Um tipo p(x) é dito isolado por φ se existir uma fórmula φ(x) com a propriedade que $\forall \psi ({\boldsymbol {x}})\in p({\boldsymbol {x}}),\varphi ({\boldsymbol {x}})\rightarrow \psi ({\boldsymbol {x}})$. Desde que subconjuntos finitos de um tipo sejam sempre realizados em ${\mathcal {M}}$, há sempre um elemento b ∈ M$^n$ de tal forma que φ(b) é verdadeira em ${\mathcal {M}}$; ou seja ${\mathcal {M}}\models \varphi ({\boldsymbol {b}})$, assim b realiza todo o tipo isolado. Então os tipos isolados serão realizados em cada subestrutura ou extensão elementar. Devido a isso, os tipos isolados nunca podem ser omitidos (veja abaixo).
Um modelo que realiza a máxima variedade possível de tipos é chamado de modelo saturado, e a construção ultrapoderosa fornece uma maneira de produzir modelos saturados.

## Exemplos de tipos

Considere a linguagem com um conectivo binário,ao qual nós chamamos de $\in$. Seja ${\mathcal {M}}$ o modelo $\langle \omega ,\in _{\omega }\rangle$, ao qual o $\omega$ é um valor ordinal padrão bem ordenado. Seja ${\mathcal {T}}$ a teoria deste modelo.
Considere o conjunto de fórmulas $p(x):=\{n\in \omega \mid n\in _{\omega }x\}$. Primeiro, nós dizemos que isso é um tipo. Seja $p_{0}(x)\subseteq p(x)$ um subconjunto finito de $p(x)$. Precisamos encontrar um $n\in \omega$ que satisfaça todas as fórmulas em $p_{0}$. Bem, podemos apenas pegar o sucessor do maior ordinal mencionado no conjunto de fórmulas $p_{0}(x)$. Então, isso claramente irá conter todos os ordinais mencionados em $p_{0}(x)$. Assim, teremos que $p(x)$ é um tipo. Em seguida, perceba que $p(x)$ não é realizado em ${\mathcal {M}}$. Pois, se fosse, existiria algum $n\in \omega$ que contém cada elemento de $\omega$. Se quiséssemos realizar o tipo,poderíamos ser tentados a considerar o modelo $\langle \omega +1,\in _{\omega +1}\rangle$,que é de fato uma supermodelo de ${\mathcal {M}}$ que compreende o tipo. Unfortunately, this extension is not elementary, isto é, esse modelo não tem ue satisfazer ${\mathcal {T}}$. Em particular, a semtemça $\exists x\forall y(y\in x)$ é satisfeita por este modelo e não por ${\mathcal {M}}$.
Então, desejamos realizar o tipo numa extensão elementar. Podemos fazer isso definindo uma nova estrutura nessa linguagem, ao qual chamamos de ${\mathcal {M}}'$. O domínio da estrutura será $\omega \cup \mathbb {Z} '$ onde $\mathbb {Z} '$ representa o conjunto de números inteiros de tal modo que$\mathbb {Z} '\cap \omega =\emptyset$. Seja $<$ a ordem habitual de $\mathbb {Z} '$. Interpretamos o simbolo $\in$ na nossa nova estrutura por $\in _{{\mathcal {M}}'}=\in _{\omega }\cup <\cup \,(\omega \times \mathbb {Z} ')$. A ideia é que estamos adicionando uma "cadeia-Z", ou cópia dos inteiros, acima de todos os ordinais finitos. Claramente qualquer elemento $\mathbb {Z} '$ realiza o tipo $p(x)$. Além disso, pode-se verificar que essa extensão é elementar.
Outro exemplo: o tipo completo do número 2 sobre o conjunto vazio, considerado como um membro dos números naturais, seria o conjunto de todas as sentenças de primeira ordem que descrevem uma variável x que são verdadeiras para x = 2. Esse conjunto incluiria fórmulas tais como $\,\!x\neq 1+1+1$, $x\leq 1+1+1+1+1$, e $\exists y(y<x)$. Esse é um exemplo de um tipo isolado,uma vez que a fórmula $x=1+1$ implica todas as outras fórmulas que são verdadeiras sobre o número 2.
Por exemplo, as sentenças
    $\forall y(y^{2}<2\implies y<x)$
e
    $\forall y((y>0\land y^{2}>2)\implies y>x)$
descrevendo a raiz quadrada de 2 são consistentes com os axiomas de campos ordenados, e pode ser estendida para um tipo completo. Esse tipo não é realizado no campo ordenado de números racionais, mas é realizado em campos ordenados de números reais. Similarmente, o conjunto infinito de fórmulas (sobre o conjunto vazio) {x>1, x>1+1, x>1+1+1, ...} não é realizado em campos ordenados de números reais, ,as é realizado em campo ordenado de hiperreais. Se permitirmos mais parâmetros, como por exemplo, todos os reais, podemos especificar um tipo $\{0<x<r:r\in \mathbb {R} \}$ que é realizado por um hiperreal infinitesimal que viola a Propriedade de Arquimedes.
A razão pela qual é útil restringir os parâmetros a um determinado subconjunto do modelo é que isso ajuda a distinguir os tipos que podem ser satisfeitos daqueles que não podem. Por exemplo, usando o conjunto completo de números reais como parâmetros poderia ser gerado um conjunto infinito e incontável de fórmulas como $x\neq 1$, $x\neq \pi$, ... que explicitamente, colocaria uma regra para cada possível valor real para x, e, portanto, nunca poderia ser realizado dentro dos números reais.

## Espaços de pedra

É útil para considerar o conjunto de n-tipos completos sobre A como um espaço topológico. Considere a seguinte relação de equivalência na fórmula nas variáveis livres x$_1$,…, x$_n$ com parâmetros em M:
    $\psi \equiv \phi \Leftrightarrow {\mathcal {M}}\models \forall x_{1},\ldots ,x_{n}(\psi (x_{1},\ldots ,x_{n})\leftrightarrow \phi (x_{1},\ldots ,x_{n})).$
Pode-se mostrar que $\psi \equiv \phi$ se, somente se eles são contidos, exatamente, nos mesmos tipos completos.
O conjunto de fórmulas nas varáveis livres x$_1$,…,x$_n$ sobre A até essa relação de equivalência é uma álgebra booleana (e é canonicamente isomorfa ao conjunto de subconjuntos A-definíveis de M$^n$). Os n-tipos completos correspondem ao ultrafiltro dessa álgebra booleana. O conjunto de n-tipos completos pode ser feito num espaço topológico, tendo os conjuntos de tipos que contém uma dada fórmula como conjuntos abertos de base. Isso constrói o Espaço de Pedra que é compacto, Hausdorff, e totalmente desconectado.
Exemplo. A teoria completa de campos algebricamente fechados de característica 0 tem eliminação de quantificador que permite mostrar que os possíveis 1-tipos completos correspondem a:
* Raízes de um dado polinômio não constante irredutível sobre os racionais com coeficiente de liderança igual a 1. Por exemplo, o tipo de raíz quadrada de 2. Cada um desses tipos são um ponto aberto de espaço de pedra.
* Elementos transcendentais, estes não são as raízes de qualquer polinômio diferente de zero. Esse tipo é um ponto no espaço de pedra que é fechado, mas não aberto.
Em outras palavras, os 1-tipos correspondem exatamente aos ideais primos do anel polinomial Q[x] sobre os racionais Q: Se r é um elemento do modelo do tipo p, então o ideal correspondente a p é o conjunto de polinomiais que possuem r como uma raiz. De modo mais geral, os n-tipos completos correspondem aos ideais primos do anel polinomial Q[x$_1$,...,x$_n$], em outras palavras, até os pontos do espectro principal deste anel. (A topologia do espaço de pedra pode, de fato, ser visualizada como a topologia de Zariski de um anel booleano induzido a um modo natural da estrutura de treliça de álgebra booleana, ao passo que a topologia de Zariski não é, em geral, de Hausdorff, isto é, no caso de anéis booleanos.) Por exemplo, se q(x,y) é um polinômio irredutível em 2 variáveis, existe um 2-tipo cuja realizações (informalmente) pares (x,y) de elementos transcendentais com q(x,y)=0.

## O teorema dos tipos omitidos

Dado um n-tipo completo p pode-se perguntar se existe um modelo da teoria que omite p, em outras palavras não existe n-tuplo no modelo que realiza p. Se p é um ponto isolado no Espaço de Pedra, isto é se {p} é um conjunto aberto, é fácil ver que todo modelo realiza p (ao menos se a teoria esta completa). O teorema dos tipos omitidos diz que inversamente, se p não é isolado, então existe um modelo contável omitindo p (desde que a linguagem seja contável).
Exemplo: Na teoria dos campos algebricamente fechados de característica 0, existe um 1-tipo representado por elementos que são transcendentais sobre o campo primo. Este é um ponto de não isolado do Espaço de Pedra (de fato, o único ponto não isolado). O campo de números algébricos é um modelo que omite esse tipo, bem como o encerramento de qualquer extensão algébrica transcendental dos racionais é um modelo de realização deste tipo.
Todos os outros tipos são "números algébricos" (mais precisamente, eles são os conjuntos de declarações de primeira ordem satisfeitas por algum dado número algébrico), e todos esses tipos são realizados em todos os campos algebricamente fechados de característica 0.