Problème de la décision
Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs de cet article est disponible ici.

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 (En 1935 Gentzen a proposé la déduction naturelle, un formalisme pour décrire les preuves du calcul des prédicats, dont l'idée était de coller au...), déduction naturelle), sans autres axiomes que ceux de l'égalité. De façon équivalente par le théorème (Un théorème est une proposition qui peut être mathématiquement démontrée, c'est-à-dire une assertion qui peut être établie comme vraie au travers d'un raisonnement logique construit à partir d'axiomes. Un théorème...) de complétude (On parle de complétude en mathématiques dans des sens très différents. On dit d'un objet mathématiques qu'il est complet pour exprimer que rien ne peut lui être ajouté, en un sens qu'il faut préciser dans chaque...), 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 (L'algorithmique est l’ensemble des règles et des techniques qui sont impliquées dans la définition et la conception d'algorithmes, c'est à dire de...). Dit autrement, la question est celle de la décidabilité du calcul des prédicats égalitaire du premier ordre : l'ensemble (En théorie des ensembles, un ensemble désigne intuitivement une collection d’objets (les éléments de l'ensemble), « une multitude qui peut être comprise comme un tout », comme...) des énoncés universellement valides du calcul des prédicats du premier ordre est-il décidable ?

Le 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...) 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 (Les prédicats d’une théorie sont les formules qui contiennent des variables libres.) (ou relation), par exemple, 0, +, ≤, ....

On parle aussi du problème de la décision dans une théorie (Le mot théorie vient du mot grec theorein, qui signifie « contempler, observer, examiner ». Dans le langage courant, une théorie est une idée ou une connaissance...) axiomatique donnée (Dans les technologies de l'information, une donnée est une description élémentaire, souvent codée, d'une chose, d'une transaction, d'un événement, etc.), par exemple dans l'arithmétique (L'arithmétique est une branche des mathématiques qui comprend la partie de la théorie des nombres qui utilise des méthodes de la géométrie algébrique et de la théorie des groupes. On...) 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 (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la fois raison,...) 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 (Un siècle est maintenant une période de cent années. Le mot vient du latin saeculum, i, qui signifiait race, génération. Il a ensuite indiqué la durée d'une génération humaine et faisait 33 ans...), 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 (Dans de nombreux contextes (scientifique, légal, etc.) l'on désigne par langage formel un mode d'expression plus formalisé et plus précis (les deux n'allant pas nécessairement de pair) que le langage de tous les jours (voir langage...) clair.

Alonzo Church (Alonzo Church 14 juin 1903 - 11 août 1995 fut un mathématicien (logicien) américain à qui l'on doit certains des fondements de l'informatique théorique.) et Alan Turing (Alan Mathison Turing (23 juin 1912 - 7 juin 1954) est un mathématicien britannique, auteur de l'article fondateur de la science informatique qui...) 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 parle de complétude en mathématiques dans des sens très différents. On dit d'un objet mathématiques qu'il est complet pour exprimer que rien ne peut lui être ajouté, en...). 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 (De façon générale un codage permet de passer d'une représentation des données vers une autre.) 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 (En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique.).

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 (L'arithmétique de Presburger est une théorie du premier ordre, dans le langage de l'arithmétique de Peano sans la multiplication, c’est-à-dire avec seulement...) à laquelle on peut ajouter sans dommage la relation d'ordre, qui se définit avec l'addition (L'addition est une opération élémentaire, permettant notamment de décrire la réunion de quantités ou l'adjonction de grandeurs...).

Pour répondre à la question, surtout pour y répondre négativement, il fallait cependant que la notion de fonction calculable (Une fonction calculable (ou fonction récursive) est une fonction semi-calculable (ou fonction partielle récursive) qui est aussi totale, c'est-à-dire définie pour toute entrée (en tout point). Ce sont les fonctions...), 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 (SENS (Strategies for Engineered Negligible Senescence) est un projet scientifique qui a pour but l'extension radicale de l'espérance de vie humaine. Par une évolution...) de Kleene (1936)... Tous ces modèles se sont révélés équivalents, ce qui est un argument pour la thèse (Une thèse (du nom grec thesis, se traduisant par « action de poser ») est l'affirmation ou la prise de position d'un locuteur, à l'égard du sujet ou du thème qu'il évoque.) de Church (1936) : on a bien capturé par l'un de ces modèles la notion de fonction calculable.

Pour montrer l'indécidabilité (En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique.) 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.

Page générée en 0.090 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique