Mostrar código-fonte de Tipo (teoria do modelo)

{{sem notas|data=janeiro de 2016}}
Na [[Teoria dos modelos|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 de interpretação (lógica)|estrutura matemática]] podem se comportar. Mais precisamente, é um conjunto de fórmulas de [[Lógica de primeira ordem|primeira ordem]] em uma linguagem ''L'' com variáveis livres x1, x2, ..., ''x''<sub>''n''</sub> que são verdadeiras de uma sequência de elementos de uma ''L''-estrutura <math>\mathcal{M}</math>. Dependendo do contexto, os tipos podem ser '''completos '''ou '''parciais '''e podem utilizar um conjunto fixo de constantes, A, da estrutura <math>\mathcal{M}</math>. A questão de quais tipos representam elementos reais de <math>\mathcal{M}</math> nos leva às ideias de [[modelo saturado|modelos saturados]] e '''tipos de omissão'''.

== Definição formal ==
Considere a [[Estrutura de interpretação (lógica)|estrutura]] <math>\mathcal{M}</math> para uma [[Linguagem formal|linguagem]] ''L''. Seja M o [[Estrutura de interpretação (lógica)|universo]] da estrutura. Para cada ''A''&nbsp;⊆&nbsp;''M'', seja ''L''(''A'') a linguagem obtida  de ''L'' a partir da adição de uma constante ''c''<sub>''a''</sub> para cada ''a''&nbsp;∈&nbsp;''A''. Em outras palavras,

