Indécidabilité
Le terme d'indécidabilité recouvre plusieurs concepts liés en logique mathématique, formalisant l'idée qu'on ne peut pas toujours conclure.
| Sommaire |
Indécidabilité d'un énoncé dans un système logique
Un énoncé mathématique est dit indécidable dans un système axiomatique s'il est impossible de le déduire, ou de déduire sa négation, à partir des axiomes.
En termes plus concrets, cela veut dire qu'on demande au système de fournir une conclusion sans lui avoir fourni suffisamment d'hypothèses. Ainsi, l'âge du capitaine d'un bateau est indécidable en fonction du tonnage et de la vitesse du navire.
Le théorème d'incomplétude de Gödel montre que dans tout système logique suffisamment puissant pour représenter l'arithmétique de Peano (l'arithmétique usuelle), il existe forcément des propositions indécidables.
Une proposition indécidable, ou sa négation, peut être ajoutée à un système cohérent pour former un autre système cohérent. C'est ainsi que l'on ajoute souvent l'axiome du choix aux axiomes de Zermelo-Fraenkel (ZF) pour former le système ZFC.
Une proposition est indécidable dans une théorie s'il existe des modèles de la théorie où la proposition est fausse et des modèles où elle est vraie.
Les ensembles indécidables
L'indécidabilité d'un énoncé est relative à un système d'axiomes. On peut cependant donner un sens absolu à la notion d'indécidabilité à propos des ensembles infinis de formules.
Un ensemble de formules ou d'expressions formelles est indécidable lorsque lui-même ou son complémentaire n'est pas (récursivement) énumérable.
Cette définition est cohérente avec la précédente parce que l'ensemble des propositions dérivables à partir d'une théorie finiment axiomatisée (des axiomes, ou schémas d'axiomes, et des règles de déduction, en nombre fini) est récursivement énumérable. Lorsque l'ensemble des vérités d'une théorie est indécidable, il y a forcément des énoncés indécidables, c’est-à-dire dans ce cas des énoncés vrais mais qui ne peuvent pas être prouvés sur la base des axiomes.
Certaines théories sont décidables au sens où un nombre fini d'axiomes ou de schémas d'axiomes suffit pour prouver toutes les vérités (toute formule ou sa négation est prouvable). Dans ce cas les ensembles des théorèmes et des vérités coïncident et ils sont décidables. Mais les théories axiomatiques fondamentales pour l'ensemble des mathématiques (arithmétique formelle, théories des ensembles, ...) ne sont pas décidables. Leurs axiomes ne suffisent jamais pour prouver toutes les formules ou leur négations tant qu'elles sont finiment axiomatisées. L'ensemble des formules prouvables, ou théorèmes, est énumérable, mais pas l'ensemble des formules non-prouvables, qui est dans ce cas différent de l'ensemble des formules dont la négation est prouvable.
Les ensembles indécidables ont été découverts et étudiés par de nombreux auteurs (Gödel, Tarski, Church, Post, Turing, Smullyan,...) à partir du théorème d'incomplétude de Gödel. Ils ont mis fin à l'espoir, formulé par Hilbert, d'une méthode unique pour résoudre tous les problèmes élémentaires (voir Incomplétude).
Indécidabilité d'un problème de décision
Définition
Un problème de décision est dit décidable s'il existe un algorithme (ou une machine de Turing) qui le décide, sinon il est indécidable. Par exemple, le problème de l'arrêt est indécidable.
Ce concept de l'indécidabilité est lié aux précédents : dans une théorie décidable, sans proposition indécidable, le problème de décider si une proposition est démontrable est décidable. Si un problème est indécidable, alors l'ensemble de toutes les questions qui ont une réponse positive est indécidable, de même que l'ensemble des questions qui ont une réponse négative.
Dire qu'un problème est indécidable ne veut pas dire que les questions posées sont insolubles mais seulement qu'il n'existe pas de méthode unique et bien définie, applicable d'une façon mécanique, pour répondre à toutes les questions, en nombre infini, rassemblées dans un même problème.
Exemples de problèmes indécidables
- Le problème de l'arrêt. Dans ce cas, les questions portent sur tous les programmes informatiques (dans un langage suffisamment puissant, tel que tous ceux utilisés en pratique) et sur tous les états initiaux possibles de la mémoire (définis par une quantité finie d'information). Il s'agit de savoir si oui ou non un ordinateur s'arrêtera lorqu'il exécute un programme à partir de l'état initial de la mémoire. L'indécidabilité du problème de l'arrêt a été prouvée par Alan Turing.
- La question si oui ou non une formule est une loi logique.
- La question si oui ou non une formule de l'arithmétique formelle est vraie (au sens des la théorie des nombres entiers standards).
- La question si oui ou non une formule est prouvable à partir des axiomes de l'arithmétique formelle. Gödel et Tarski ont prouvé que cet ensemble est différent du précédent. On peut prouver qu'il est plus petit (voir Cohérence des axiomes de l'arithmétique formelle)
- La question si oui ou non une formule est prouvable à partir des axiomes d'une théorie des ensembles cohérente, ou de toute théorie cohérente suffisamment riche (en un sens difficile à préciser. Que tous les théorèmes de l'arithmétique formelle y soient prouvables est une condition suffisante mais non nécessaire).
- La question si oui ou non une équation diophantienne a une solution. La preuve de son indécidabilité est le théorème de Matiyasevich(1970)
- La question si oui ou non une formule est une identité de la logique combinatoire, qui est une autre formulation du lambda-calcul. Son indécidabilité a été prouvée par Alonzo Church.
- La question si oui ou non une expression formelle est un élément d'un ensemble énumérable. Dans ce cas, les questions portent sur toutes les expressions formelles et tous les noms d'ensembles d'un univers suffisamment riche pour représenter tous les ensembles énumérables. (voir Smullyan, Theory of formal systems)
- On trouvera d'autres exemples dans théorème d'incomplétude de Gödel
- Et beaucoup d'autres,...