Théorie axiomatique

Quand on veut définir précisément cette notion en logique mathématique, on définit tout d'abord précisément le langage de la théorie : par exemple un langage du premier ordre.

Suivant les auteurs, on désigne par « théorie » :

1. un ensemble quelconque d'énoncés (des formules closes, c’est-à-dire sans variable libre) du langage considéré ;
2. ou un ensemble d'énoncés clos par déduction dans la logique considérée, sans autre précision il s'agit de la logique classique.

Dans le premier cas, le mot « théorie » fait référence à un ensemble d'axiomes de la théorie. Dans le second, il fait référence aux théorèmes de la théorie.

Un choix immédiat, quoique guère intéressant, serait de prendre tous les théorèmes comme axiomes ; il y a donc toujours un système d'axiomes pour une théorie donnée (au sens close par déduction), et il y a même forcément plusieurs systèmes d'axiomes possibles pour une théorie donnée. Pratiquement, quelle que soit la définition utilisée, le contexte permet de lever les ambiguïtés.

Cette notion très extensive de théorie est celle utilisée en logique mathématique, en particulier en théorie des modèles. Ainsi l'ensemble des énoncés du langage de l'arithmétique, vrais dans les entiers usuels, est évidemment clos par déduction. Mais, comme on le déduit immédiatement du premier théorème d'incomplétude de Gödel, il n' y a aucun moyen de donner un système d'axiomes pour cette théorie, moyen que l'on puisse utiliser dans la pratique mathématique, car pour cela il faudrait au minimum pouvoir reconnaître « sans trop d'effort » (on veut dire mécaniquement) un axiome parmi les énoncés du langage de la théorie.

On est donc amené à introduire une notion plus précise, la notion de théorie récursivement axiomatisable (voir la suite de cet article), qui est d'ailleurs un préalable pour énoncer le théorème de Gödel que l'on vient d'évoquer.

Une théorie est dite cohérente, ou de façon équivalente non contradictoire ou encore consistante, quand il existe des énoncés de la théorie qui ne sont pas démontrables. Cela revient à dire, en tout cas en logique classique ou intuitionniste, que l'on ne peut pas démontrer de contradiction. En calcul des prédicats classique du premier ordre, une théorie est cohérente si et seulement si elle a un modèle : c'est le théorème de complétude. Les théories utilisées en mathématiques sont supposées cohérentes, même si, dès que ces théories permettent de développer suffisamment d'arithmétique, il ne peut y avoir de démonstration de cette cohérence sans supposer la cohérence d'une théorie plus forte, comme le montre le second théorème d'incomplétude de Gödel.

On considérera pour la suite que les théories sont des théories du premier ordre de la logique classique, même si de fait, la plupart des notions évoquées ont un sens en logique intuitionniste, dans des logiques d'ordre supérieur, etc.

Une théorie récursivement axiomatisable est une théorie qui peut être axiomatisée de façon qu'il soit possible de reconnaître de façon purement mécanique les axiomes parmi les énoncés du langage de la théorie. C'est le cas des théories utilisées pour formaliser tout ou partie des mathématiques usuelles, comme l'arithmétique de Peano ou la théorie des ensembles de Zermelo-Fraenkel.

Intuitivement on demanderait même aux systèmes d'axiomes plus que cela : on doit pouvoir vérifier « sans avoir à réfléchir » qu'un certain énoncé est un axiome. C'est ce que l'on capture de façon imparfaite, en disant que cette vérification est mécanique, c'est-à-dire que l'on pourrait la confier à une machine, un ordinateur. Un ordinateur est capable de vérifications qui n'ont rien d'immédiat pour un être humain, à plus forte raison si l'ordinateur est purement théorique, telle la machine de Turing, que l'on utilise pour formaliser ces notions. Par exemple, la géométrie euclidienne, dans sa formalisation au premier ordre, est décidable, ce qui signifie que l'ensemble de ses théorèmes est un système d'axiomes récursif, bien que clairement inutilisable pour axiomatiser vraiment la géométrie, vu la complexité de la procédure de décision. Mais cette notion se formalise bien, c'est celle qui convient pour les théorèmes d'incomplétude ou d'indécidabilité.

Une condition est que les énoncés du langage de la théorie elle-même puissent être reconnus de façon mécanique, on dit que le langage est récursif. On conçoit bien que c'est le cas quand les symboles spécifiques du langage (appelés parfois la signature du langage) : symbole de constantes, de fonction ou d'opération, de prédicat ou de relation, sont en nombre fini. Par exemple l'arithmétique de Peano utilise, en dehors du vocabulaire purement logique (dont l'égalité), les symboles ${\displaystyle 0,s,+,\times }$ et éventuellement ${\displaystyle \leq }$ qui sont bien en nombre fini. On peut également construire des langages récursifs de signature infinie.

