Type (théorie des modèles) — Wikipédia

Pour les articles homonymes, voir Type.

En théorie des modèles, un type est un ensemble de formules à une même variable libre, consistant avec une théorie donnée, c'est-à-dire tel qu'il existe un modèle de la théorie en question dont un élément satisfait chacune des formules du type.

Soit T une théorie dans un langage L, M un modèle de T et A ⊆ M un ensemble de paramètres. On appelle type (partiel) sur A tout ensemble ${\displaystyle \Sigma }$ de formules en (au plus) une même variable libre à paramètres dans A consistant avec Diag(A) (le diagramme complet de A), i.e. tel qu'il existe une ${\displaystyle L_{A}}$-structure N et b ∈ N et pour toute formule ${\displaystyle \phi }$ de ${\displaystyle \Sigma }$, N ⊨ ${\displaystyle \phi }$(b).

Plus généralement, pour un entier naturel non nul n, on définit de manière similaire les n-types (ensembles consistants de formules à variables libres parmi n variables fixées). On peut également étendre cette définition aux ordinaux quelconques, on parle de ${\displaystyle \alpha }$-types.

Toujours dans le même cadre, on désigne par type complet sur A un type ${\displaystyle \Sigma }$ tel que pour toute ${\displaystyle L_{A}}$-formule ${\displaystyle \phi }$ à au plus une variable libre, on a ${\displaystyle \Sigma \vdash \phi }$ (i.e. toute réalisation de ${\displaystyle \Sigma }$ réalise également ${\displaystyle \phi }$) ou bien ${\displaystyle \Sigma \vdash \lnot \phi }$.

L'ensemble des n-types complets sur A est noté ${\displaystyle S_{n}(A)}$, si A = ∅ on note parfois ${\displaystyle S_{n}(T)}$.

Les conventions varient selon les auteurs, et certains nomment type partiel ce que nous appelons type et type nos types complets.

Soit a ∈ M ⊨ T, A ⊆ M, on appelle type de a sur A l'ensemble des formules que M satisfait en a (cela comprend donc les formules closes). On voit sans peine qu'il s'agit d'un type complet, que l'on note ${\displaystyle tp(a/A)}$ ; la définition s'adapte pour des uples d'éléments de taille quelconque.

Pour tout entier non nul n, on munit ${\displaystyle S_{n}(A)}$ d'une topologie : on la définit en prenant comme ouverts de base les parties ${\displaystyle <\varphi >:=\{p\in S_{n}(A)\,;\,\varphi \in p\}}$.

On remarque que cette topologie est totalement discontinue : tout ouvert de base <φ> est également un fermé puisque son complémentaire est <¬φ>. D'autre part, le théorème de compacité entraine la compacité de l'espace ${\displaystyle S_{n}(A)}$.

Les espaces de types permettent, dans un langage dénombrable, une caractérisation simple des théories ${\displaystyle \aleph _{0}}$-catégoriques (en), qui ont exactement un modèle dénombrable (à isomorphisme près) : un théorème de Ryll-Nardzewski (en) affirme qu'une théorie T complète, dénombrable dont les modèles sont infinis est ${\displaystyle \aleph _{0}}$-catégorique si et seulement si pour tout entier n, ${\displaystyle S_{n}(T)}$ est fini. Voir aussi Théorie k-catégorique.

Théorie stable (en)

• Portail de la logique
• Portail des mathématiques