On peut faire strictement la même chose avec les fonctions récursives qu'avec la machine de Turing, donc oui, elles sont simulables. Il me semble d'ailleurs qu'elles ont été le premier modèle de calcul proposé.
Je ne sais pas si comprends bien ce qui est entendu par "résoluble de façon non-algorithmique". Revenons aux glorieux systèmes équations diophantiennes.Il est clair que si tu limites le mot "résoluble" à "résoluble à l'aide d'un ordinateur", le raisonnement basé sur l'emploi de "résoluble, mais seulement de façopn non algorithmique" ne veut rien dire pour toi. Seulement les mathématiques non seulement ont existé avant les ordinateurs, mais elles continuent à explorer des problèmes inaccessibles aux ordinateurs. Justement pardce que le cerveau humain est autre chose qu'un ordinateur.
Le fait qu'une machine de Turing ne puisse pas résoudre un système est prouvé. Dans le monde merveilleux des mathématiques je veux dire.
Donc maintenant, prenons Conan le mathématicien, donnons-lui un système, demandons-lui s'il existe une solution ou non. Ce que je crois comprendre de vos idées est : Conan finira par répondre à la question de façon juste, si on lui laisse assez de temps. Peu importe comment il s'y prend (voyage astral chamanique par exemple), au bout d'un certain laps de temps, il revient vers nous avec sa preuve. C'est ça ?
Je ne suis pas très au fait de ce qu'on considère être une preuve mathématique formelle. Je crois me souvenir qu'une preuve est une série de dérivations respectant les règles d'inférence menant de l'énoncé à une tautologie.
Donc question : si on se donne les axiomes qui vont bien et les règles d'inférence de bon goût, est-ce que l'ensemble des preuves ne serait pas un peu énumérable ? (vraie question sans malice)
Supposons que oui, pour le plaisir de la conversation (car j'y prends plaisir, ne nous leurrons pas) (et puis mine de rien, ça me semble relativement plausible).
Maintenant laissons du temps à Conan. Il finit par prouver que le système est résoluble (ou pas), il a une preuve. Qui a un certain numéro dans la liste des preuves. Mettons que c'est la 42 tenez, ça nous amusera.
Machinette (c'est le petit nom de la machine de Turing), peut énumérer les preuves, elle le fait. En arrivant à la 42, pouf, elle remarque qu'elle prouve que le système qu'on lui a fourni a une solution (ou pas).
Machinette 1 - 1 Conan
Bon ça c'est un peu emmerdant, parce que ça veut dire que Machinette a une méthode toute conne pour prouver qu'un système d'équations diophantiennes a une solution ou pas : elle énumère les preuves et puisque Conan est capable de prouver pour tout système d'équations diophantiennes qu'il a une solution (ou pas), Machinette pourra toujours trouver une preuve de l'existence (ou pas) de solution à tout système. Ce qui est impossible, puisque Machinette ne peut pas décider ce problème.
Ce qui impliquerait que Conan, en fait, ne peut pas, pour tout système d'équations diophantiennes, arriver à déterminer si oui ou non il possède une solution. Ou du moins, il ne peut pas l'exprimer par une preuve formelle, ce qui est embêtant, parce que du coup il ne peut pas convaincre les joyeux cimmériens que la preuve est vraie.
Il serait donc préférable que l'ensemble des preuves ne soit pas énumérable. Sauf que quand même, à bien y penser, je crois volontiers qu'il l'est, l'ensemble des preuves écrites en français châtié étant indubitablement énumérable.
Tiens c'est pas mal comme argument ça.
Et donc du coup, hop, je serais quand même très tenté de croire que non, Conan ne peut pas décider dans le cas général qu'un système d'équations diophantiennes est résoluble ou pas. Ou bien, s'il le peut (par exemple en évoquant les mânes de ses ancêtres), il ne pourra pas en convaincre ses petits camarades au moyen d'une preuve mathématique, ce qui est un peu chiant, parce que du coup ce ne sont plus des maths.
