- Type (théorie des modèles)
-
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.
Sommaire
Définition
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 Σ 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 LA-structure N et b∈N et pour toute formule ϕ de Σ, N |= ϕ(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 α-types.
Toujours dans le même cadre, on désigne par type complet sur A un type Σ tel que pour toute LA-formule ϕ à au plus une variable libre, on a Σ | − ϕ (i.e. toute réalisation de Σ réalise également ϕ) ou bien Σ | − ¬ϕ
L'ensemble des n-types complets sur A est noté Sn(A), si A=∅ on note parfois Sn(T).
Les conventions varient selon les auteurs, et certains nomment type partiel ce que nous appelons type et type nos types complets.
Exemples
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
Pour tout entier non nul n, on munit Sn(A) d'une topologie: on la définit en prenant comme ouverts de base les parties <φ>:={p∈Sn(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 Sn(A).
Applications
Les espaces de types permettent, dans un langage dénombrable, une caractérisation simple des -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
-catégorique si et seulement si pour tout entier n, Sn(T) est fini. Voir aussi Théorie k-catégorique.Article connexe
Théorie stable (en)
Wikimedia Foundation. 2010.
