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é).
Histoire
L'idée d'interprétation de théories mathématiques dans des structures apparaît assez tôt, dès le . Ainsi l'abbé BuéeAdrien-Quentin Buée, Mémoire sur les quantités imaginaires, Royal Society of London, 1806. 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 publiera Grundlagen der Geometrie Foundations of Geometry (traduction de 1902) numérisée sur le Projet Gutenberg (Les fondements de la géométriehttps://www.pedagogie.ac-aix-marseille.fr/upload/docs/application/pdf/2019-11/principes_fondamentaux_geometrie_-_david_hilbert.pdf) 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.
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ésTraduit dans le recueil Logique, sémantique, métamathématique, Armand Colin 1972, p. 157-269.. 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.
Concepts fondamentaux de la théorie des modèles
Un langage 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 , 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 ou ].
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 ; est une formule. Il existe un ensemble fini tel que .
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.
Les modèles du calcul propositionnel classique 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 , le ou et le non sont emboîtés l’un dans l’autre. Mais le non et le et 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é ait été définie. Montrons comment définir la vérité et la fausseté des formules de complexité . Soit une formule de complexité , obtenue à partir de la formule ou des formules et de complexité ou inférieure, au moyen d'un connecteur logique. La vérité ou la fausseté de et est donc déjà définie.
a) : Si est vrai alors est faux, par définition de la négation. Si est faux alors est vrai, pour la même raison.
b) : Si et sont tous les deux vrais alors aussi, mais est faux dans tous les autres cas.
c) : Si et sont tous les deux faux alors aussi, mais est vrai dans tous les autres cas.
d) : Si est vrai et est faux alors est faux, mais 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 variables propositionnelles atomiques, il suffit en fait de vérifier la vérité de la formule dans les modèles possibles donnant les diverses valeurs de vérité aux 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.
Exemples
Montrons que (loi de Peirce) est une tautologie, en utilisant la règle d). Si est vraie, alors étant de la forme est vraie. Si est faux, alors est vrai, est faux, et est vrai.
Étant vrai dans tout modèle, est une tautologie. Elle est donc également prouvable au moyen de systèmes de déduction, par exemple la déduction naturelle.
Par contre, n'est pas prouvable. En effet, dans un modèle où est faux, est également faux.
Les modèles dans le calcul des prédicats 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 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 -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.
L'interprétation des formules atomiques dans un modèle 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.
La définition de la véracité des formules complexes 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) : Si l'une des formules obtenues en substituant un élément de U à toutes les occurrences libres de dans l'interprétation de est fausse alors est fausse, sinon, si n'a pas d'autres variables libres que , est vraie.