Solutions partielles au problème de l'arrêt
Bonjour. Mon niveau en logique est assez faible et je n'utilise pas forcément les bons vocabulaires et concepts. J'ai quand même posé cette question sur CStheory mais il y a quelque chose qui ne leur plait pas, et je n'ai pas compris pourquoi.
On peut donc le reformuler comme ça : une fois qu'on a posé $T_1 = PA$ qui nous donne donc $bb(k)$ pour $k \le K(T_1)$, comment "trouver" $T_2$ telle que $K(T_2) > K(T_1)$ ?
Et je suppose que si on se donne une suite de théories (dont les théorèmes sont récursivement énumérables) $T_n$ telles que pour tout programme $P$ qui ne s'arrête pas, il existe $n$ tel que $T_n$ prouve que $P$ ne s'arrête pas, alors avec $T_n$ on peut calculer la fonction $bb(k)$ du busy beaver pour $k $ inférieur à un certain $K(T_n)$ (on peut calculer des bornes inférieures pour $K(T_n)$), et avec la suite $(T_n)$ on peut donc calculer $bb(k)$ pour tout $k$, si bien que la suite de théories $T_n$ n'est pas "calculable" (il n'existe pas d'algorithme qui les génère toutes).L'idée c'est qu'on nous donne un programme $P$ sans paramètres et on aimerait essayer de trouver si $P$ s'arrête ou pas (par exemple $P$ est la fonction qui énumère les entiers en essayant de trouver un contre-exemple à la conjecture de Goldbach, ou encore qui essaye de trouver une contradiction dans ZFC).
Donc on exécute $P$ et s'il s'arrête on le saura en un temps fini.
En même temps on exécute un algorithme qui "essaye de démontrer" que $P$ ne s'arrête pas. Quel algorithme ? A priori un algorithme qui énumère les théorèmes d'un certain système formel, par exemple PA.
Cela devrait permettre de résoudre le problème de la halte dans une "bonne partie" des cas.
La question est donc : est-ce la façon la plus évidente et élégante de faire ? Si oui, est-ce faisable d'écrire concrètement cet algorithme (qui énumère les théorèmes de PA pour essayer de prouver que $\lnot \text{halt} P$), de discuter en quoi il est "canonique" (ou pas) et comment il serait possible de l'améliorer (en remplaçant PA par une théorie plus forte ?) afin de résoudre le problème de la halte dans un plus grand nombre de cas.
On peut donc le reformuler comme ça : une fois qu'on a posé $T_1 = PA$ qui nous donne donc $bb(k)$ pour $k \le K(T_1)$, comment "trouver" $T_2$ telle que $K(T_2) > K(T_1)$ ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Puisque la halte n'est pas décidable, ça veut dire qu'il n'existe pas de suite croissante et récursive de théories cohérentes récursivement énulérables et telle que pour tout programme $P$, la halte de $P$ est déterminée par ces théories à partir d'un certain rang.
J'ai pas compris qui était tes $K(T_n)$.
Écrire l'algo est très facile une fois qu'on a fixé le système formel. D'autre part l'algo en lui-même ne nous apprend rien: c'est grosso modo un parcours d'arbre.
Donc donnez n'importe quel candidat au titre de "test d'arrêt", il y aura toujours un code source qui lui fait dire le contraire de ce qu'il veut dire.
$T = PA$ permet de calculer $bb(k)$ pour $k \le K(T)$ (où $K(T)+1$ est la taille du plus petit programme dont l'arrêt est indécidable dans $T$). On ne peut pas calculer $K(T)$ mais on peut calculer des bornes inférieures qui convergent vers $K(T)$ en un temps fini.
Donc en pratique quand on se donne $T$ on peut calculer $bb(k)$ pour $k\le K(T)$ et se pose alors le problème de trouver une théorie $T_2$ plus forte telle que $K(T_2) > K(T)$.
A mon avis le problème de l'arrêt c'est le seul moyen de rendre la logique, les théories, les modèles vraiment concrets et accessibles. Si j'ai posé cette question c'est déjà pour voir si j'avais compris.
Si je demande le code c'est parce que : je ne suis pas capable de l'écrire, je suppose que quelqu'un l'a déjà écrit, et que je vois ça comme une base extrêmement concrète pour discuter de logique. Si c'est une simple boucle alors écris-le ! Il arrive souvent qu'on imagine qu'un programme fera moins de 200 lignes et au final 10000 lignes plus tard il n'est toujours pas achevé.
Ma seconde question est comment écrire vite-fait un pseudo-code pour la fonction $\text{provesHalt}$ qui avec une chaîne de caractère $s$ et un programme $P$ teste si dans PA, $s$ démontre que $P$ ne s'arrête pas.
En cherchant 'sequent calculus source code' on trouve des codes en Haskell dont la doc suggère qu'ils s'en approchent peut-être, mais après un survol rapide ils n'ont pas l'air d'être beaucoup plus lisibles que les cours sur le calcul des séquents.
C'est peut-être plus clair écrit comme ça
Si $T$ est une théorie axiomatique, alors on l'utilise pour avoir une solution partielle $\text{StopT}$ au problème de l'arrêt Le premier théorème d'incomplétude de Gödel c'est que si $\text{StopT(ParadoxeT)}$ renvoie une valeur alors celle-ci est forcément absurde.
Donc si $T$ est consistante alors $\text{StopT(ParadoxeT)}$ ne s'arrête pas.
Autrement dit, si $T$ est consistante, alors l'arrêt de $\text{ParadoxeT}$ est indécidable dans $T$.
Proposition : on peut démontrer ce dernier théorème dans ZFC : pour toute théorie axiomatique $T$ (récursivement énumérable, capable de formaliser le problème de l'arrêt), si $T$ est consistante alors $\text{StopT(ParadoxeT)}$ et donc $\text{ParadoxeT}$ ne s'arrête pas.
Ce qui donne le second théorème d'incomplétude de Gödel : si ZFC prouve sa propre consistance, alors ZFC prouve que $\text{ParadoxeZFC}$ ne s'arrête pas, et donc $\text{StopZFC(ParadoxeZFC)}$ renvoie $0$, ce qui est absurde.
Ma question c'est si cette Proposition est vraiment démontrable dans ZFC ?
Ce qu'il faut introduire en fait c'est des nouveaux axiomes qui caractérisent de manière aussi serrée que possible les "vrais" entiers*. Par exemple, Delahaye avait proposé d'introduire des axiomes de la forme "la complexité de Kolmogorov de $s$ est supèrieure à $k$" avec $s$ une très longue chaîne. En effet, avec très forte probabilité, un tel énoncé est vrai mais pas prouvable. Évidemment, on peut avoir pas de chance et tomber par hasard sur une $s$ qui a faible complexité de Kolmogorov...
*pour ce faire, on pourrait aussi se dire: puisque le premier ordre ne me permet pas de parler de bon ordre, qui est tout de même une propriété fondamentale des "vrais entiers", pourquoi ne pas ajouter le second ordre? Et puis tant que j'y suis, autant mettre aussi le troisième ordre, le quatrième ordre, etc... et puis une fois que j'ai tous les ordres entiers, pourquoi ne pas continuer dans les ordinaux? Mais comme j'ai tout de même envie de rester en logique du premier ordre, je vais gommer au dessus-de chaque quantificateur et de chaque variable le petit $(i)$ qui indique qu'il s'agit d'un quantificateur ou d'une variable d'ordre $i$. Ce faisant, on obtient exactement la théorie des ensembles, qui est effectivement beaucoup plus forte que $PA$.
Je pense que ma "preuve" des théorèmes d'incomplétude de Gôdel est moins fausse en remplaçant "ZFC prouve sa propre consistance" par "ZFC prouve la consistance de ce que répond $\text{StopZFC}$".
Car in fine le problème survient si parmi les théorèmes énumérés par $\text{StopZFC}$, l'un d'eux est que le programme $\text{StopZFC(ParadoxeZFC)}$ ne s'arrête pas, théorème qui est une conséquence de "$\text{StopZFC}$ est consistant en tant que solution partielle au problème de l'arrêt".
Cela devrait être une preuve de "ZFC + consistance de $\text{StopZFC}$ en tant que solution partielle au problème de l'arrêt" est inconsistant,
mais ça ne veut pas dire du tout que ZFC + Cons(ZFC) soit inconsistant.
Que pour tout programme $p$, si $\text{StopT}(p)$ renvoie $1$ alors $p$ s'arrête,
et que si $\text{StopT}(p)$ renvoie $0$ alors $p$ ne s'arrête pas.
Ou bien : que pour tout programme $p$ qui s'arrête, $\text{StopT}(p)$ renvoie $1$, et que pour tout programme $p$ qui ne s'arrête pas, $\text{StopT}(p)$ renvoie $0$ ou ne s'arrête pas.
(je n'ai pas vraiment décidé car les deux me semblent à peu près équivalents)
Ce ne sont que des formules d'arithmétiques qui quantifient sur les suites de la forme $a_{n+1} = f(a_n,m)$ où $f$ est une machine de Turing universelle (fixée à l'avance) qui interprète l'entier $m$ comme le code source de $p$ et $a_n$ comme sa mémoire de travail, donc ça ne devrait poser aucun problème de d'écrire tout ça dans PA ou ZFC.
Exercice (très facile pour toi, vu ce que tu as dit sur ta formation) : il existe un programme P de type (disons) entier qui a comme propriété que pour tout entier $n$, $T$ ne prouve pas que P ne donnera pas $n$ à l'exécution.
Il suit par exemple que T ne peut prouver qu'un nombre fini d'énoncés de la forme "s a une complexité au moins égal log(log(log(s)))" où s est une suite finie de 0 et de 1.
En bref, je m'arrête là "chercher à résoudre, même partiellement, le problème de l'arrêt" est un projet qu'il ne faudra pas te vanter d'avoir dans les diners en ville ;-)
Pourquoi n'apprendrais-tu pas un peu de lambda-calcul? Je suis sûr que tu y trouverais un immense plaisir
Et il suffit que l'arrêt d'un seul programme soit indécidable dans $T$ pour avoir que la proportion de programmes dont l'arrêt soit décidable dans $T$ décroisse exponentiellement avec la taille du programme.
Tu prends le point fixe*** de : p fait défiler toutes les preuves (d'une théorie T fixée), et dès qu'il tombe sur une preuve qui conclut que $<<p$ n'affichera par $n>>$, il se dépêche d'afficher $n$.
Un tel programme ne s'arrête pas et évidemment $T$ (sauf si elle est déconnante) ne parvient à exclure aucun des $n$ de la liste des possibles terminaisons de $p$.
Je n'ai pas compris ton dernier argument. Il y a quand-même un peu plus de travail pour parvenir à légitimer un énoncé tel que "presque tous les énoncés sont indécidables".
*** $[x\mapsto (g(x(x)) )] ([x\mapsto (g(x(x)) )]) $ est un point fixe de $g$.
Au départ un programme ne prend pas d'argument (un programme on peut l'exécuter, et pour ce faire, il faut bien avoir fixé ses arguments). Donc un programme qui prend des arguments en entrée, c'est en fait une définition de pleins de programmes, un pour chaque valeur possible des entrées.
On regarde le programme $q_T(p)$ qui énumère les théorèmes de $T$ et dès que l'un d'eux prouve que $p$ ne renverra pas $n$, alors il l'affiche. Donc $q_T(p)$ ne s'arrête pas.
Ensuite tu fais quoi ?
D'autre part, j'ai re-regardé ma "démonstration" des théorèmes d'incomplétude, et je suis assez convaincu qu'elle marche, donc qu'on peut très bien parler uniquement de la consistance de $\text{StopT}$ en tant que solution partielle a problème de l'arrêt, donc de ce que dit $T$ de l'arrêt des programmes, donc des formules $\Sigma_1,\Pi_1$ de la hiérarchie arithmétique. ça me fait me demander ce que je "rate" en regardant uniquement ces formules $\Sigma_1,\Pi_1$.
Sachant que dans tous les cas, pour n'importe quelle formule $f$, on peut regarder l'arrêt du programme qui énumère les théorèmes de $T$ pour essayer de démontrer $f$ ou $\lnot f$.
1) le pas grave: je ne sais quel paradigme et quelles conventions tu utilises pour parler d'informatique, mais tous les programmes sont des fonctions programmables et toutes les fonctions programmables sont des programmes. On a juste une notion d'application qui fait passer de l'un à l'autre: on note $p(q)$ ce qui se passe quand on exécute le programme $p$ après avoir mis $q$ en haut de pile vide. Autrement dit, c'est juste le programme $[push(q); call(p)]$. De plus le "résultat" (ou la valeur, mais bof bof pour le mot valeur) d'un programme est "boucle" (j'invente, c'est peu important, on dit juste qu'il ne s'arrête pas) s'il ne s'arrête pas, et sinon, le contenu du sommet de la pile juste après son exécution.
Bref, il n'y a pas de fonctions distinguées à proprement parler dans cette histoire. On "simule" la poésie syntaxique des maths, par exemple avec la programmation récursive (au sens informatico-nonlogique), etc, mais un programme ce n'est des instructions basiques de tests, lectures et écritures, entrée-sorties. Par exemple, "il n'y a pas" de fonction factorielle, il y a un programme factorielle, qui est le suivant : et quand on veut "faire plaisir aux gens et mettre les petits plats dans les grands, on camoufle ça dans une présentation
function factorielle (paramètre n: entier naturel)
mais c'est du vernis ça.
2) Plus grave: est-ce que tu peux essayer de préciser le plus formellement ce que tu demandes, désires ou autre? Je ne demande qu'à te répondre après que ce sera fait.
Précision pour les autres lecteurs: une pile est une suite de valeurs (en général finie en pratique :-D ).
Après exécution de "pop x", la pile $u=[u_0,u_1,\ldots]$ devient $[u_1,u_2,\ldots]$ et $x$ a pris la valeur $u_0$.
Après exécution de "push x", la pile $u=[u_0,u_1,\ldots]$ devient $[r,u_0,u_2,\ldots]$ où $r$ est la valeur de la mémoire $x$
Pour une théorie T, on regarde Et Un théorème t qui démontre que f_T(f_T,f_T) ne s'arrête pas ou ne renvoie pas n causera l'arrêt de f_T(f_T,f_T) en renvoyant n, donc sera contradictoire,
donc si T est consistante alors f_T(f_T,f_T) ne s'arrête pas,
donc si T est consistante alors pour tout n, T ne démontre pas que f_T(f_T,f_T) ne renverra pas n.
[À ton service. :-) AD]
@reuns: je ne sais pas si je ne suis pas clair mais ta reformulation ne fait pas partie de mon habitude. Tu redis ce que j'ai dit en mettant T en indice et en explicitant le combinateur de point fixe dans notre cas particulier. Mais pourquoi ne pas mettre T en paramètre et admettre une bonne fois pour toute le combinateur de point fixe ? Ça t’économiserait des efforts de pensée non ?
Et sinon je ne sais plus quels désirs souhaites-tu exprimer ici ie quelles questions reste-t-il ?
Le (enfin "un") combinateur de point fixe est défini par :
et pour ce dire, tu n'as pas besoin de documenter f, c'est uniforme, tu as f(p(f)) == p(f) pour toute f.
De même, c'est dommage d'écrire $f_T$ à la place de $f(T)$, non?
Mon but premier c'était d'arriver à comprendre et à formaliser les théories axiomatiques et l'incomplétude en terme de programmes et de leur arrêt, donc d'arriver à faire ça
Maintenant je me pose des questions, je ne sais pas vraiment lesquelles :
- Supposons que "p s'arrête" est bien défini et est soit vrai soit faux, et que T est consistante. Si l'arrêt de p est indécidable dans T (donc p ne s'arrête pas) alors T + "p ne s'arrête pas" est évidemment consistante, mais plus bizarre T + "p s'arrête" aussi est consistante. Est-ce qu'on a une raison de penser que ce genre de cas existe ou n'existe pas dans PA ou ZFC, donc que PA prouve l'arrêt d'un programme qui en fait ne s'arrête pas ?
- Qu'est-ce que je rate en ne regardant pas les choses plus compliquées que l'arrêt de programmes ? (sachant que pour toute formule $f$ je peux toujours regarder l'arrêt du programme qui énumère les théorèmes de T pour essayer de prouver $f$ ou $\lnot f$)
- Est-ce que ce qu'il faut regarder c'est la hiérarchie (compliquée) d'oracles mentionnée ici ?
- Enfin je me pose des questions sur l'aspect "canonique" de PA comme théorie pour parler de l'arrêt des programmes ou de l'arithmétique (au départ le seul truc canonique dont on dispose c'est le programme $\text{Stop}_0(p)$ qui exécute p et renvoie 1 s'il s'arrête)
De mon téléphone
(avec le tiers-exclu
$T \ |\!= \ \lnot f$
ssi $T \ |\!= f \implies $ faux
ssi $T+f \ |\!= $ faux
ssi $T+f$ inconsistante)
Et les "entiers infinis" si ça signifie les entiers non-standards alors ça ne me dérange a priori pas plus que ça de les "rater"
Pour ZFC c'est plus discutable mais j'y crois.
D'une manière générale, quelque soit la théorie (même non récursive), elle ne peut pas garantir que tous ses entiers (si elle parle d'entiers) sont les "vrais entiers au sens de GG l'intervenant du forum qui voudrait que cette notion ait un sens").
On a plus qu'un raison, on a un théorème qui le dit presque, ou plus précisément, aucun modèle de PA (ou de ZF) ne peut être "sûr de l'intérieur" que tous les programmes qu'il prétend s'arrêter s'arrêtent "vraiment". On peut même aller bien plus loin, mais je n'entre pas dans les détails, qui ne sont pas spécialement informatiques de toute façon.
Mais ne l'as-tu pas déjà compris? Si ta théorie est récursive et suffisamment expressive (c'est une exigence bien moins forte que celle de parler des entiers), l'énoncé indécidable naturelle (exprimé en termes informatiques) est "le programme p s'arrête" où p:=[faire défiler toutes les preuves dans T et s'arrêter dès qu'on en trouve une qui conclut que p ne s'arrête pas]
Tu peux aussi considérer le programme suivant, puisque tu as titré "problème de l'arrêt" : f(p):= [faire défiler les preuves jusqu'à en trouver une qui décide en conclusion si p s'arrête ou pas]. Ca te donne des indécidables à partir du seul fait de savoir que le problème de l'arrêt n'est pas récursif.
Cela dit, et c'est un reproche que je fais aux traités qui ont présenté toutes ces choses, à savoir d'oublier de signaler ce qui suit: le mieux est quand-même de faire remarquer aux gens que Z:="je ne suis pas prouvable" est un énoncé absolument et parfaitement mathématique (puisque "prouvable (dans X)" l'est) et que ça a été une erreur méthodologique grave de chercher à usine-à-gazer la notion alors que c'était évident (enfin ce l'était dès lors qu'il était connu et prouvé que "prouvable" a un sens mathématique alors que vrai n'en a pas). Beaucoup de "connaisseurs" ont la lacune de croire qu'ils font acte de pédagogie quand ils présentent Z. C'est vraiment dommage.
C'est un peu comme les élèves qui pensent qu'ils ont fait une erreur parce qu'ils ont écrit "comme $v=v$ donc .." ou comme un jour, une personne qui m'a répondu que c'est faux que la chose admise la plus dure à prouver est $X\to X$ (on discutait des indécidables, et j'en signalais parmi les plus évidents)
Rien ne nous garantit pourtant que le calcul de $A(1000,1000)$ s'arrête. La seule chose qu'on sait, c'est qu'aucun modèle de Peano n'acceptera de dire qu'il ne s'arrête pas (et a forciori aucun de ZF, etc). Autrement dit, si tu ajoutes à l'arithmétique élémentaire que $A$ ne s'arrête pas, alors tu peux définir (assez facilement une relation $R$ qui a comme propriété que $R(0)$ et $[\forall x: (R(x)\to R(x+1))$ et $\neg (\forall xR(x))]$.
Mais ça n'a rien d'un scoop, puisque de toute façon le simple fait d'affirmer que ce calcul ne s'arrête pas consiste à concevoir $A(1000,1000)$ comme "un entier infini", donc à croire à l'existence extérieure d'une ensemble contenant $0$ et stable par successeur qui ne le contient pas, et, ce qui nous fait une belle jambe, on gagne en plus avec les remarques qui précèdent qu'un tel ensemble n'appartiendra jamais à aucun modèle de ZF (ni de théorie assez nettement plus faible d'ailleurs, mais "faible" est tout à fait relatif ici)
La plupart des matheux (97% environ?) travaillent aux niveaux $\alpha:=0$ parfois 1 ou 2. Quand (rarement), ils essaient pour la première fois de monter (par exemple, pendant des rêveries de vacances où ils ne sont plus au labo), ils font quasi-systématiquement la même grave faute (qu'ont fait nos ancètres, etc) et "croire" ou "préjuger sans croire" que l'indiscernabilité pourra être traité comme une égalité (c'est très exactement l'opposé qui est vrai et prouvable) et c'est ce "traumatisme" qui engendre les âneries qu'on lit parfois sur "à isomorphisme près", etc.
Je ne sais pas s'il y a des gens qui ne font pas cette erreur, je ne me rappelle même plus si je l'ai faite ou non (enfin moi, je ne suis pas passé des maths à la logique, mais de la logique aux maths, donc je n'ai pas été confronté au problème) quand ils ont expérimenté ces méditations. Le fait que l'on trouve même (et plus actuellement qu'il y a 20 ou 30ans) des militants de "on ne veut plus que ce soit considéré comme une faute". Ce phénomène d'introduire de la politique dans les sciences est assez nouveau me semble-t-il
Et si un modèle de PA pense "il existe n tel que p s'arrête en n étapes" c'est qu'il existe un élément n de ce modèle tel que dans ce modèle p s'arrête en n étapes.
Donc si "p termine" est un théorème de PA alors il existe un vrai entier n tel que p termine en n étapes. Qu'on ne soit pas forcément capable d'expliciter un tel n est une autre question.
Mais c'est trivial que si PA est consistante et prouve que $p$ s'arrête en $n$ étapes alors c'est vrai..
Le problème c'est si PA prouve qu'il existe un $n$ (sans le donner) tel que $p$ s'arrête en $n$ étapes.
Non ça n'a rien d'évident que si PA prouve qu'il existe un $n$ tel que $p$ s'arrête en $n$ étapes, alors ce $n$ existe vraiment.
Et si on ne peut pas donner un tel $n$, alors c'est qu'il n'existe pas.
On a une croyance : que pour un programme $p$ fixé, la question "$p$ s'arrête ou pas" a toujours une vraie réponse, soit oui, soit non.
La question c'est si parfois PA répond des conneries (mais qu'évidemment on a aucun moyen de le prouver).
Si la réponse est oui, alors d'une certaine manière ça montre que notre croyance n'a pas vraiment de sens. Si la réponse est non, ça montre que notre croyance a un sens, dans un certain sens.
1) À partir du moment où une structure vérifie certains énoncés, elle vérifie aussi toutes leurs conséquences logiques.
2) Les "vrais entiers" vérifient les axiomes de Péano et de la logique classique.
3) Si un modèle de PA pense "il existe n tel que p s'arrête en n étapes" c'est qu'il existe un élément n de ce modèle tel que dans ce modèle p s'arrête en n étapes.
Votre malentendu provient de ce que, comme beaucoup de gens, vous oubliez car c'est tacite que vous travaillez dans ZF (et non pas ex nihilo). Le mot "vrai entier" n'a pas de sens en dehors de ZF. Le fait par exemple que $3$ soit un vrai entier n'est rien de plus que ZF prouve que $3$ est un entier. De même la terminaison d'un programme n'a pas de sens en dehors de ZF, il est donc normal que tu te demandes ce que peut bien vouloir dire "s'arrête". De même que "que peut bien vouloir dire $q:=10^{(2^{5000})}?$ est un entier fini". La réponse est simple, elle veut juste dire qu'il n'existe pas d'injection de $q$ dans $q$ qui ne soit pas surjective, mais ça on n'en sait rien, la seule chose qu'on sait c'est qu'une telle injection n'appartient à aucun modèle de ZF (ni même de ZF-AxiomeInfini**).
** si tu veux éviter les malentendus, d'ailleurs sache que Peano et ZF-AxiomeInfini sont essentiellement la même chose, sauf que la deuxième est plus pertinente (Peano, c'est juste parce qu'il y a les opérations des enfants dedans qu'elle est célèbre, mais elle est malsaine car artificielle, entre autre, les définitions complètement artificielle de $+$et $\times$ par récurrence). Le mieux est d'ailleurs de prendre NBG-AxiomeInfini, même si ce n'est pas l'usage,car comme ça, au lieu d'une théorie on a un seul axiome.
- on a donc que PA + "$p$ s'arrête" est consistante et prouve que $p$ s'arrête, alors qu'en fait $p$ ne s'arrête pas
- on se pose donc la question si PA peut ou ne peut pas faire le même genre d'embrouille.
Tu me réponds "PA a les vrais entiers pour modèle". En quoi c'est censé me convaincre ? Et de combien d'oracles et de théories annexes t'as besoin pour préciser ton argument ?
(a priori le but c'est de ne pas supposer la consistante de ZF pour répondre, sauf bien sûr si c'est le seul argument qu'on a)
Exercice: prouver qu'on peut se contenter des ensembles définissables sans paramètres.
@reuns: je te le redis il n'existe aucun argument valable ça a été prouvé qu'il n'y en a pas. Ceux qui y croient se livrent à un genre d'acte de foi (qui a le mérite de risquer une falsification). De plus les progrès de la physique rendent douteux que même A(1000,1000) ne soit pas infini comme déjà expliqué ci dessus. Alors tu penses bien que cons(Peano)...
Pour A:=(A=>0=1), pardonne-moi mais je ne vois pas le rapport avec Péano.
Et non, je sais bien que pouvoir prouver $P(n)$ pour chaque n n'entraîne pas $\forall n P(n)$ (au passage ça te couteraît quoi de rajouter une barre oblique avant forall, et des dollars autour?). Mais si je pars d'une structure que je sais vérifier la propriété $P(x)$ pour chacun de ses éléments $x$ (ici la "structure" c'est les entiers que je peux écrire avec papier et crayon), alors je peux affirmer que cette structure vérifie $\forall x P(x)$. Or si on me donne une propriété qui vérifie l'initialisation et l'hérédité, je sais qu'elle sera vérifiée par tout entier que je peux écrire. (autrement dit: $\vdash P(n)$ pour tout $n$ n'équivaut pas à $\vdash \forall n P(n)$, mais $\mathfrak M \models P(n)$ pour tout $n$ équivaut par définition à $\mathfrak M \models \forall n P(n)$).
Je parle de tout ça parce que j'ai l'impression que le désir de reuns c'est de comprendre en quoi le fait que PA prouve "p termine" garantit que dans la vraie vie p va terminer. Si on ne suppose pas que la vraie vie est un modèle de PA (ou du moins, une bonne approximation: tant qu'on ne laisse pas tourner un programme plus lomgtemps que l'âge de l'univers on peut faire comme si tous les entiers existaient), il n'y a effectivement aucune raison de supposer ça.
Par contre pour tout $x$ $(prouvable(x) \to x) \to prouvable(x)$ est un théorème. :-D
Soit $W:= (\forall X: (prouvable(X)\to X))$ et $P=prouvable (W\to (P\to \perp)$.
Supposons $P$. Alors $prouvable (W\to (P\to \perp))$, donc si $W$ alors $W\to (P\to \perp)$ alors $P\to \perp$, alors $\perp$.
Il suit que $prouvable(W\to (P\to \perp))$ (je viens d'en donner une preuve), c'est à dire $P$ et on répète ce qui précède, pour arriver à $\perp$. Moralité: $W\to \perp$.
Ce schéma te permet d'éviter des fautes du genre "je suppose implicitement $prouvable(a)\to a$ sans le dire"
*** Tu as dû vouloir dire : $D(D(X)\to X)\to D(X)$, mais c'est tout à fait différent!!! (en oubliant les "D", tu dis entre autre que quand un truc n'est pas prouvable, il est vrai :-D , ce qui n'était pas ton intention j'imagine). J'ai abrégé prouvable par "D".