La théorie des modèles est une branche de la logique mathématique qui traite de la construction et de la classification des structures. Elle définit en particulier les modèles des théories axiomatiques, l'objectif étant d'interpréter les structures syntaxiques (termes, formules, démonstrations...) dans des structures mathématiques (ensemble des entiers naturels, groupes, univers...) de façon à leur associer des concepts de nature sémantique (comme le sens ou la vérité).

L'idée d'interprétation de théories mathématiques dans des structures apparaît assez tôt, dès le XVII^e siècle. Ainsi l'abbé Buée^[1] et Jean-Robert Argand, puis Gauss et Cauchy donnent un modèle géométrique dans lequel les nombres complexes, objets certes commodes pour les calculs mais à l'époque sans signification, sont interprétés comme des points du plan euclidien (le plan complexe est parfois nommé plan d'Argand) et leurs opérations comme des transformations géométriques. Mais c'est sans doute l'apparition des géométries non euclidiennes qui fut la plus déterminante dans l'émergence de l'idée de modèle. D'abord fondées sur des variantes du postulat des parallèles d'Euclide, elles apparaissaient comme un simple jeu formel et n'avaient que peu de crédit face au statut de vérité absolue de la géométrie euclidienne. Elles ont peu à peu été acceptées à partir du moment où l'on a pu en donner des modèles, c'est-à-dire des supports géométriques avec des interprétations spécifiques pour les concepts formels de points, de droites, etc. Les modèles ont permis d’interpréter la géométrie non euclidienne dans la géométrie euclidienne. Ainsi Poincaré donne un modèle du plan hyperbolique à partir d'un demi-plan du plan complexe. Plus tard, Hilbert fera une conférence à Paris où il donnera une signification numérique à tous les termes de la géométrie euclidienne dans le but de démontrer l’indépendance des axiomes de la géométrie euclidienne vis-à-vis des autres axiomes^{[réf. nécessaire]}.

Deux des pionniers de la théorie des modèles sont Leopold Löwenheim et Thoralf Skolem qui démontrent un puissant théorème d'existence de modèles de toutes « tailles » (cardinaux), énoncé en 1915 par le premier et démontré par le second en 1920.

En 1933, une étape importante de l'histoire de cette théorie est franchie avec la définition de la vérité par Alfred Tarski, dans un article intitulé Le concept de vérité dans les langages formalisés^[2]. Le but de Tarski est de donner une définition de la vérité en accord avec le langage courant et de préciser la théorie de la correspondance. Pour que les antinomies logiques soient évitées, il propose de définir le "vrai" et le "faux" dans un méta-langage. Par exemple, il distingue la proposition "il neige" de l'observation du fait qu'il neige effectivement dans le monde réel. Pour cela, Tarski introduit le concept de satisfaisabilité, au sens que la proposition "il neige" est satisfaite par la réalité (en tant que « modèle » de la formule) seulement dans le cas où il neige. L'objectif de cet exemple est de montrer la différence entre l'objet linguistique et son interprétation qui permet de juger la proposition. Pour ce faire, il introduit l'étude formelle de la sémantique du calcul des prédicats.

Il a cependant fallu attendre les années 1950 et 60 pour que la théorie des modèles devienne une discipline à part entière. Parmi ses pionniers figurent Tarski, R. L. Vaught et M. Morley. Aujourd'hui, la théorie des modèles est l'une des branches les plus importantes de la logique.

Un langage ${\displaystyle L}$ est un ensemble de constantes, de fonctions, de prédicats et de variables. L'objet de recherche dans la théorie des modèles sont des théories, donc des ensembles de formules. Un modèle est une structure sur ${\displaystyle L}$, qui satisfait les axiomes de la théorie en question.

Il y a deux approches de recherche principales dans la théorie des modèles:

1) La compréhension d'une structure singulière, qu'on considère comme donnant la signification [par exemple ${\displaystyle (\mathbb {N} ,+,*)}$ ou ${\displaystyle (\mathbb {R} ,+,*)}$].

2) L'enquête pour trouver des caractéristiques communes à un nombre de structures [par exemple des structures algébriques comme un anneau ou un corps].

Parmi les théorèmes importants en théorie des modèles, trois jouent un rôle principal, car ils donnent les conditions générales pour qu'une théorie ait un modèle :

