Décidabilité

En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique.

Cet article traite des significations particulières qu'a pris le terme « décidabilité » en mathématiques et en informatique. Pour une approche plus générale voir décision.

L’indécidabilité est la négation de la décidabilité. Dans les deux cas, il s'agit de formaliser l'idée qu'on ne peut pas toujours conclure lorsque l'on se pose une question, même si celle-ci est sous forme logique.

Décidabilité, indécidabilité d'un énoncé dans un système logique

Une proposition (on dit aussi énoncé) est dite décidable dans une théorie axiomatique si on peut la démontrer ou démontrer sa négation dans le cadre de cette théorie. Un énoncé mathématique est donc indécidable dans une théorie s'il est impossible de le déduire, ou de déduire sa négation, à partir des axiomes de cette théorie. Pour distinguer cette notion d'indécidabilité de la notion d'indécidabilité algorithmique (voir ci-dessous), on dit aussi que l'énoncé est indépendant du système d'axiomes. C'est le cas notamment du célèbre postulat des parallèles d'Euclide, relativement à sa géométrie[1], ou encore de l'hypothèse du continu relativement à la théorie des ensembles usuelle, selon laquelle il n'y a pas de cardinal entre celui de l'ensemble des entiers naturels et celui de l'ensemble des nombres réels, dont Paul Cohen a démontré, en 1963, qu'elle était indécidable.

En logique classique, d'après le théorème de complétude, 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. On utilise souvent des modèles pour montrer qu'un énoncé est indépendant d'un système d'axiomes (dans ce cadre, on préfère employer indépendant plutôt qu'indécidable). La propriété utilisée dans ce cas n'est pas le théorème de complétude mais sa réciproque, très immédiate, appelée théorème de correction. C'est d'ailleurs ainsi qu'apparut pour la première fois la notion de modèle, avec la construction au XIXe siècle par Eugenio Beltrami de modèles de géométries non euclidiennes (qu'il appelait des représentations) ne vérifiant pas l'axiome des parallèles, et leur utilisation, en admettant le fait, assez intuitif, que la géométrie euclidienne est cohérente, pour démontrer que l'axiome des parallèles est indépendant des autres axiomes de la géométrie, ou encore indécidable dans le système formé des axiomes restants.

Une théorie mathématique pour laquelle tout énoncé est décidable est dite complète, sinon elle est dite incomplète. Beaucoup de théories mathématiques sont incomplètes, parce qu'il y a des énoncés, exprimables dans le langage de la théorie, qui ne sont pas déterminés par les axiomes (théorie des groupes, des anneaux…). Certaines théories, comme la théorie des corps algébriquement clos d'une caractéristique donnée[2], celle des corps réels clos[3], ou encore l'arithmétique de Presburger[4], sont complètes. Le théorème d'incomplétude de Gödel nous garantit que toute théorie axiomatique cohérente, et suffisamment puissante pour représenter l'arithmétique de Peano (l'arithmétique usuelle), est incomplète, pourvu qu'elle soit axiomatisée de façon que l'on puisse décider, au sens algorithmique (voir ci-dessous), si un énoncé est ou non un axiome. Cette dernière hypothèse, qui semble un peu compliquée à énoncer, est très naturelle et vérifiée par les théories axiomatiques usuelles en mathématiques.

Décidabilité, indécidabilité algorithmique d'un problème de décision

Définition

Un problème de décision est dit décidable s'il existe un algorithme, une procédure mécanique qui se termine en un nombre fini d'étapes, qui le décide, c'est-à-dire qui réponde par oui ou par non à la question posée par le problème. S'il n'existe pas de tels algorithmes, le problème est dit indécidable. Par exemple, le problème de l'arrêt est indécidable. On peut formaliser la notion de fonction calculable par algorithme, ou par procédure mécanique, de diverses façons, par exemple en utilisant les machines de Turing. Toutes les méthodes utilisées se sont révélées équivalentes dès qu'elles étaient suffisamment générales, ce qui constitue un argument pour la thèse de Church : les fonctions calculables par une procédure mécanique sont bien celles qui sont calculées selon l'un de ces modèles de calcul. La thèse de Church est indispensable pour interpréter, de la façon attendue, une preuve d'indécidabilité.

Si aucun procédé mécanique ou algorithme ne peut répondre à la question, on peut parler d’indécidabilité algorithmique, pour distinguer cette notion de l’indécidabilité logique exposée dans le paragraphe précédent (ou parfois de décidabilité au sens de Turing pour la décidabilité algorithmique, et de décidabilité au sens de Gödel pour la décidabilité logique).

