Entscheidungsproblem

Carte Commune · n° 267816

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

Lire sur Wikipédia