(i) Le théorème de compacité pour la logique du premier ordre, (les formulations 1 et 2 sont équivalentes) :

1) Soit ${\displaystyle X\models \varphi }$; ${\displaystyle \varphi }$ est une formule. Il existe un ensemble fini ${\displaystyle X_{\text{fin}}\subseteq X}$ tel que ${\displaystyle X_{\text{fin}}\models \varphi }$.

2) Si toute partie finie d'un ensemble de formules Γ a un modèle, alors Γ a un modèle.

(ii) Le théorème de complétude de Gödel assure qu'en logique classique du premier ordre, la réciproque est vraie : toute théorie non contradictoire possède au moins un modèle. Il clôt des recherches qui remontent au théorème de Löwenheim-Skolem (iii), qui énonce que toute théorie, dans un langage dénombrable du premier ordre, qui possède un modèle infini, possède aussi un modèle de n'importe quelle cardinalité infinie.

En calcul propositionnel de la logique classique, il n'y a pas de quantificateurs existentiels ou universels. Les formules sont constituées de propositions atomiques reliées itérativement par des connecteurs logiques. Un modèle consiste à définir, pour chaque variable propositionnelle atomique, une valeur de vérité (vraie ou fausse). On peut alors en déduire la vérité ou la fausseté de toute formule complexe.

La complexité d'une formule est mesurée par le nombre maximal d’opérateurs emboîtés. Par exemple dans ${\displaystyle (\lnot P)\lor (Q\land R)}$, le ou ${\displaystyle \lor }$ et le non ${\displaystyle \lnot }$ sont emboîtés l’un dans l’autre. Mais le non et le et ${\displaystyle \land }$ ne le sont pas. Cette proposition est de complexité 2 parce qu’elle a au maximum deux opérateurs emboîtés.

Les formules de complexité 0 sont les formules atomiques. C'est le modèle choisi qui définit leur valeur de vérité.

Supposons que la vérité et la fausseté de toutes les formules de complexité ${\displaystyle n}$ ait été définie. Montrons comment définir la vérité et la fausseté des formules de complexité ${\displaystyle n+1}$. Soit ${\displaystyle P}$ une formule de complexité ${\displaystyle n+1}$, obtenue à partir de la formule ou des formules ${\displaystyle Q}$ et ${\displaystyle R}$ de complexité ${\displaystyle n}$ ou inférieure, au moyen d'un connecteur logique. La vérité ou la fausseté de ${\displaystyle Q}$ et ${\displaystyle R}$ est donc déjà définie.

a) ${\displaystyle P=\lnot Q}$ : Si ${\displaystyle Q}$ est vrai alors ${\displaystyle P}$ est faux, par définition de la négation. Si ${\displaystyle Q}$ est faux alors ${\displaystyle P}$ est vrai, pour la même raison.

b) ${\displaystyle P=(Q\land R)}$ : Si ${\displaystyle Q}$ et ${\displaystyle R}$ sont tous les deux vrais alors ${\displaystyle P}$ aussi, mais ${\displaystyle P}$ est faux dans tous les autres cas.

c) ${\displaystyle P=(Q\lor R)}$ : Si ${\displaystyle Q}$ et ${\displaystyle R}$ sont tous les deux faux alors ${\displaystyle P}$ aussi, mais ${\displaystyle P}$ est vrai dans tous les autres cas.

d) ${\displaystyle P=(Q\to R)}$ : Si ${\displaystyle Q}$ est vrai et ${\displaystyle R}$ est faux alors ${\displaystyle P}$ est faux, mais ${\displaystyle P}$ est vrai dans tous les autres cas.

Une formule vraie dans tout modèle est dite universellement valide (en particulier, une tautologie en est une). Si la formule possède ${\displaystyle n}$ variables propositionnelles atomiques, il suffit en fait de vérifier la vérité de la formule dans les ${\displaystyle 2^{n}}$ modèles possibles donnant les diverses valeurs de vérité aux ${\displaystyle n}$ propositions atomiques pour prouver que cette formule est une tautologie. Le nombre de modèles étant fini, il en résulte que le calcul des propositions est décidable : il existe un algorithme permettant de décider si une formule est une tautologie ou non.

Par ailleurs, le théorème de complétude du calcul des propositions établit l'équivalence entre être une tautologie et être prouvable dans un système de déduction adéquat.

