Problème de la décision

Problème de la décision


En logique mathématique, on appelle problème de la décision le fait de déterminer de façon mécanique, par un algorithme, si un énoncé est un théorème de la logique égalitaire du premier ordre, c’est-à-dire s'il se dérive dans un système de déduction (voir système à la Hilbert, calcul des séquents, déduction naturelle), sans autres axiomes que ceux de l'égalité. De façon équivalente par le théorème de complétude, il s'agit de savoir si un énoncé est universellement valide, c’est-à-dire vrai dans tous les modèles (de l'égalité). Il s'agit de décidabilité algorithmique. Dit autrement, la question est celle de la décidabilité du calcul des prédicats égalitaire du premier ordre : l'ensemble des énoncés universellement valides du calcul des prédicats du premier ordre est-il décidable ?

Le problème de la décision dépend en fait du choix du langage du premier ordre : sa signature, les "briques" de base, qui permettent la construction des énoncés, symboles de constantes, de fonctions (ou opérations), et de prédicat (ou relation), par exemple, 0, +, ≤, ....

On parle aussi du problème de la décision dans une théorie axiomatique donnée, par exemple dans l'arithmétique de Peano. IL s'agit alors de déterminer si un énoncé est un théorème de la théorie en question. Dans un langage donné, une solution positive au problème de la décision fournit une solution positive aux problèmes de la décision pour toutes les théories finiment axiomatisables de ce langage. En effet, un énoncé C se déduit d'un système fini d'axiomes si et seulement si on peut dériver en logique pure que la conjonction de ces axiomes entraîne C.

Le problème fut posé par David Hilbert et Wilhelm Ackermann en 1928. On utilise d'ailleurs parfois le terme allemand Entscheidungsproblem pour désigner le problème de la décision, c'est le cas très souvent en anglais, pour éviter les confusions.

La question remonte à Gottfried Leibniz qui, au dix-septième siècle, imaginait la construction d'une machine qui pouvait manipuler des symboles afin de déteminer les valeurs des énoncés mathématiques. Il comprit que le premier pas serait d'avoir un langage formel clair.

Alonzo Church et Alan Turing donnèrent (indépendamment) en 1936, une réponse négative au problème de la décision pour l'arithmétique (par exemple l'arithmétique de Peano ou une théorie cohérente plus forte). Ils utilisent largement les méthodes développées par Kurt Gödel pour démontrer le premier théorème d'incomplétude. On peut énoncer ainsi le résultat :

Une théorie récursivement axiomatisable, cohérente et capable de "formaliser l'arithmétique", est algorithmiquement indécidable.

Les conditions précises du théorème sont celles du théorème de Gödel-Rosser. Si l'on examine ces conditions, on se rend compte qu'elles sont réalisées par une théorie finiment axiomatisable, et donc on obtient une réponse négative au problème de la décision dans le langage de l'arithmétique (on peut prendre 0, 1, + , ×). Ce résultat est souvent appelé théorème de Church :

Le calcul des prédicats égalitaire du premier ordre dans le langage de l'arithmétique est algorithmiquement indécidable.

On en déduit par codage une réponse négative pour le problème de la décision dès que le langage contient un symbole de prédicat binaire (en plus de l'égalité). Par contre si le langage ne contient que des symboles de prédicats unaires et des symboles de constante (pas de symboles de fonction), alors le calcul des prédicats égalitaire du premier ordre correspondant, le calcul des prédicats monadiques du premier ordre, est décidable.

Par ailleurs, il existe des théories décidables dont le langage contient un symbole de prédicat binaire : la théorie des ordres denses (celle de Q l'ensemble des rationnels dans le seul langage de l'ordre) pour prendre un exemple très simple, ou encore l'arithmétique de Presburger à laquelle on peut ajouter sans dommage la relation d'ordre, qui se définit avec l'addition.

Pour répondre à la question, surtout pour y répondre négativement, il fallait cependant que la notion de fonction calculable, c’est-à-dire calculable mécaniquement, par un algorithme, soit formalisée. Cela s'est fait en plusieurs étapes. Plusieurs modèles de calcul, que l'on dirait maintenant Turing-complets, sont apparus dans les années 1930. On peut citer les fonctions λ-calculables d'Alonzo Church (1930), les fonctions récursives générales de Herbrand et Gödel (Gödel 1934, en précisant une idée de Herbrand 1931), les machines de Turing (1936), les systèmes de Post (1936), les fonctions récursives au sens de Kleene (1936)... Tous ces modèles se sont révélés équivalents, ce qui est un argument pour la thèse de Church (1936) : on a bien capturé par l'un de ces modèles la notion de fonction calculable.

Pour montrer l'indécidabilité de l'arithmétique, l'argumentation d'Alan Turing est la suivante. Supposons que nous ayons un algorithme de décision pour l'arithmétique de Peano. La question de savoir si une machine de Turing donnée s'arrête ou non, peut être formulée comme un énoncé du premier ordre (on utilise les méthodes développées par Gödel), lequel serait alors résolu par l'algorithme de décision. Mais Turing avait prouvé précédemment qu'il n'y a pas d'algorithme général pour décider de l'arrêt d'une machine de Turing.

Voir aussi

Références

Sources

En Français

  • 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]
    Fonctions récursives au sens de Kleene, Théorème de Church…
  • Jean-Pierre Azra et Bernard Jaulin, Récursivité, Gauthier-Villars, 1973 (ISBN 2-04-007244-6)
    Théorème de Church, théories décidables et indécidables…

