Bonjour,
dans le cadre de la discussion (indécidébilité de la décidabilité) j'en suis venu à me poser une autre question :
y a-t-il coïncidence entre la décidabilité logique et la décidabilité algorithmique ???
je suppose ici que la décidabilité logique, ou décidabilité au sens de Gödel, se dit d'un énoncé qui est prouvable ou réfutable à partir d'une théorie T dans un langage L.
La décidabilité algorithmique, ou décidabilité au sens de Turing, se dit d'un énoncé pour lequel il existe un algorithme (une machine de Turing) qui termine nécessairement en décidant de l'énoncé, en disant s'il est vrai ou non dans une théorie T sur un langage L.
Je suppose (contredites moi si je me trompe) que la décidabilité algorithmique implique la décidabilité logique, il me semble que c'est plutôt la réciproque qui pose problème pour cette "coïncidence"....
Par exemple : connait-on un langage L, une théorie T et une formule F sur L qui soit décidable au sens de Gödel et ne le soit pas au sens de Turing ?
Question parallèle : répondre oui à ma question n'est-il pas équivalent à affirmer la thèse de Church ??
-----