Montrons que ${\displaystyle ((P\to Q)\to P)\to P}$ (loi de Peirce) est une tautologie, en utilisant la règle d). Si ${\displaystyle P}$ est vraie, alors ${\displaystyle ((P\to Q)\to P)\to P}$ étant de la forme ${\displaystyle R\to P}$ est vraie. Si ${\displaystyle P}$ est faux, alors ${\displaystyle P\to Q}$ est vrai, ${\displaystyle (P\to Q)\to P}$ est faux, et ${\displaystyle ((P\to Q)\to P)\to P}$ est vrai.

Étant vrai dans tout modèle, ${\displaystyle ((P\to Q)\to P)\to P}$ est une tautologie. Elle est donc également prouvable au moyen de systèmes de déduction, par exemple la déduction naturelle.

Par contre, ${\displaystyle (P\to Q)\to P}$ n'est pas prouvable. En effet, dans un modèle où ${\displaystyle P}$ est faux, ${\displaystyle (P\to Q)\to P}$ est également faux.

Dans le calcul des prédicats du premier ordre de la logique classique, les prédicats utilisés s'appliquent sur des variables. Pour définir un modèle, il convient donc d'introduire un ensemble dont les éléments serviront de valeurs à attribuer aux variables. Comme pour le calcul propositionnel, on commence par définir la vérité ou la fausseté des formules atomiques dans un domaine donné, avant de définir de proche en proche la vérité ou la fausseté des formules composées. On peut ainsi définir par étapes successives la vérité de toutes les formules complexes de la logique du premier ordre composées à partir des symboles fondamentaux d’une théorie.

Pour qu'un énoncé utilisant un ensemble de symbole défini par un langage ${\displaystyle {\mathcal {L}}}$ soit considéré comme vrai, c'est-à-dire qu'on puisse dire qu'il soit un théorème, il faut et il suffit que toutes les ${\displaystyle {\mathcal {L}}}$-structures satisfassent l'énoncé.

Une formule est atomique lorsqu’elle ne contient pas d’opérateurs logiques (négation, conjonction, existentiation…). Atomique ne veut pas dire ici qu’une formule ne contient qu’un seul symbole mais seulement qu’elle contient un seul symbole de prédicat fondamental. Les autres noms qu’elle contient sont des noms d’objet et ils peuvent être très complexes. Qu’une formule est atomique veut dire qu’elle ne contient pas de sous-formule. Il s’agit d’une atomicité logique.

Une interprétation d'un langage du premier ordre est une structure, définie par les éléments suivants.

• Un ensemble U non vide, l’univers de la théorie. À chaque nom d’objet (constante) mentionné dans le langage est associé un élément de U.
• À chaque prédicat unaire (à une place) fondamental mentionné dans le langage est associé une partie de U, l’extension de ce prédicat. C'est l'ensemble des valeurs pour lequel on décide que le prédicat est vrai. À chaque prédicat binaire fondamental mentionné dans le langage est associé une partie du produit cartésien U × U, c’est l’ensemble de tous les couples pour lesquels le prédicat est vrai. De même pour les prédicats ternaires, ou d’arité supérieure.
• À chaque opérateur unaire mentionné dans le langage est associé une fonction de U dans U. À chaque opérateur binaire mentionné dans le langage est associé une fonction de U × U dans U. De même pour les opérateurs d’arité supérieure.

L’ensemble U, ou l’interprétation dont il fait partie, est un modèle d’une théorie lorsque tous les axiomes de cette théorie sont vrais relativement à cette interprétation.

L'usage du mot, modèle, est parfois multiple. Tantôt il désigne l'ensemble U, tantôt l'ensemble des formules atomiques vraies, tantôt l'interprétation. Souvent, quand on dit un modèle d'une théorie, on suppose automatiquement qu'elle y est vraie. Mais on dit aussi qu'une théorie est fausse dans un modèle.

Dès qu’on a une interprétation d’une théorie, la véracité de toutes les formules qui mentionnent seulement les constantes, les prédicats et les opérateurs fondamentaux, peut être définie. On commence par les formules atomiques et on procède récursivement aux formules plus complexes.

On reprend les règles définies dans le paragraphe relatif aux modèles du calcul propositionnel, et on définit les deux règles supplémentaires, relatives au quantificateur universel et existentiel.

