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

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

Concepts associés (39)

Cours associés (6)

Séances de cours associées (41)

Problème de la décision

Machine de Turing

En informatique théorique, une machine de Turing est un modèle abstrait du fonctionnement des appareils mécaniques de calcul, tel un ordinateur. Ce modèle a été imaginé par Alan Turing en 1936, en vue de donner une définition précise au concept d’algorithme ou de « procédure mécanique ». Il est toujours largement utilisé en informatique théorique, en particulier dans les domaines de la complexité algorithmique et de la calculabilité.

Théorèmes d'incomplétude de Gödel

Les théorèmes d'incomplétude de Gödel sont deux théorèmes célèbres de logique mathématique, publiés par Kurt Gödel en 1931 dans son article (« Sur les propositions formellement indécidables des Principia Mathematica et des systèmes apparentés »). Ils ont marqué un tournant dans l'histoire de la logique en apportant une réponse négative à la question de la démonstration de la cohérence des mathématiques posée plus de 20 ans auparavant par le programme de Hilbert.

MATH-483: Gödel and recursivity

Gödel incompleteness theorems and mathematical foundations of computer science

MATH-318: Set theory

Set Theory as a foundational system for mathematics. ZF, ZFC and ZF with atoms. Relative consistency of the Axiom of Choice, the Continuum Hypothesis, the reals as a countable union of countable sets,

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

Coq: Introduction

Présente Coq, couvrant la définition des propositions, la démonstration des théorèmes, et l'utilisation de tactiques.

Fonctions harmoniques sub/super MATH-305: Introduction to partial differential equations

Explore les fonctions sub/super harmoniques et leurs applications dans un contexte théorique.

Théorie de calcul : problèmes de comptage et de décision CS-119(c): Information, Computation, Communication

Explore le comptage des ensembles infinis et les problèmes de décision, montrant les limites du calcul dans la résolution de certains problèmes indécis.