Um '''1-tipo (de <math>\mathcal{M}</math>) 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''<sub>0</sub>(''x'')&nbsp;⊆&nbsp;''p''(''x'') existe algum ''b''&nbsp;∈&nbsp;''M'', dependendo do ''p''<sub>0</sub>(''x''), com <math> \mathcal{M} \models p_0(b) </math> (isto é. todas as fórmulas em ''p''<sub>0</sub>(''x'') são verdadeiras em <math>\mathcal{M}</math> quando ''x'' é substituído por  ''b'').

Similarmente, um '''''n''-tipo (de <math>\mathcal{M}</math>) sobre''' ''A'' é definido como sendo um conjunto de ''p''(''x''<sub>1</sub>,…,''x''<sub>''n''</sub>) = ''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''<sub>1</sub>,…,''x''<sub>''n''</sub>), desta forma, para cada subconjunto finito ''p''<sub>0</sub>('''''x''''') ⊆ ''p''('''''x''''') existem alguns elementos ''b''<sub>1</sub>,…,''b''<sub>''n''</sub> ∈ ''M'' com <math>\mathcal{M}\models p_0(b_1,\ldots,b_n)</math>.

'''Tipo completo''' refere-se aos tipos que são [[Teoria completa|maximais]] com respeito a inclusão, isto é, se ''p''('''''x''''') é um tipo completo, então para cada <math>\phi(\boldsymbol{x}) \in L(A,\boldsymbol{x})</math> e <math> \phi(\boldsymbol{x}) \in p(\boldsymbol{x})</math>  or  <math>\lnot\phi(\boldsymbol{x}) \in p(\boldsymbol{x})</math>. 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 <span id="realizationOfTypes" contenteditable="false"></span>'''realizado em <math>\mathcal{M}</math>''' se houver um elemento '''''b'''''&nbsp;∈&nbsp;''M''<sup>''n''</sup> de modo que <math>\mathcal{M}\models p(\boldsymbol{b})</math>. A existência de uma tal realização é garantida, para qualquer tipo, através do [[Teorema da compacidade|Teorema da Compacidade]], embora a realização possa acontecer em alguma [[Equivalência elementar|extensão elementar]] de <math>\mathcal{M}</math>, ao invés de no próprio <math>\mathcal{M}</math>. Se um tipo completo é realizado por '''''b''''' em <math>\mathcal{M}</math>, então o tipo é designado como <math>tp_n^{\mathcal{M}}(\boldsymbol{b}/A)</math> e referido como '''o tipo completo de ''b'' sobre''' ''A''.

<span>Um tipo </span>''p''('''''x''''') é dito '''isolado por ''φ''''' se existir uma fórmula ''φ''('''''x''''') com a propriedade que <math>\forall \psi(\boldsymbol{x}) \in p(\boldsymbol{x}), \varphi(\boldsymbol{x}) \rightarrow \psi(\boldsymbol{x})</math>. Desde que subconjuntos finitos de um tipo sejam sempre realizados em <math>\mathcal{M}</math>, há sempre um elemento '''''b'''''&nbsp;∈&nbsp;''M''<sup>''n''</sup> de tal forma que ''φ''('''''b''''') é verdadeira em <math>\mathcal{M}</math>; ou seja <math>\mathcal{M} \models \varphi(\boldsymbol{b})</math>, 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 [[Saturated model|modelo saturado]], e a construção [[Ultraproduct|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 <math>\in</math>. Seja <math>\mathcal{M}</math> o modelo <math>\langle \omega, \in_{\omega}\rangle</math>, ao qual o <math>\omega</math> é um valor ordinal padrão bem ordenado. Seja <math>\mathcal{T}</math> a teoria deste modelo.

Considere o conjunto de fórmulas <math>p(x):=\{ n \in \omega \mid n\in_{\omega} x \} </math>. Primeiro, nós  dizemos que isso é um tipo. Seja <math>p_0(x)\subseteq p(x)</math> um subconjunto finito de  <math>p(x)</math>. Precisamos encontrar um <math>n\in\omega</math> que satisfaça todas as fórmulas em <math>p_0</math>. Bem, podemos apenas pegar o sucessor do maior ordinal mencionado no conjunto de fórmulas <math>p_0(x)</math>. Então, isso claramente irá conter todos os ordinais mencionados em <math>p_0(x)</math>. Assim, teremos que <math>p(x)</math>  é um tipo. Em seguida, perceba que <math>p(x)</math> não é realizado em <math>\mathcal{M}</math>. Pois, se fosse, existiria algum <math>n\in\omega</math> que contém cada elemento de <math>\omega</math>. Se quiséssemos realizar o tipo,poderíamos ser tentados a considerar o modelo <math>\langle \omega+1,\in_{\omega+1}\rangle</math>,que é de fato uma [[supermodelo]] de <math>\mathcal{M}</math> que compreende o tipo. Unfortunately, this extension is not elementary, isto é, esse modelo não tem ue satisfazer <math>\mathcal{T}</math>. Em particular, a semtemça <math>\exists x \forall y (y\in x)</math> é satisfeita por este modelo e não por <math>\mathcal{M}</math>.

Então, desejamos realizar o tipo numa extensão elementar. Podemos fazer isso definindo uma nova estrutura nessa linguagem, ao qual chamamos de <math>\mathcal{M}'</math>. O domínio da estrutura será <math>\omega \cup \mathbb{Z}'</math> onde <math>\mathbb{Z}'</math> representa o conjunto de números inteiros de tal modo que<math>\mathbb{Z}'\cap\omega=\emptyset</math>. Seja <math><</math> a ordem habitual de <math>\mathbb{Z}'</math>. Interpretamos o simbolo <math>\in</math> na nossa nova estrutura por <math>\in_{\mathcal{M}'} = \in_{\omega} \cup < \cup \,(\omega \times \mathbb{Z}')</math>. A ideia é que estamos adicionando uma "cadeia-Z", ou cópia dos inteiros, acima de todos os ordinais finitos. Claramente qualquer elemento <math>\mathbb{Z}'</math> realiza o tipo <math>p(x)</math>. 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''&nbsp;=&nbsp;2. Esse conjunto incluiria fórmulas tais como  <math>\,\!x\ne 1+1+1</math>, <math>x\le 1+1+1+1+1</math>, e <math>\exists y(y<x)</math>. Esse é um exemplo  de um tipo isolado,uma vez que a fórmula <math>x = 1+1</math> implica todas as outras fórmulas que são verdadeiras sobre o número 2.

Por exemplo, as sentenças
: <math>\forall y(y^2<2 \implies y<x)</math>
e
: <math>\forall y((y>0 \land y^2>2) \implies y>x)</math>
descrevendo a [[Raiz quadrada de dois|raiz quadrada de 2]]  são consistentes com os axiomas de [[Corpo ordenado|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 [[Número hiper-real|hiperreais]]. Se permitirmos mais parâmetros, como por exemplo, todos os reais, podemos especificar um tipo <math>\{ 0 < x < r : r \in \mathbb{R} \}</math> que é realizado por um hiperreal [[infinitesimal]] que viola a [[Propriedade arquimediana|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 <math>x\ne 1</math>, <math>x\ne \pi</math>, ... 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''<sub>1</sub>,&#x2026;, ''x''<sub>''n''</sub> com parâmetros em ''M'':
: <math>\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)).</math>
Pode-se mostrar que <math>\psi \equiv \phi</math> se, somente se eles são contidos, exatamente, nos mesmos tipos completos.

O conjunto de fórmulas nas varáveis livres ''x''<sub>1</sub>,&#x2026;,''x''<sub>''n''</sub> sobre ''A'' até essa relação de equivalência é uma [[Álgebra booleana (estrutura)|álgebra booleana]] (e é canonicamente isomorfa ao conjunto de subconjuntos ''A''-definíveis de ''M''<sup>''n''</sup>). 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 é [[Espaço compacto|compacto]], [[Espaço de Hausdorff|Hausdorff]], e [[Totally disconnected space|totalmente desconectado]].

'''Exemplo'''. A teoria completa de [[Corpo algebricamente fechado|campos algebricamente fechados]] de característica 0 tem [[Eliminação de Quantificadores|eliminação de quantificador]] que permite mostrar que os possíveis 1-tipos completos correspondem a:
* [[Raiz (matemática)|Raízes]] de um dado [[Polinômio irredutível|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''<sub>1</sub>,...,''x''<sub>n</sub>], em outras palavras, até os pontos do [[Espectro de um anel|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.

== Referências ==
* Hodges, Wilfrid (1997). ''A shorter model theory''. [[Cambridge University Press]]. [[International Standard Book Number|ISBN]]&nbsp;0-521-58713-1.
* Chang, C.C.; [[Howard Jerome Keisler|Keisler, H. Jerome]] (1989). ''Model Theory'' (third ed.). [[Elsevier]]. [[International Standard Book Number|ISBN]] 0-7204-0692-7.
* Marker, David (2002). ''Model Theory: An Introduction''. [[Graduate Texts in Mathematics]] 217. Springer. [[International Standard Book Number|ISBN]] 0-387-98760-6.

{{Portal3|Matemática}}
{{Controle de autoridade}}

[[Categoria:Teoria dos modelos]]