Type (théorie des modèles)

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher
Page d'aide sur l'homonymie 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.

Définition[modifier | modifier le code]

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 \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 L_A-structure N et b∈N et pour toute formule \phi de \Sigma, N |= \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 \alpha-types.

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

L'ensemble des n-types complets sur A est noté S_n(A), si A=∅ on note parfois S_n(T).

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

Exemples[modifier | modifier le code]

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 tp(a/A); la définition s'adapte pour des uples d'éléments de taille quelconque.

Topologie des espaces de types[modifier | modifier le code]

Pour tout entier non nul n, on munit S_n(A) d'une topologie: on la définit en prenant comme ouverts de base les parties <φ>:={p∈S_n(A) ; φ∈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 S_n(A).

Applications[modifier | modifier le code]

Les espaces de types permettent, dans un langage dénombrable, une caractérisation simple des théories \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 \aleph_0-catégorique si et seulement si pour tout entier n, S_n(T) est fini. Voir aussi Théorie k-catégorique.

Article connexe[modifier | modifier le code]

Théorie stable (en)