Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Problème de la décision
Résumé
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é).
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.
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).
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.