e) ${\displaystyle P=\forall x\;Q}$ : Si l'une des formules obtenues en substituant un élément de U à toutes les occurrences libres de ${\displaystyle x}$ dans l'interprétation de ${\displaystyle Q}$ est fausse alors ${\displaystyle P}$ est fausse, sinon, si ${\displaystyle Q}$ n'a pas d'autres variables libres que ${\displaystyle x}$, ${\displaystyle P}$ est vraie.

f) ${\displaystyle P=\exists x\;Q}$ : Si l'une des formules obtenues en substituant un élément de U à toutes les occurrences libres de ${\displaystyle x}$ dans l'interprétation de ${\displaystyle Q}$ est vraie alors ${\displaystyle P}$ est vraie, sinon, si ${\displaystyle Q}$ n'a pas d'autre variables libres que ${\displaystyle x}$, ${\displaystyle P}$ est fausse.

e) et f) permettent de définir la véracité et la fausseté de toutes les formules closes, c’est-à-dire sans variables libres.

La véracité et la fausseté de toutes les formules complexes, sans variables libres, de la logique du premier ordre, peut donc être déterminée dans un modèle donné.

Une formule vraie dans tout modèle s'appelle loi logique ou théorème. Comme pour le calcul propositionnel, le théorème de complétude de Gödel énonce l'équivalence entre loi logique et formule prouvable dans un système de déduction adéquat. Ce résultat est remarquable, compte tenu du fait que, contrairement au calcul des propositions, le nombre de modèles pouvant être envisagé est en général infini. D'ailleurs, contrairement au calcul des propositions, le calcul des prédicats n'est pas décidable.

La formule ${\displaystyle \exists x\;\forall y\;(R(x)\to R(y))}$ est une loi logique. En effet, considérons un modèle U non vide. Il y a alors deux possibilités.

• Ou bien on attribue la valeur vraie à R(y) lorsque y se voit attribuer une valeur quelconque dans U, et dans ce cas, on attribue à x une valeur quelconque dans U. L'implication ${\displaystyle R(x)\to R(y)}$ est alors vraie pour tous les y dans U, donc ${\displaystyle \forall y\;(R(x)\to R(y))}$ est également vraie dans U, et x désignant également un élément de U, ${\displaystyle \exists x\;\forall y\;(R(x)\to R(y))}$ est vraie dans U.
• Ou bien on attribue la valeur faux à R(y) pour au moins un y dans U. Désignons alors par x cet élément. Alors pour tout y de U, ${\displaystyle R(x)\to R(y)}$ est vraie, donc ${\displaystyle \forall y\;(R(x)\to R(y))}$ est vraie dans U, et donc ${\displaystyle \exists x\;\forall y\;(R(x)\to R(y))}$ est également vraie.

Dans les deux cas, la formule est vraie. U étant quelconque, la formule est vraie dans tout modèle, et peut également être prouvée au moyen d'un système de déduction.

Par contre, la formule ${\displaystyle \exists x(P\to Q(x))\to (P\to \forall xQ(x))}$ n'est pas prouvable. Il suffit de prendre comme modèle un ensemble U à deux éléments a et b, à poser P et Q(a) vraies, et Q(b) faux. ${\displaystyle P\to \forall xQ(x)}$ est faux dans U, alors que ${\displaystyle \exists x(P\to Q(x))}$ est vraie (avec x = a). Il en résulte que ${\displaystyle \exists x(P\to Q(x))\to (P\to \forall xQ(x))}$ est fausse dans U. La formule étant falsifiable n'est pas un théorème.

On dit d'une théorie qu'elle est catégorique si tous ses modèles sont isomorphes (deux modèles 𝔐 et 𝔐' sont isomorphes s'il existe un homomorphisme bijectif de M dans M'). Une théorie catégorique caractériserait donc véritablement la structure dont elle énonce les lois. Mais les théories du premier ordre ne peuvent être catégoriques dès qu'elles ont un modèle infini d'après le théorème de compacité, plus précisément d'après les théorèmes de Lowenheim-Skolem. Une théorie du premier ordre qui a des modèles infinis peut être cependant complète, c'est-à-dire que tous ses modèles satisfont les mêmes énoncés. Par exemple la théorie des ordres totaux denses sans extrémités, qui est une théorie complète, a pour modèles (ℚ, <) et (ℝ, <), qui ont les mêmes théorèmes (énoncés dans le seul langage de l'ordre !), sans être isomorphes, puisqu'ils ne sont même pas équipotents.