Contrairement à l'indécidabilité logique, qui porte sur la vérité ou la fausseté d'un seul énoncé (ou plus précisément sur l'impossibilité de le démontrer ou de démontrer sa négation dans un système axiomatique donné), l'indécidabilité algorithmique porte sur l'impossibilité de résoudre le problème dans le cas général, ce qui n'exclut pas la possibilité de le résoudre dans certains cas particuliers.

Ensembles décidables et indécidables

Un sous-ensemble des entiers naturels est dit décidable, quand le problème de l'appartenance d'un entier quelconque à cet ensemble est décidable, indécidable sinon. On généralise directement aux n-uplets d'entiers. On dit aussi d'un ensemble décidable qu'il est récursif. Le complémentaire d'un ensemble décidable est décidable. On montre en théorie de la calculabilité qu'un ensemble récursivement énumérable dont le complémentaire est récursivement énumérable est récursif (c'est-à-dire décidable).

On généralise ces notions aux langages formels, par des codages « à la Gödel » (c'est-à-dire qu'on associe un entier à chaque proposition du langage) ; il est possible aussi de les définir directement. Dans le cas des théories logiques closes par déduction, on parle alors de théorie décidable, ou de théorie indécidable. Une théorie T est dite décidable si l'ensemble des numéros de Gödel des théorèmes de T est un ensemble récursif, elle est dite indécidable sinon. [5].

