Problème de la décision
De Wikipedia, l'encyclopédie encyclopedia
Ne doit pas être confondu avec Problème de décision.
En logique mathématique, on appelle problème de la décision ou, sous son nom d'origine en allemand, Entscheidungsproblem, 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é).
Cet article ne cite pas suffisamment ses sources ().
Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références ».
En pratique : Quelles sources sont attendues ? Comment ajouter mes sources ?
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.