Problème de la décision

En logique mathématique, on appelle problème de la décision ou, sous son nom d'origine en allemand, , 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 la décision est un exemple de problème de décision : une question de décidabilité au sens algorithmique. Ici 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, 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 
La question du problème de décision remonte à Gottfried Wilhelm Leibniz qui, au , 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).

En 1928, David Hilbert et Wilhelm Ackermann posent le problème de la décision tel que nous le connaissons aujourd'hui.

En 1936, Alan Turing et Alonzo Church donnent chacun une réponse négative à ce problème pour l'arithmétique.

Exemple : arithmétique de Peano 
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 constantes (pas de symboles de fonctions), alors le calcul des prédicats du premier ordre égalitaire 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 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.

Alonzo Church 
Pour répondre de manière négative à la question, Church s'appuie essentiellement sur le théorème de Gödel-Rosser et 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 : 

Les conditions précises du théorème sont celles du théorème de Gödel-Rosser. Si on les examine, on se rend compte qu'elles sont réalisées par une théorie finiment axiomatisable. Un énoncé est démontrable dans une telle théorie si et seulement si la conjonction des axiomes de cette théorie entraîne cet énoncé. On obtient ainsi une réponse négative au problème de la décision dans le langage de l'arithmétique (on peut prendre 0, 1, + , ×).

Alan Turing 
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 des prédicats du premier ordre égalitaire dans le langage arithmétique est indécidable.

Voir aussi 
 Problème de décision
 Théorème d'incomplétude de Gödel

Références

Sources

En français 
  
 Jean-Pierre Azra et Bernard Jaulin, Récursivité, Gauthier-Villars, 1973

En anglais 
 S. C. Kleene - Introduction to metamathematics - Elsevier - 1952  -  (réédité)
M. Davis - The undecidable - 2004

Articles originaux 
 
 
  et 

Décision
Logique mathématique