Entscheidungsproblem

Entscheidungsproblem

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 de 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

References

Sources

En Français

  • René Cori, Daniel Lascar, Logique mathématique (tome II) - Masson - 1994 - ISBN 2-225-84080-6

fonctions récursives au sens de Kleene, Théorème de Church ....

  • Jean-Pierre Azra, 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.
Ce document provient de « Probl%C3%A8me de la d%C3%A9cision ».

Wikimedia Foundation. 2010.

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

Игры ⚽ Поможем написать реферат

Regardez d'autres dictionnaires:

  • Entscheidungsproblem — Saltar a navegación, búsqueda El Entscheidungsproblem (en castellano: problema de decisión) fue el reto en lógica simbólica de encontrar un algoritmo general que decidiera si una fórmula del cálculo de primer orden es un teorema. En 1936, de… …   Wikipedia Español

  • Entscheidungsproblem — In mathematics, the Entscheidungsproblem (pronounced [ɛntˈʃaɪdʊŋspʁoˌbleːm], German for decision problem ) is a challenge posed by David Hilbert in 1928. The Entscheidungsproblem asks for an algorithm that will take as input a description of a… …   Wikipedia

  • Entscheidungsproblem — Eine Eigenschaft auf einer Menge heißt entscheidbar (auch: rekursiv), wenn es ein Entscheidungsverfahren für sie gibt. Ein Entscheidungsverfahren ist ein Algorithmus, der für jedes Element der Menge beantworten kann, ob es die Eigenschaft hat… …   Deutsch Wikipedia

  • Entscheidungsproblem — noun /ɛntˈʃʌɪdʊŋsˌpɹɒbləm/ A decision problem, of finding a way to decide whether a formula is true or provable within a given system. ‘The Entscheidungsproblem,’ Rudy said. ‘Meaning?’ Alan explained, ‘Hilbert wanted to know whether any given… …   Wiktionary

  • Entscheidungsproblem — El Entscheidungsproblem (en castellano: problema de decisión) fue el reto en lógica simbólica de encontrar un algoritmo general que decidiera si una fórmula del cálculo de primer orden es un teorema. En 1936, de manera independiente, Alonzo… …   Enciclopedia Universal

  • Entscheidungsproblem — …   Useful english dictionary

  • Markov-Entscheidungsproblem — Bei dem Markow Entscheidungsproblem (MEP, auch Markow Entscheidungsprozess) handelt es sich um ein nach dem russischen Mathematiker Andrei Andrejewitsch Markow benanntes Modell von Entscheidungsproblemen, bei denen der Nutzen eines Agenten von… …   Deutsch Wikipedia

  • Markow-Entscheidungsproblem — Bei dem Markow Entscheidungsproblem (MEP, auch Markow Entscheidungsprozess) handelt es sich um ein nach dem russischen Mathematiker Andrei Andrejewitsch Markow benanntes Modell von Entscheidungsproblemen, bei denen der Nutzen eines Agenten von… …   Deutsch Wikipedia

  • Anfragenselektion — Entscheidungsproblem im Rahmen des Investitionsgüter Marketing, bes. bei Sondermaschinen, Anlagen und Systemen. Da die Angebotserstellung aufgrund einer Anfrage mit erheblichen Kosten verbunden ist und die Auftragserteilung schwerwiegende… …   Lexikon der Economics

  • Turing machine — For the test of artificial intelligence, see Turing test. For the instrumental rock band, see Turing Machine (band). Turing machine(s) Machina Universal Turing machine Alternating Turing machine Quantum Turing machine Read only Turing machine… …   Wikipedia

Share the article and excerpts

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