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 :
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 :
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.