Cohérent (système formel)

Imaginez une machine qui part d’axiomes et applique mécaniquement des règles à des phrases. Si elle peut produire à la fois « la lampe est allumée » et « la lampe n’est pas allumée », le système formé par ses axiomes et ses règles est contradictoire. Un système cohérent évite cette situation : aucune affirmation et sa négation ne peuvent toutes deux sortir d’une démonstration correcte.

Cette garantie ne dit pas que la machine sait répondre à toute question. Elle dit seulement que ses réponses démontrables ne se détruisent pas mutuellement.

Un système formel fixe un langage, des axiomes et des règles d’inférence. Une formule est démontrable lorsqu’une suite finie d’applications de ces règles la fait découler des axiomes. Le système est cohérent, ou consistant, lorsqu’il n’existe aucune formule, notée A, pour laquelle A et sa négation sont toutes deux démontrables.

Dans une logique classique, un système incohérent devient inutilisable pour distinguer le vrai du faux : le principe d’explosion permet alors de démontrer n’importe quelle formule. La cohérence ne doit toutefois pas être confondue avec la complétude. Un système peut être cohérent tout en laissant certaines propositions indécidables, c’est-à-dire sans démontrer ni la proposition ni sa négation.

Le second théorème d’incomplétude de Gödel concerne les théories formelles cohérentes, effectivement axiomatisées et assez expressives pour formaliser une part suffisante de l’arithmétique. Sous les conditions usuelles de représentabilité de la démonstration, une telle théorie ne démontre pas l’énoncé qui formalise sa propre cohérence. Si elle est incohérente, elle démontre au contraire toute formule, y compris cet énoncé : ce n’est évidemment pas une preuve fiable de cohérence.

Trois éléments structurent un système formel. Le langage détermine les symboles et les formules bien formées. Les axiomes fournissent les points de départ. Les règles d’inférence autorisent chaque passage d’une ligne de preuve à la suivante. Lorsque la logique considérée comporte une négation, celle-ci appartient au langage : elle peut être primitive ou construite à partir d’autres symboles, et n’est pas présente dans tout système formel.

Le langage conditionne les énoncés que les axiomes et les preuves peuvent exprimer. Les axiomes et les règles déterminent ensemble ce qui est démontrable ; la cohérence porte donc sur leur combinaison, pas sur une phrase isolée. Ces données suffisent à construire les démonstrations possibles et à poser le test décisif : trouve-t-on une formule A ainsi qu’une preuve de A et une preuve de sa négation ?

Considérons un petit système de logique propositionnelle classique. La lettre p signifie « la lampe est alimentée » et la lettre q « la lampe s’allume ». Les deux prémisses sont « si p, alors q » et p. La règle utilisée est le modus ponens : de « si p, alors q » et de p, elle autorise à conclure q.

1. On inscrit la prémisse $p\to qp\; \backslash to\; q$.
2. On inscrit la prémisse p.
3. Le modus ponens donne q. Aucune de ces étapes ne donne la négation de q.

Pour contrôler l’ensemble du système, attribuons la valeur « vrai » à p et à q. Les deux prémisses sont alors vraies. Les axiomes usuels de la logique propositionnelle sont vrais sous toute attribution, et le modus ponens préserve la vérité. Toute formule démontrable est donc vraie sous cette attribution. Or une formule et sa négation ne peuvent pas y être vraies ensemble : le système est cohérent.

Ce contrôle est refaisable : si l’on ajoutait la négation de q comme troisième prémisse, q et sa négation seraient immédiatement démontrables. Le système ainsi augmenté serait incohérent.

Lorsqu’un logicien propose des axiomes, il cherche une preuve de cohérence, souvent en construisant un modèle dans lequel tous les axiomes sont vrais. S’il trouve plutôt une formule et sa négation démontrables, il doit retirer ou modifier au moins un axiome ou une règle.

Pour un système fini très simple, on peut examiner toutes les attributions de vérité ou automatiser la recherche d’un modèle. Pour une théorie arithmétique riche, cette vérification exhaustive n’est pas disponible ; on emploie des arguments métamathématiques menés dans une théorie extérieure.

Face à une preuve supposée de cohérence interne, le bon réflexe est d’identifier précisément la théorie qui raisonne et celle dont la cohérence est affirmée. Le second théorème de Gödel interdit certaines autopreuves, pas toute preuve relative de cohérence.

Cohérence et complétude. La cohérence interdit de démontrer simultanément A et sa négation. La complétude demanderait que, pour chaque énoncé du domaine considéré, A ou sa négation soit démontrable. Une proposition indécidable peut donc exister dans un système cohérent.

Cohérence syntaxique et satisfaisabilité. La première parle de preuves formelles ; la seconde demande un modèle dans lequel tous les axiomes sont vrais. En logique propositionnelle classique, l’existence d’un tel modèle garantit la cohérence, comme dans l’exemple de p et q. L’équivalence générale dépend toutefois de la logique et des théorèmes de correction et de complétude disponibles.

Cohérence et vérité. Un système peut être cohérent sans décrire correctement l’objet visé. Des axiomes compatibles entre eux peuvent avoir un modèle sans être vrais de l’interprétation que l’on voulait étudier.

Ne pas conclure après quelques essais. L’absence de contradiction dans les premières démonstrations examinées ne prouve pas la cohérence. Il faut un argument qui couvre toutes les preuves possibles, par exemple un modèle et un théorème de correction.

Préciser la théorie extérieure. Une preuve de cohérence est relative aux moyens admis pour la mener. Une théorie plus forte peut parfois prouver la cohérence d’une théorie plus faible ; cela ne constitue pas l’autopreuve interdite par le second théorème d’incomplétude.

Respecter les hypothèses de Gödel. La formule « aucun système ne peut prouver sa cohérence » est fausse. La limitation vise certaines théories cohérentes, effectivement axiomatisées et suffisamment riches en arithmétique, avec une formalisation adéquate de la démontrabilité.

Une théorie incohérente peut affirmer sa cohérence. En logique classique, elle démontre toute formule par explosion. Le symptôme n’est donc pas l’absence d’un énoncé interne de cohérence, mais l’existence d’une contradiction démontrable.

L’entrée axiome précise le rôle des points de départ d’une théorie et leur articulation avec les règles de déduction.

La notice Gödel Kurt situe le mathématicien auquel sont dus les théorèmes qui bornent les ambitions des systèmes formels assez riches.

L’article Les théorèmes d’incomplétude de Gödel développe la portée des deux résultats au-delà de la seule question de cohérence.