Ê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
Décidabilité
Résumé
En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique.
L’indécidabilité est la négation de la décidabilité. Dans les deux cas, il s'agit de formaliser l'idée qu'on ne peut pas toujours conclure lorsque l'on se pose une question, même si celle-ci est sous forme logique.
Une proposition (on dit aussi énoncé) est dite décidable dans une théorie axiomatique si on peut la démontrer ou démontrer sa négation dans le cadre de cette théorie. Un énoncé mathématique est donc indécidable dans une théorie s'il est impossible de le déduire, ou de déduire sa négation, à partir des axiomes de cette théorie. Pour distinguer cette notion d'indécidabilité de la notion d'indécidabilité algorithmique (voir ci-dessous), on dit aussi que l'énoncé est indépendant du système d'axiomes. C'est le cas notamment du célèbre postulat des parallèles d'Euclide, relativement à sa géométrie, ou encore de l'hypothèse du continu relativement à la théorie des ensembles usuelle, selon laquelle il n'y a pas de cardinal entre celui de l'ensemble des entiers naturels et celui de l'ensemble des nombres réels, dont Paul Cohen a démontré, en 1963, qu'elle était indécidable.
En logique classique, d'après le théorème de complétude, une proposition est indécidable dans une théorie s'il existe des modèles de la théorie où la proposition est fausse et des modèles où elle est vraie. On utilise souvent des modèles pour montrer qu'un énoncé est indépendant d'un système d'axiomes (dans ce cadre, on préfère employer indépendant plutôt quindécidable). La propriété utilisée dans ce cas n'est pas le théorème de complétude mais sa réciproque, très immédiate, appelée théorème de correction. C'est d'ailleurs ainsi qu'apparut pour la première fois la notion de modèle, avec la construction au par Eugenio Beltrami de modèles de géométries non euclidiennes (qu'il appelait des représentations) ne vérifiant pas l'axiome des parallèles, et leur utilisation, en admettant le fait, assez intuitif, que la géométrie euclidienne est cohérente, pour démontrer que l'axiome des parallèles est indépendant des autres axiomes de la géométrie, ou encore indécidable dans le système formé des axiomes restants.
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.