Un cas particulier évident de théorie récursivement axiomatisable est celui des théories finiment axiomatisables, c’est-à-dire des théories pour lesquelles on peut donner un nombre fini d'axiomes. Ainsi la théorie des groupes, la théorie des corps sont finiment axiomatisables.

Certaines théories ont un nombre infini d'axiomes, mais ceux-ci sont décrits de façon finie, on parle alors de schéma d'axiomes. Par exemple l'arithmétique de Peano, théorie du premier ordre, énonce la récurrence comme un schéma d'axiomes : il faut un axiome par formule pour laquelle on énonce la récurrence. L'arithmétique de Peano est donc donnée par une infinité d'axiomes, mais on voit bien que l'on pourra reconnaître mécaniquement les énoncés qui expriment la récurrence parmi les énoncés du langage.

Tout ceci se formalise rigoureusement en codant les formules du langage par des entiers et en utilisant la théorie de la calculabilité. Une fois les énoncés codés par des entiers, on dit qu'un ensemble d'énoncés est récursif si la fonction caractéristique des codes de ces énoncés est une fonction calculable. Une théorie récursivement axiomatisable est donc une théorie qui possède un système d'axiomes récursif.

Il est également possible de définir ces notions sans passer par des codages par les entiers, en utilisant la théorie des langages formels. Il se trouve que ces notions sont souvent utiles dans un contexte (théorème d'incomplétude de Gödel, théorème de Church) où de toute façon on a besoin de coder arithmétiquement les formules.

En mathématiques, on s'accorde à penser que l'on peut reconnaître sans effort d'imagination que « quelque chose », disons une suite de phrases, est une preuve. S'agissant d'une preuve formelle, on doit pouvoir en vérifier les étapes pas à pas de façon mécanique. Vu notre définition de théorie, une condition nécessaire pour que cela soit vrai est que la théorie soit récursivement axiomatisable. Si l'on examine n'importe quel système formel pour la logique, par exemple un système à la Hilbert ou le calcul des séquents, on se convainc que cette condition est suffisante : ainsi, on peut vérifier de façon purement mécanique qu'une formule se déduit de deux formules par modus ponens. Là encore on formalise ceci rigoureusement en codant les preuves par des entiers et en utilisant la théorie de la calculabilité, et l'on montre que

dans une théorie récursivement axiomatisable, « être une preuve » est décidable.

On déduit de ce résultat que l'on peut énumérer de façon mécanique les théorèmes d'une théorie récursivement axiomatisable. Dit autrement, on peut construire une machine théorique, qui va fonctionner indéfiniment, et donner un à un tous les théorèmes de la théorie. Plus formellement,

l'ensemble des théorèmes d'une théorie récursivement axiomatisable est récursivement énumérable.

Cela ne permet pas de vérifier mécaniquement qu'un énoncé est un théorème. On peut bien lancer la machine, tant que l'on n'obtient pas l'énoncé que l'on cherche à démontrer, sans autre information, on ne sait pas si c'est parce que la machine le donnera plus tard ou ne le donnera jamais.

Esquissons une preuve informelle de ce résultat. Considérons que les preuves sont écrites en utilisant un nombre fini de lettres. Toutes les lettres doivent compter : ${\displaystyle x_{0}}$ fait deux lettres, ${\displaystyle x_{10}}$ trois lettres etc. La taille d'une preuve est le nombre de lettres utilisées pour l'écrire. On compte les répétitions et une preuve peut être de taille arbitrairement grande, mais il n'y a qu'un nombre fini (éventuellement nul) de preuves d'une taille donnée. On peut donc énumérer de façon mécanique les preuves en énumérant successivement toutes celles d'une taille fixée, puis toutes celles d'une taille strictement plus grande, et ceci indéfiniment. On en déduit une énumération mécanique des théorèmes : il suffit de lire à chaque fois la conclusion de la preuve. Telle quelle, rien n'empêche cette énumération de produire des répétitions (mais il serait possible d'en construire une qui les évite). Cependant si on lance la machine qui énumère les théorèmes, il y a peu de chances que l'on trouve un théorème intéressant avant très très longtemps.

On a en fait la réciproque du résultat. On peut donc énoncer[1]

une théorie est récursivement axiomatisable si et seulement si l'ensemble des théorèmes de cette théorie est récursivement énumérable.

On construit un système d'axiomes décidable pour un ensemble de théorèmes récursivement énumérable à l'aide d'une petite astuce logique. Soit

${\displaystyle A_{0},\ A_{1},\ A_{2},\ \dots \ ,\ A_{n},\ \dots }$

la suite des théorèmes telle qu'énumérée par une machine. On construira tout aussi mécaniquement la suite des conjonctions successives des énoncés de cette théorie, soit

${\displaystyle A_{0},\ (A_{0}\land A_{1}),\ (A_{0}\land A_{1}\land A_{2}),\ \dots \ ,\ (A_{0}\land A_{1}\land \dots \land A_{n}),\ \dots }$

que l'on choisit comme nouveau système d'axiomes. Comme la suite de départ est l'ensemble des théorèmes d'une théorie, donc est close par déduction, on a ainsi extrait une sous-suite infinie. Les énoncés de cette suite axiomatisent trivialement la théorie initiale. La suite des axiomes obtenue est énumérée de façon strictement croissante en taille (par exemple le nombre de signes nécessaires pour écrire l'énoncé), puisque chaque axiome est obtenu en complétant le précédent par conjonction avec un nouvel énoncé. Pour savoir si un énoncé quelconque B est un axiome, il suffit donc d'énumérer ceux-ci jusqu'à trouver soit l'énoncé B, et alors c'est bien un axiome, soit un énoncé de taille strictement supérieure, et ce n'en est pas un. Techniquement, si l'on formalise, on utilise le résultat de calculabilité suivant : l'ensemble image d'une fonction récursive strictement croissante est un ensemble récursif.

On prouve exactement de la même façon (car la clôture par déduction n'intervient pas dans la démonstration) que

une théorie qui a un ensemble récursivement énumérable d'axiomes, a un ensemble récursif d'axiomes.

et donc la notion de théorie axiomatisable par un ensemble récursivement énumérable d'axiomes n'a pas grand intérêt (autant prendre directement tous les théorèmes).

Pour les théories récursivement axiomatisables, on peut établir un lien entre la notion de décidabilité au sens logique . Un énoncé est décidable si lui ou sa négation est un théorème, et la notion de décidabilité au sens algorithmique, un ensemble est décidable – ou récursif – si l'on peut décider mécaniquement de l'appartenance à cet ensemble.

On dit qu'une théorie est complète quand tous les énoncés du langage de la théorie sont décidables dans la théorie, c'est-à-dire que chaque énoncé est un théorème ou sa négation est un théorème.

On dit qu'une théorie est récursive (on dit aussi décidable, mais on évitera de le faire dans la suite car cela prête trop à ambiguïté dans ce contexte), quand l'ensemble de ses théorèmes est récursif.

Une théorie récursive est évidemment récursivement axiomatisable : il suffit de prendre pour axiomes tous les théorèmes. On montre qu'il existe des théories récursivement axiomatisables qui ne sont pas récursives, comme l'arithmétique de Peano, mais aussi des théories beaucoup plus simples, le calcul des prédicats dans un langage suffisamment riche, comme celui de l'arithmétique ou un langage avec au moins un symbole de prédicat binaire (voir théorème de Church). Mais on peut montrer que :

Une théorie récursivement axiomatisable et complète est récursive (c’est-à-dire décidable au sens algorithmique).

Montrons ce résultat. On peut supposer la théorie cohérente, car l'ensemble des théorèmes d'une théorie incohérente est l'ensemble de toutes les formules closes, qui est récursif dès que le langage de la théorie est récursif. Si une théorie est cohérente et complète, l'ensemble des énoncés qui ne sont pas des théorèmes est l'ensemble des énoncés dont la négation est un théorème. On en déduit très facilement qu'il est également récursivement énumérable. Or l'ensemble des énoncés du langage de la théorie est récursif. On sait en théorie de la calculabilité que si un ensemble est récursivement énumérable, et si son complémentaire à l'intérieur d'un ensemble récursif est récursivement énumérable, cet ensemble est récursif.

Détaillons l'argument, en l'adaptant à notre cas particulier. Nous avons une machine qui énumère les théorèmes de la théorie, supposée cohérente. Nous voulons savoir si l'énoncé ${\displaystyle B}$ est un théorème. On lance la machine et on compare à chaque étape l'énoncé produit à ${\displaystyle B}$ et à sa négation. Comme la théorie est complète ce processus termine : on finit par produire soit ${\displaystyle B}$, soit sa négation. On vient de définir un procédé mécanique qui permet de savoir si un énoncé donné est démontrable (la machine a produit ${\displaystyle B}$) ou non démontrable (la machine a produit la négation de ${\displaystyle B}$, donc par cohérence de la théorie, ${\displaystyle B}$ n'est pas démontrable). La théorie est donc récursive.

Par contraposée, on obtient immédiatement qu'une théorie récursivement axiomatisable qui n'est pas récursive ne peut être complète. On peut donc très bien démontrer le premier théorème d'incomplétude de Gödel en utilisant ce résultat (comme dans la référence bibliographique indiquée).

René Cori et Daniel Lascar, Logique mathématique II. Fonctions récursives, théorème de Gödel, théorie des ensembles, théorie des modèles [détail des éditions]

• Axiome
• Axiomatisation