Problème de la décision

Un article de Wikipédia, l'encyclopédie libre.
Sauter à la navigation Sauter à la recherche

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 sans autres axiomes que ceux de l'égalité (exemples : système à la Hilbert, calcul des séquents, déduction naturelle). De façon équivalente par le théorème de complétude, il s'agit finalement de savoir si un énoncé est universellement valide, c’est-à-dire vrai dans tous les modèles (de l'égalité).

Le problème de décision est une question de décidabilité algorithmique. Autrement dit, 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 fut posé par David Hilbert et Wilhelm Ackermann en 1928

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, les symboles de constantes, de fonctions (ou opérations), et de prédicat (par exemple, 0, +, ≤, …).

Dans un langage donné (exemple : dans l'arithmétique de Peano c'est le langage arithmétique), 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 (*).

Histoire[modifier | modifier le code]

La question du problème de décision remonte à Gottfried Wilhelm Leibniz qui, au XVIIe siècle, imaginait la construction d'une machine qui pouvait manipuler des symboles (qui plus tard seront ceux de constantes, de fonctions,...) afin de déterminer les valeurs des énoncés mathématiques. Il comprit que le premier pas serait d'avoir un langage formel clair (dont le problème dépend).

Exemple : arithmétique de Peano[modifier | modifier le code]

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.

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). Ils déduisirent 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.

A. Church[modifier | modifier le code]

Pour répondre de manière négative à la question, Church s'appuie essentiellement sur le théorème de Gödel-Rosseret des méthodes développées par Gödel pour démontrer le premier théorème d'incomplétude. Le résultat énoncé est :

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 les examine, 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, + , ×).

A. Turing[modifier | modifier le code]

Rappelons l'apparition de plusieurs modèles de calcul dans les années 1930 (on peut citer les fonctions λ-calculables de Church (1930), les fonctions récursives générales de Herbrand et Gödel (1931 - 1934), les machines de Turing (1936)), qui se révèlent être tous équivalents, et permettent de définir une fonction calculable, c'est-à-dire qui se calcule mécaniquement, par un algorithme par exemple.

Pour montrer l'indécidabilité de l'arithmétique, l'argumentation d'Alan Turing est la suivante : il suppose par l'absurde avoir un algorithme de décision pour l'arithmétique de Peano. Or la question de savoir si une machine de Turing donnée s'arrête ou non peut s'écrire comme énoncé de premier ordre (grâce aux méthodes développées par Gödel). Alors cet énoncé sera résolu par l'algorithme de décision. Or Turing avait démontré qu'il n'existe aucun algorithme pour décider de l'arrêt d'une machine de Turing. Il y a absurdité : le calcul de prédicat égalitaire du premier ordre dans le langage arithmétique est indécidable.

Voir aussi[modifier | modifier le code]

Références[modifier | modifier le code]

Sources[modifier | modifier le code]

En français[modifier | modifier le code]

  • 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[modifier | modifier le code]

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

Articles originaux[modifier | modifier le code]