Les seules théories du premier ordre catégoriques sont des théories qui n'ont que des modèles d'une cardinalité finie donnée (la condition n'est bien-sûr pas suffisante).

Une notion qui est, elle, plus pertinente pour les théories du premier ordre est celle de κ-catégoricité, pour un certain cardinal infini κ : une théorie est dite κ-catégorique quand tous ses modèles de cardinal infini κ (au sens de la cardinalité du domaine) sont isomorphes. Par exemple, on peut démontrer que la théorie des ordres linéaires denses sans extrémités est ℵ₀-catégorique : tous ses modèles de cardinalité dénombrable sont isomorphes à (ℚ, <).

L'arithmétique de Peano axiomatisée au premier ordre, n'est pas ℵ₀-catégorique : elle possède des modèles dit non standards, qui ne sont pas isomorphes au modèle standard des entiers naturels, mais peuvent être dénombrables.

On peut considérer que l'arithmétique du second ordre est catégorique seulement si on ne considère que les modèles pleins : une classe de modèles que l'on ne peut caractériser axiomatiquement de façon satisfaisante.^[pas clair] Si cette théorie permet de caractériser les entiers naturels, c'est relativement par exemple à la théorie des ensembles (c'est-à-dire à un modèle de celle-ci). Pour la sémantique de Henkin, qui admet des théorèmes de complétude et de compacité, l'arithmétique du second ordre, comme toutes les théories du second ordre, n'est pas catégorique.

Soit K une classe non vide de L-structures. Peut-on caractériser K par un ensemble d’énoncés ?

- On dit qu’une classe de L-structures est EC (elementary class) s’il existe un ensemble fini Γ d’énoncés tel que K = Mod (Γ) (cela veut dire que toutes les classes de L-structures dans K sont exactement tous les modèles de Γ)

- On dit qu’une classe de L-structures est EC_Δ (elementary class in the wider sense) s’il existe un ensemble Γ d’énoncés (pas nécessairement fini) tel que K=Mod(Γ)

Une classe EC est donc aussi EC_Δ.

En tentant de caractériser les classes de L-structures finies (ie. dont l’univers contient un nombre fini d’éléments), on découvre les limites du pouvoir expressif de la logique du premier ordre: il est impossible, au premier ordre, de caractériser le fini. Voici la démonstration :

(Pour la démonstration, le théorème suivant est nécessaire : si un ensemble d’énoncés a des modèles finis de taille arbitrairement grande (c’est-à-dire que pour tout n, il existe un modèle dont l’univers a au moins n éléments), alors il a un modèle infini). Soit K_f la classe des L-structures finies. Supposons que K_f est EC_Δ. Donc il existe Γ un ensemble d’énoncés tel que K_f = Mod(Γ). Ainsi Γ a des modèles de taille finie arbitrairement grandes (car K_f contient toutes les classes de L-structures dont le domaine est fini) donc, par le théorème, Γ a un modèle infini. Contradiction, car par hypothèse, Mod(Γ) est la classe de toutes les L-structures finies. Donc K_f n’est pas EC_Δ , donc à fortiori pas EC.

Les modèles présentés jusqu'ici sont des modèles de la logique classique. Mais il existe d'autres logiques, par exemple la logique intuitionniste qui est une logique qui construit les démonstrations à partir des prémisses. Il existe pour cette logique une théorie des modèles, les modèles de Kripke avec un théorème de complétude : une formule est démontrable en logique intuitionniste si et seulement si elle est vraie dans tout modèle de Kripke.

Ces modèles permettent par exemple de répondre aux questions suivantes. Soit ${\displaystyle F}$ une formule close :

• Ou bien ${\displaystyle F}$ n'est pas un théorème de la logique classique. Pour le montrer, il suffit d'exhiber un modèle classique qui invalide la formule ;
• Ou bien ${\displaystyle F}$ est un théorème de la logique classique. Pour le montrer, il suffit d'en donner une démonstration dans un système de déduction de la logique classique. Il y a alors deux sous-cas :

Ou bien ${\displaystyle F}$ est également un théorème de la logique intuitionniste. Pour le montrer, il suffit d'en donner une démonstration dans un système de déduction intuitionniste (ou de montrer que ${\displaystyle F}$ est vraie dans tous les modèles de Kripke) ;

