problèmes arithmétiques indécidables

Dans un système du premier ordre qui contient l'arithmétique de Peano avec les opérations $+$ et $\times$
P(n) : il existe une démonstration de $0=1$ en moins de $n$ symboles.

Le problème c'est que les symboles des variables sont en nombre infini.
-> Les variables liées sont gentilles $\forall x, x\geqslant 0$ et $\forall y, y\geqslant 0$ sont les mêmes formules pour une certaine relation d'équivalence qui se comprend bien mais très sciante techniquement, de ce que je me souviens de mon humble apprentissage en auto-didacte de la théorie de la démonstration.
Il y aurait donc un nombre fini de variables liées vu sous cet angle.
-> Peut-il y avoir des variables libres dans une preuve de $0=1$? Je sais pas trop. Je dirais non, car lorsque l'on dit soit $x$ blabla, il ressort quantifié universellement, dans le résultat final = le théorème.
Si on les met de côté il y a l'algorithme "nyakatoutécrire modulo la relation d'équivalence (il y a soit $0$, soit $1$ soit $\ldots$, soit $n-1$ variables liées) et puis nyakatouteslestesterdanschacundescas"

On aura compris que c'est juste une réflexion à voix haute sur une question d'un thème que je trouve intéressant en logique : l'indécidabilité, de quelqu'un qui n'est pas expert en la matière mais qui a droit à la parole.

S

$\exists \text{preuve}(P)$
syntax error
en mettant des parenthèses ailleurs je me fais jeter aussi.

S

Moi ce qui me fascine c'est le manque de méta : méta-logique méta-maths et méta-programmation en maths, alors qu'il y a des questions fascinantes [small](notamment, à mon avis, du côté des programmes informatiques qui résolvent tout seuls des théorèmes)[/small]

Donc ma question était vraiment basée sur une interrogation : peux-tu ajouter à ta théorie logique que $\left(\ \exists Dem(P) \ \right) \implies P$ et si oui, qu'est-ce que ça change ? [small](sachant que lorsqu'on raisonne avec notre intuition, on l'utilise fréquemment)[/small]

@reuns : je ne sais pas si tu connais tout ça et si du coup je parle dans le vide ou pas, mais peut-être une façon plus intuitive de voir le 2nd théorème d'incomplétude est celle de Krivine dans son "Théorie des ensembles", où il le prouve en fait sur ZF plutôt que sur Peano (certes, c'est moins fort). Réecrit dans ZF, Dem(P) peut se voir comme "pour tout modèle M de ZF,M vérifie P", mais Dem(P) peut ne pas impliquer P, si par exemple le modèle "général" dont on veut savoir s'il satisfait P ne satisfait pas "il existe un modèle de ZF" : "aux yeux" d'un tel modèle, Dem(P) est vraie, et pourtant P pas forcément.
Plus concrètement si on se prend P qui n'est pas prouvable (elle peut être réfutable, mais on s'en fiche), alors on considère un modèle de ZF dans lequel P est fausse et dans lequel "il existe un modèle de ZF" est fausse aussi. Alors dans ce modèle, dem(P) est vraie, et pourtant P ne l'est pas, par construction.

Je n'ai pas lui le fil, je réponds à toute vitesse au tout premier post, pardon de ne découvrir le fil que maintenant. @LMPC: quasiment toutes les équations diophantiennes sont indécidables (parmi celles n'ayant pas de solution) et donc répondent à ta question.

reuns: c'est le théorème de Löb qui garantit que si pour un énoncé de PA: $Dem(\#P) \implies P$ est prouvable alors $P$ est prouvable ($\#P$ désigne le numéro de Gödel de $P$).