Modèles, preuves, calculs : la logique mathématique moderne s’est organisée autour de trois questions qui se répondent l’une à l’autre. Cette page les fait fonctionner, chacune sur un exemple que la machine calcule entièrement.
« Aujourd’hui, la logique mathématique se structure en trois grands champs : la théorie des modèles, lien entre syntaxe (formules) et sémantique (structures concrètes) ; la théorie de la preuve, structure combinatoire des démonstrations ; la théorie de la calculabilité (ou théorie de la récursion), initiée par Alan Turing et Alonzo Church, qui formalise la notion d’algorithme et constitue le pont direct vers l’informatique théorique. »
On y ajoute souvent un quatrième champ, la théorie des ensembles, qui étudie les fondements et l’infini. Les trois champs cités partagent le même matériau — des suites finies de symboles — mais posent trois questions différentes.
Question : que disent réellement les formules ?
On compare des structures (un ensemble muni de relations et d’opérations) et l’on cherche ce qu’un langage peut ou ne peut pas exprimer. Outils : compacité, jeux, élimination des quantificateurs. Planche 1.
Question : de quoi une démonstration est-elle faite ?
Une preuve n’est plus seulement un certificat : c’est un objet combinatoire, un arbre que l’on peut mesurer, transformer, simplifier. Outils : calcul des séquents, élimination des coupures. Planches 2 et 3.
Question : que peut faire une machine ?
On définit précisément ce qu’est un algorithme, puis on démontre ce qu’aucun algorithme ne peut faire. Outils : machines de Turing, λ-calcul, réductions. Planches 4 et 5.
Ces champs ne sont pas cloisonnés : une preuve est un programme (planche 3), un problème indécidable se rencontre aussi bien en théorie des modèles qu’en théorie de la preuve (planche 5), et la compacité de la théorie des modèles sert à démontrer des résultats de calculabilité.
Deux structures peuvent être différentes sans qu’aucune formule courte ne les distingue. Le jeu d’Ehrenfeucht-Fraïssé mesure exactement cela. Deux joueurs, un nombre de tours fixé : le Spoiler veut montrer que les structures diffèrent, le Duplicateur qu’elles se ressemblent. À chaque tour, le Spoiler choisit un élément dans l’une des deux structures, le Duplicateur doit répondre par un élément de l’autre. Le Duplicateur gagne si, à la fin, les éléments choisis se correspondent dans le même ordre. Théorème : le Duplicateur gagne en k tours exactement lorsque aucune formule de profondeur de quantificateurs k ne sépare les deux structures.
À vous de jouer le Spoiler : cliquez un point, en haut ou en bas. La machine répond en Duplicateur, en jouant au mieux.
La machine résout le jeu pour toutes les tailles et en déduit le seuil : à partir de quelle taille deux ordres finis de tailles différentes deviennent-ils indiscernables en k tours ? Aucune formule ne compte donc au-delà de ce seuil.
Gentzen a donné aux démonstrations une forme normalisée : le calcul des séquents. Un séquent Γ ⇒ Δ se lit « si tout ce qui est à gauche est vrai, alors l’un au moins des énoncés de droite l’est ». Chaque connecteur a une règle à gauche et une règle à droite ; démontrer, c’est remonter des règles jusqu’à des axiomes. La preuve devient un objet fini que l’on peut mesurer : profondeur, nombre de règles, nombre de branches.
Deux systèmes, deux idées de la vérité. Le calcul classique autorise plusieurs formules à droite : c’est ce qui rend démontrable le tiers exclu. Le calcul intuitionniste n’en autorise qu’une seule : démontrer « A ou non-A » y exige de démontrer A, ou de démontrer non-A. Une preuve intuitionniste contient toujours une construction.
Écrivons une démonstration de « A implique A » : on suppose A, on conclut A. Écrivons maintenant le programme qui prend une donnée de type A et la renvoie : λx:A. x. C’est le même objet. Plus généralement : une formule est un type, une démonstration est un programme, et utiliser un lemme puis le démontrer (une coupure) correspond à appeler une fonction. Simplifier la preuve, c’est exécuter le programme.
En 1936, Turing propose une machine idéalisée : un ruban infini de cases contenant 0 ou 1, une tête qui lit et écrit une case, un nombre fini d’états internes, et une table de règles « dans l’état q, en lisant s : écrire, se déplacer d’une case, changer d’état ». Church, la même année, définissait le calculable par le λ-calcul de la planche 3 : les deux notions se sont révélées équivalentes, ce qui a donné la thèse de Church-Turing — tout ce qui est calculable par un procédé mécanique l’est par une machine de Turing.
Les trois champs se rejoignent sur un même obstacle : certains problèmes n’ont aucune méthode générale de résolution. Ce n’est pas un manque d’astuce, c’est un théorème. Deux expériences le rendent palpable, puis un tableau récapitule ses visages dans chaque domaine.
Soit BB(n) le plus grand nombre de 1 qu’une machine à n états puisse laisser sur un ruban vide avant de s’arrêter. Pour le connaître, il faudrait distinguer les machines qui s’arrêtent de celles qui tournent sans fin : BB n’est donc calculable par aucun algorithme. On peut pourtant l’établir pour de très petites valeurs, en examinant toutes les machines une par une. La machine le fait ici : elle énumère les 1 728 machines à 2 états, puis le million de machines à 3 états (la première règle étant fixée, ce qui ne change rien au record).
| n | BB(n) : 1 écrits | pas avant l’arrêt | statut |
|---|---|---|---|
| 1 | 1 | 1 | immédiat |
| 2 | 4 | 6 | calculé ci-dessus |
| 3 | 6 | 21 | calculé ci-dessus |
| 4 | 13 | 107 | établi en 1983 (Brady) |
| 5 | 4 098 | 47 176 870 | établi en 2024 par une preuve formelle collective, vérifiée en Rocq/Coq |
| 6 | > 1036 534 | > 1036 534 | minoration de 2010, très largement dépassée depuis |
Un jeu de dominos : chacun porte un mot en haut et un mot en bas. Peut-on en aligner une suite (avec répétitions) de façon que la ligne du haut et celle du bas forment le même mot ? C’est la correspondance de Post (1946). Chaque cas se vérifie en un clin d’œil, mais aucune méthode générale ne décide si une solution existe : le problème est indécidable — et une solution peut être arbitrairement longue.
Cliquez les dominos pour construire vous-même une suite.
Le même obstacle, traduit dans chaque champ. Les trois colonnes parlent du même théorème : à partir du moment où un formalisme sait simuler une machine, il hérite de son indécidabilité.
| Champ | Problème indécidable | Ce qui reste possible |
|---|---|---|
| Calculabilité | Arrêt d’une machine sur une entrée donnée (Turing, 1936) ; théorème de Rice (1953) : toute propriété non triviale de ce que calcule un programme est indécidable. | Énumérer les machines qui s’arrêtent (semi-décision) ; décider pour des classes restreintes ; mesurer le coût (complexité). |
| Théorie de la preuve | Validité d’une formule du premier ordre (Church et Turing, 1936) : aucune méthode ne décide si une formule est démontrable. | Énumérer les démonstrations ; décider le calcul propositionnel (planche 2) ; automatiser des fragments (résolution, arithmétique linéaire). |
| Théorie des modèles | Théorie de l’arithmétique (ℕ, +, ×) : indécidable (Church, Tarski). Théorie des groupes de type fini : problème du mot indécidable (Novikov, 1955 ; Boone, 1958). | Des théories complètes et décidables : ordres denses, corps réels clos (Tarski, 1948), (ℕ, +) (Presburger, 1929), corps algébriquement clos. |
La frontière passe donc à l’intérieur de chaque champ, entre les fragments décidables, où les algorithmes fonctionnent, et les théories assez riches pour parler de calcul, où aucune méthode générale n’existe. Une grande part de la logique contemporaine consiste précisément à repérer cette frontière — et à installer les outils juste du bon côté.
Ce que les formules distinguent, et ce qu’elles ne distinguent pas. Les jeux donnent la mesure exacte de la puissance d’un langage.
La démonstration devient un arbre que l’on peut normaliser. Classique ou intuitionniste : deux formes de preuve, deux usages.
Une preuve est un programme, un programme est une machine, et certaines questions n’ont aucune réponse mécanique.
Où sont les applications ? La théorie des modèles a servi à démontrer des théorèmes de géométrie diophantienne (Hrushovski) et fonde l’analyse des bases de données. La théorie de la preuve est la base des assistants de preuve et des langages de programmation typés (la logique linéaire de Girard, 1987, a inspiré la gestion de la mémoire de langages comme Rust). La calculabilité est devenue l’informatique théorique, et sa fille la théorie de la complexité pose la question P contre NP.
Et la théorie des ensembles ? Souvent citée comme quatrième champ, elle étudie les fondements et les infinis, avec les méthodes de forcing de Cohen. Les pages de cette série sur la quête des fondements et sur ZFC lui sont consacrées.
Degrés d’indécidabilité. Entre le décidable et le problème de l’arrêt, il existe une infinité de niveaux intermédiaires (Friedberg et Muchnik, 1956-1957) : l’indécidabilité n’est pas un mur unique, mais un paysage.
Dans la même série. Les pages sur la métamathématique (complétude, incomplétude, théorie des modèles) et sur la quête des fondements (paradoxe de Russell, ZFC) précèdent naturellement celle-ci.