Ou bien ${\displaystyle F}$ n'est pas démontrable en logique intuitionniste. Pour le montrer, il suffit de donner un modèle de Kripke invalidant la formule.

C'est ainsi qu'on peut démontrer que :

${\displaystyle (\lnot \forall x\;F(x))\to (\exists x\;\lnot F(x))}$ est un théorème dans la logique classique, mais pas de la logique intuitionniste ;

${\displaystyle (\lnot \exists x\;F(x))\to (\forall x\;\lnot F(x))}$ est un théorème dans la logique intuitionniste (et également de la logique classique).

Les modèles de Kripke servent aussi à donner des modèles pour les logiques modales.

Nous avons déjà donné des applications des modèles :

• satisfaire ou au contraire falsifier une formule (par exemple distinguer formule vraie en logique classique mais fausse en logique intuitionniste : la formule est vraie dans tout modèle classique, mais il existe un modèle en logique intuitionniste qui la falsifie) ;
• prouver qu'une théorie ou un système d'axiomes n'est pas contradictoire en exhibant un modèle satisfaisant tous les axiomes.

En ce qui concerne les systèmes d'axiomes, les modèles interviennent également pour montrer l'indépendance des axiomes entre eux, ou établir la non-contradiction d'un système axiomatique en s'appuyant sur la non-contradiction d'un autre système (on parle alors de « consistance relative »). Donnons quelques exemples.

En géométrie, le V^e postulat d'Euclide est indépendant des autres axiomes de la géométrie. En effet, d'une part, le plan de la géométrie euclidienne est un modèle dans lequel ce postulat est vrai. D'autre part, le demi-plan de Poincaré est un modèle de la géométrie hyperbolique dans lequel ce postulat est faux. Dans ce modèle, l'univers (le plan hyperbolique) est constitué des points du demi-plan euclidien ouvert supérieur ${\displaystyle \{(x,y)\;|\;y>0\}}$. Les droites du plan hyperbolique sont les ensembles d'équation ${\displaystyle x=a}$ ou ${\displaystyle (x-a)^{2}+y^{2}=R^{2}}$.

Dans cet univers, si on se donne une droite et un point extérieur à cette droite, il existe une infinité de droites passant par le point et non sécantes à la première droite.

Dans cet exemple, on voit qu'on peut construire un modèle de la nouvelle théorie (le plan hyperbolique et ses droites) en se servant d'un modèle de l'ancienne (dans le plan euclidien : le demi-plan et ses demi-droites et demi-cercles). Si on suppose la « cohérence » ou « consistance » de la géométrie euclidienne, alors on a établi celle de la géométrie hyperbolique.

Cette utilisation de modèles pour montrer la consistance relative d'une théorie est très fréquente. Considérons par exemple la théorie des ensembles, notée ZF. Considérons par ailleurs la théorie, notée ZFC, constituée de ZF à laquelle on ajoute l'axiome du choix. On peut montrer que si ZF est non contradictoire alors ZFC aussi. En effet (grâce au théorème de complétude de Gödel) on suppose qu'il existe un modèle de ZF. On est alors capable, dans ce modèle, d'associer à tout ordinal α un ensemble F_α de façon que :

• la classe L « réunion » de tous les F_α vérifie tous les axiomes de ZF ;
• les F_α sont constructibles par récurrence transfinie, dans le sens où F_α est défini à partir des F_β, pour β < α ;
• si l'on définit l'ordre d'un y de L comme étant le plus petit ordinal α tel que y appartienne à F_α, alors, à tout x non vide de L « on peut associer » un élément de x d'ordre minimal, que l'on note f(x).

On a alors défini une « fonction » f de L dans L (ou plus exactement, une classe fonctionnelle) vérifiant ${\displaystyle \forall x\neq \varnothing ,f(x)\in x}$. Autrement dit, f est une « fonction de choix » dans L, si bien que L vérifie non seulement ZF mais aussi l'axiome du choix. L est donc un modèle de ZFC.

Toujours dans un modèle de ZF, si l'on pose ${\displaystyle R_{0}=\varnothing }$ et pour tout entier ${\displaystyle n}$, ${\displaystyle R_{n+1}={\mathcal {P}}(R_{n})}$ (ensemble des parties de ${\displaystyle R_{n}}$), alors la réunion des ${\displaystyle R_{n}}$ pour tout ${\displaystyle n}$ entier définit un modèle qui vérifie tous les axiomes de ZF sauf l'axiome de l'infini. Ceci prouve (toujours sous l'hypothèse que ZF est non contradictoire) que ce dernier axiome ne peut être dérivé des autres axiomes.