En Anglais

  • S.C. Kleene - Introduction to metamathematics - Elsevier - 1952 - (ISBN 0720421039) (réédité)

Articles originaux

  • Alonzo Church, « An unsolvable problem of elementary number theory », American Journal of Mathematics, 58 (1936), pp 345–363
  • Alonzo Church, « A note on the Entscheidungsproblem », Journal of Symbolic Logic, 1 (1936), pp 40–41.
  • Alan Turing, « On computable numbers, with an application to the Entscheidungsproblem », Proceedings of the London Mathematical Society, Series 2, 42 (1936), pp 230–265. Online version. Errata appeared in Series 2, 43 (1937), pp 544–546.

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Problème de la décision de Wikipédia en français (auteurs)

Игры ⚽ Поможем написать курсовую

Regardez d'autres dictionnaires:

  • Probleme de la decision — Problème de la décision En logique mathématique, on appelle problème de la décision le fait de déterminer de façon mécanique, par un algorithme, si un énoncé est un théorème de la logique égalitaire du premier ordre, c’est à dire s il se dérive… …   Wikipédia en Français

  • DÉCISION — La réflexion moderne sur la question de savoir quel parti prendre lorsqu’on se trouve confronté à un choix difficile a été esquissée pour la première fois par Blaise Pascal, au XVIIe siècle, dans le fameux texte du «pari» sur l’entrée dans la… …   Encyclopédie Universelle

  • Problème décisionnel — Décision La décision est le fait d effectuer un choix lors de la confrontation à un problème afin de le résoudre. Il existe au moins trois grandes approches du concept de décision : La première estime que la décision est un choix de type… …   Wikipédia en Français

  • Decision — Décision La décision est le fait d effectuer un choix lors de la confrontation à un problème afin de le résoudre. Il existe au moins trois grandes approches du concept de décision : La première estime que la décision est un choix de type… …   Wikipédia en Français

  • Probleme de decision — Problème de décision On parle de problème de décision dans des contextes variés. Cet article est destiné à décrire ce terme en informatique, ou en mathématiques. En algorithmique, un problème de décision est une question mathématiquement définie… …   Wikipédia en Français

  • Décision — « Décidé » redirige ici. Pour le navire corsaire, voir Le Décidé. La décision est le fait d un acteur (ou d un ensemble plus ou moins cohérent d acteurs) qui effectue un choix entre plusieurs solutions susceptibles de résoudre le… …   Wikipédia en Français

  • Problème P = NP — En mathématiques, et plus précisément en informatique théorique, la relation entre la classe des problèmes de complexité P et la classe des problèmes de complexité NP est un problème non résolu, et est considéré par de nombreux chercheurs comme… …   Wikipédia en Français

  • Problème de décision — On parle de problème de décision dans des contextes variés. Cet article est destiné à décrire ce terme en informatique, ou en mathématiques. En algorithmique, un problème de décision est une question mathématiquement définie portant sur des… …   Wikipédia en Français

  • Probleme du sac a dos — Problème du sac à dos Le problème du sac à dos : quelles boîtes choisir afin de maximiser la somme emportée tout en ne dépassant pas les 15 kg autorisés ? Le problème du sac à dos, noté également KP (en anglais, Knapsack Problem) est un …   Wikipédia en Français

  • problème — [ prɔblɛm ] n. m. • 1382; lat. problema, du gr. problêma 1 ♦ Question à résoudre qui prête à discussion, dans une science. Problèmes philosophiques, moraux, métaphysiques. Le problème du mal. Soulever un problème. C est là la clé, le nœud du… …   Encyclopédie Universelle

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”