Ces notions ne doivent pas être confondues avec celles de théorie complète et théorie incomplète vues au paragraphe précédent, parce que (bien que cela présente peu d'intérêt pratique) on peut parfaitement prendre comme axiomes tous les énoncés vrais (au sens de "vrais dans un modèle donné"), et alors la théorie est complète alors qu'elle reste indécidable ; et parce que, inversement, une théorie très pauvre comme la théorie des groupes commutatifs possède de nombreux modèles et est donc incomplète, alors qu'on détermine facilement lesquelles de ses propositions sont des théorèmes, et donc qu'elle est décidable.

Exemples d'ensembles et de problèmes décidables

Tous les sous-ensembles finis des entiers sont décidables (il suffit de tester l'égalité à chacun des entiers de l'ensemble). On peut construire un algorithme pour décider si un entier naturel est pair ou non (on fait la division par deux, si le reste est zéro, le nombre est pair, si le reste est un, il ne l'est pas), donc l'ensemble des entiers naturels pairs est décidable ; il en est de même de l'ensemble des nombres premiers. Notons qu'un ensemble peut être théoriquement décidable sans qu'en pratique la décision puisse être faite, parce que celle-ci nécessiterait trop de temps (plus que l'âge de l'univers) ou trop de ressources (plus que le nombre d'atomes de l'univers). L'objet de la théorie de la complexité des algorithmes est d'étudier les problèmes de décision en prenant en compte ressources et temps de calcul.

Le problème de savoir si une proposition est vraie dans l'arithmétique de Presburger, c'est-à-dire dans la théorie des nombres entiers naturels avec l'addition mais sans la multiplication, est décidable.

Exemples de problèmes indécidables
  • L'indécidabilité du problème de l'arrêt a été démontrée par Alan Turing en 1936. Il n'existe pas d'algorithme qui permette de décider si, étant donné une machine de Turing quelconque et un mot d'entrée, le calcul de celle-ci s'arrête ou non. Du fait de la thèse de Church, ce résultat est très général. Depuis l'apparition de l'informatique, on peut l'interpréter ainsi : il n'existe pas de programme permettant de tester n'importe quel programme informatique d'un langage suffisamment puissant, tels tous ceux qui sont utilisés en pratique, afin de conclure dans tous les cas s'il s'arrêtera en un temps fini ou bouclera à jamais.
  • Plus généralement le théorème de Rice énonce que toute question sur les programmes informatiques qui ne dépend que du résultat du calcul (qu'il se termine ou non, valeur calculée etc.) est indécidable ou triviale (ici, « trivial » s'entend par : la réponse est toujours la même (oui ou non) quel que soit le programme).
  • La question de savoir si oui ou non un énoncé de la logique du premier ordre est universellement valide (démontrable dans toute théorie) dépend de la signature du langage choisie (les symboles d'opération ou de relation…). Ce problème, parfois appelé problème de la décision, est indécidable pour le langage de l'arithmétique, et plus généralement pour n'importe quel langage égalitaire du premier ordre qui contient au moins un symbole de relation binaire (comme < ou ∈). Pour un langage égalitaire du premier ordre ne contenant que des symboles de prédicat unaires (calcul des prédicats égalitaire monadique), il est décidable.
  • La question de savoir si oui ou non une proposition énoncée dans le langage de l'arithmétique (il faut les deux opérations, + et ×) est vraie dans le modèle standard de l'arithmétique est indécidable (c'est une conséquence du premier théorème d'incomplétude de Gödel, ou du théorème de Tarski).
  • La prouvabilité d'un énoncé à partir des axiomes de l'arithmétique de Peano est indécidable (voir problème de la décision). Gödel a montré que cet ensemble est strictement inclus dans le précédent. Comme l'axiomatique de Peano a une infinité d'axiomes, cela ne se déduit pas directement de l'indécidabilité du problème de la décision dans le langage, énoncée précédemment. Les deux résultats se déduisent d'un résultat général pour les théories arithmétiques qui satisfont certaines conditions. L'arithmétique de Peano vérifie ces conditions, mais aussi l'arithmétique Q de Robinson, qui a un nombre fini d'axiomes.
  • La prouvabilité d'un énoncé à partir des axiomes d'une théorie des ensembles cohérente, et plus généralement de toute théorie cohérente qui permet d'exprimer « suffisamment » d'arithmétique formelle est indécidable (voir problème de la décision).
  • La question de savoir si oui ou non une équation diophantienne quelconque possède une solution. La preuve de son indécidabilité est le théorème de Matiiassevitch (1970).
  • La question de savoir si oui ou non deux termes du lambda-calcul sont β-équivalents, ou de façon similaire, l'identité de deux termes de la logique combinatoire. Son indécidabilité a été prouvée par Alonzo Church.
  • Le problème de correspondance de Post est indécidable.

Théories décidables

Une théorie axiomatique est décidable s'il existe un algorithme qui réponde toujours par oui ou non à la question de savoir si un énoncé donné est démontrable dans cette théorie. Un tel algorithme peut être facilement étendu en un algorithme de recherche de démonstration formelle (sous la condition, vérifiée par les théories « usuelles », que le fait d'être un axiome soit décidable) : une fois que l'on sait qu'un énoncé est démontrable, il suffit d'énumérer toutes les démonstrations bien formées jusqu'à trouver une démonstration de cet énoncé. Cet algorithme de recherche n'a bien sûr qu'un intérêt théorique, sauf dans des cas particulièrement simples.

Même si une théorie est décidable, la complexité algorithmique de sa décision peut être rédhibitoire.

Exemples de théories décidables :

  • la théorie des corps réels clos, avec des algorithmes basés sur l'élimination des quantificateurs, qui produisent au vu d'un énoncé un énoncé équivalent sans quantificateurs ∀ ou ∃ ; les énoncés sans quantificateurs de la théorie sont trivialement décidables ; la complexité des algorithmes connus est élevée et ne permet que la décision d'énoncés très simples ;
  • l'arithmétique de Presburger (arithmétique entière sans multiplication, ou, ce qui revient au même, avec multiplication restreinte au cas où l'un des opérandes est une constante)[6].

Décidabilité logique et décidabilité algorithmique

Les deux notions de décidabilité interprètent chacune la notion intuitive de décision dans des sens clairement différents. Elles sont cependant liées.

On considère en effet en mathématiques qu'une démonstration, si elle peut être difficile à trouver, doit être « facile » à vérifier, en un sens très informel (et discutable — mais ce n'est pas l'objet de cet article). Quand on formalise, on traduit ceci en demandant que le problème de reconnaître si un assemblage de phrases est une démonstration formelle soit décidable. Pour que ceci soit exact, il faut supposer que l'ensemble des axiomes de la théorie est décidable, ce qui, on l'a déjà mentionné, est très naturel. Sous cette hypothèse, l'ensemble des théorèmes d'une théorie devient récursivement énumérable ; une telle théorie, si elle est complète, est alors décidable (voir article théorie axiomatique pour des justifications et détails supplémentaires).

En revanche, une théorie décidable n'est pas nécessairement complète. Ainsi, la théorie des corps algébriquement clos n'est pas complète, puisque la caractéristique n'est pas précisée : ainsi l'énoncé du premier ordre 1 + 1 = 0 n'est pas conséquence de la théorie, puisqu'il existe des corps algébriquement clos de caractéristique différente de 2, et l'énoncé du premier ordre 1 + 1 ≠ 0 ne l'est pas non plus, puisqu'il existe des corps algébriquement clos de caractéristique 2[7]. Mais la théorie des corps algébriquement clos est décidable[8]. La théorie des corps algébriquement clos d'une caractéristique donnée est, quant à elle, complète[2] et décidable.

Vérité et décidabilité

Pour pouvoir comparer utilement ces deux notions, il faut disposer d'une définition rigoureuse de la notion de vérité ; celle-ci a été formulée par Alfred Tarski. En logique (du premier ordre) on dit qu'un énoncé est vrai dans un modèle donné de la théorie s'il est satisfait (en un sens technique, mais assez intuitif) par les objets de ce modèle ; un énoncé démontré est évidemment vrai dans tout modèle, et pour une théorie cohérente, la réciproque est vraie : c'est le théorème de complétude de Gödel. La situation est nettement plus complexe pour des énoncés indécidables : il existe (en prenant la réciproque du résultat précédent) des modèles dans lesquels ils sont vrais et des modèles dans lesquels ils sont faux (exhiber de tels modèles est d'ailleurs une des façons classiques de prouver l'indécidabilité), et, la plupart du temps, il n'y a pas d'argument permettant de préférer un cas à un autre ; c'est par exemple, en géométrie, le cas de l'axiome des parallèles. Cependant, les énoncés arithmétiques ont un statut particulier : un énoncé de la forme "pour tout n entier, P(n) est vraie" (par exemple « n>5 est somme de trois nombres premiers »), s'il est indécidable, est nécessairement vrai (dans l'ensemble des entiers "naïfs", appelés souvent les entiers standard), car sinon, un contre-exemple fournirait une démonstration effective de sa négation. Partant de ce constat, toute une théorie logique délicate, l'étude de la hiérarchie arithmétique, a été développée par Stephen Cole Kleene.