L'un des objectifs de la théorie des modèles est de proposer une caractérisation et une classification des théories, en particulier des théories mathématiques, sur la base des propriétés que possèdent leurs modèles (pour reprendre la formule de Shelah, le programme général est de construire une « classification theory »^[3]).

La stabilité^[4],[5] est à cet égard une propriété significative (pour les prolégomènes et le développement de la théorie de la stabilité, se rapporter notamment aux travaux de Morley et de Shelah). En particulier, pour les théories complètes dans un langage dénombrable, on peut s'intéresser à la propriété d'être ${\displaystyle \omega }$-stable (on lit « oméga-stable »).

Nous devons au préalable introduire certaines notions. On appelle un 1-type un ensemble de formules ${\displaystyle \Sigma (v)}$ avec v une variable tel que ${\displaystyle T\cup \Sigma }$ est satisfaisable dans la structure, c'est-à-dire tel que ${\displaystyle M\models \psi (v)[a]}$ pour toute formule ${\displaystyle \psi (v)}$ appartenant à ${\displaystyle \Sigma (v)}$ et ${\displaystyle M\models T[a]}$ avec ${\displaystyle M}$ la structure, T la théorie, ${\displaystyle a}$ une assignation de variables. Il faut remarquer que la notion de type peut être généralisée : pour un n-type, on considère l'ensemble des formules ${\displaystyle \Sigma (v)}$ avec v un n-uplet. Nous pouvons spécifier la définition précédente en considérant les 1-types sur un ensemble A : les formules de ${\displaystyle \Sigma (v)}$ peuvent comporter des paramètres qui appartiennent à A. On dit que le 1-type t est complet si pour toute formule du langage ${\displaystyle \psi (v)}$, on a soit ${\displaystyle \psi (v)\in t}$ ou ${\displaystyle \neg \psi (v)\in t}$.

Dès lors, une théorie est ${\displaystyle \omega }$-stable si pour chaque modèle de la théorie (pour chaque ensemble A inclus dans l'univers), il existe au plus un nombre dénombrable de 1-types complets (sur A). Intuitivement, cela signifie que la théorie présente une forme de simplicité car elle ne possède pas un nombre trop grand de types, ces derniers peuvent être aisément classés : on retrouve une notion analogue à celle de base dans un espace vectoriel. Par ailleurs, l'oméga-stabilité est à mettre en relation avec la notion de catégoricité non-dénombrable ; nous cherchons alors à donner sens à l'idée d'une caractérisation unique et concise d'une théorie (voir la section consacrée à la catégoricité).

Exemple

D'après le théorème de Macintyre (1971), la théorie des corps algébriquement clos est ${\displaystyle \omega }$-stable (la démonstration repose sur le théorème de la base de Hilbert, et donc l'axiome du choix).

La propriété de stabilité peut être généralisée de la façon suivante : une théorie T dans un langage L est stable s'il existe un cardinal ${\displaystyle \kappa \geq |L|}$ tel que pour tout modèle de T de cardinalité inférieure ou égale à ${\displaystyle \kappa }$, il y a au plus un nombre ${\displaystyle \kappa }$ de 1-types complets.

• Calcul des prédicats
• Calcul des propositions
• Déduction naturelle
• Skolémisation
• Logique classique
• Logique intuitionniste
• Logique minimale
• Modèle non standard
• Sémantique de Kripke
• Sémantique dénotationnelle
• Type (théorie des modèles)
• Théorie stable (en)

Cours de sémantique formelle

• Daniel Lascar, La théorie des modèles en peu de maux, Cassini, 2009, (ISBN 978-2-84225-137-6)
• (en) C. C. Chang et H. Jerome Keisler, Model Theory, Amsterdam/New York/New York, NY, USA, Elsevier, coll. « Studies in Logic and the Foundations of Mathematics », 1990, 3^e éd. (1^re éd. 1973) (ISBN 978-0-444-88054-3, lire en ligne). Ouvrage de référence sur le sujet lors de sa parution.

• Portail des mathématiques
• Portail de la logique