Formules prouvables à partir de PA

Pourquoi le fait que toutes les fonctions récursives sont fortement représentables ne suffit-il pas? La fonction qui à $n$ associe le $n+1$-ème entier premier est récursive, il existe donc une formule $A$ telle que $\vdash (\forall x) (\exists ! y) A(x, y)$ et ($\vdash A(x, y)$ si, et seulement si, $y$ est le $(x+1)$-ème nombre premier). Que l'on ait $\vdash (A(x, y) \Rightarrow (P(y) \wedge y >x))$ (où $P(y)$ signifie "$y$ est premier") devrait être immédiat; d'où $\vdash (\forall x) (\exists y>x) P(y)$.
Qu'est-ce qui cloche?

Poirot à partiellement raison car on n'a pas de fonctions dans le langage de PA il faut utiliser le théorème chinois pour décrire ce que veut dire factorielle (ou produit d'une liste,etc) qui passera par un codage des suites finies.

Cela dit ce n'est pas non plus "bien méchant".

Une suite est un triplet (a, b, c) et l'image de n par elle est le reste de à divisé par (b+cn)

Je n'utilise pas de fonction dans PA. J'utilise un théorème qui dit qu'il existe une formule $A$ de PA telle que, pour tous entiers $x$ et $y$, on a $\vdash A(x, y)$ si, et seulement si, $y$ est le $(x+1)$-ème nombre premier et telle que $\vdash (\forall x) (\exists ! y) A(x, y)$.

@poirot: la récurrence avec juste les formules closes entraîne PA.

Mieux : tout PA théorème peut se prouver en utilisant une seule fois la récurrence sans paramètre (exercice pas si difficile , ne pas se laisser intimider)