Notes et références
  1. Euclide, Les Éléments, livre I, postulat 5.
  2. On le montre facilement par le théorème de Vaught, par exemple Chang et Keisler 1990, p. 139-140 ou ces notes de cours d'Elisabeth Bouscaren à Paris-Sud.
  3. Chang et Keisler 1990, p. 344.
  4. Annoncée en Chang et Keisler 1990, p. 43, exercice du chapitre 5.
  5. Cori et Lascar, Logique Mathématique, Tome 2, Chapite 6 "Théorème de Gödel", paragraphe 3.8
  6. Rabin et Fischer ont démontré en 1974 que n'importe quel algorithme de décision pour l'arithmétique de Presburger possède un pire cas avec un temps d'exécution supérieur à , pour une constante c > 0.
  7. Il s'agit de logique du premier ordre. Pour chaque entier premier p, le fait qu'un corps a pour caractéristique p s'énonce au premier ordre par un seul axiome de la forme 1 + … + 1 = 0. Pour la caractéristique 0, il faut une infinité d'axiomes (toutes les négations des précédents).
  8. La décidabilité a été démontrée par élimination des quantificateurs, par Alfred Tarski en 1948 dans A Decision Method for Elementary Algebra and Geometry, selon Chang et Keisler 1990, p. 58.

Voir aussi

Bibliographie
  • Olivier Carton, Langages formels, calculabilité et complexité, [détail de l’édition] (lire en ligne)
  • Jean-Michel Autebert, Calculabilité et décidabilité, Dunod, 1992 (ISBN 978-2225826320)
  • Pierre Wolper, Introduction à la calculabilité, 3e éd., Dunod, 2006 (ISBN 978-2100499816)
  • (en) C. C. Chang et H. Jerome Keisler, Model Theory, Amsterdam/New York/New York, NY, USA, Elsevier, coll. « Studies in Logic and the Foundations of Mathematics », , 3e éd. (1re éd. 1973) (ISBN 978-0-444-88054-3, lire en ligne)

Articles connexes

Lien externe

« Les limites théoriques de l'informatique. Les problèmes indécidables » Cycle de trois leçons dispensées par Jean-François Raskin, Samuel Fiorini et Gilles Geeraerts au Collège Belgique de l'Académie royale des sciences, des lettres et des beaux-arts de Belgique.

  • Portail de la logique
  • Portail de l'informatique théorique
Cet article est issu de Wikipedia. Le texte est sous licence Creative Commons - Attribution - Partage dans les Mêmes. Des conditions supplémentaires peuvent s'appliquer aux fichiers multimédias.