Vérité dans le modèle standard de l'arithmétique

[Médiat]

Peut-on dire alors que le théorème (affirmant l'existence d'un polynôme sans racine) fournit un algorithme pour lister une classe d'éléments de l'ensemble des propositions vraies dans lN ? Ces éléments étant systématiquement de la forme "le polynôme P_A n'a pas de racines dans lN" où A est une théorie satisfaisant aux hypothèses du théorème.

Ce n’est pas tout à fait cela, on exhibe une famille de polynôme n’ayant pas de racine dans IN, et on se débrouille pour choisir, en fonction de A (l’hypothèse de récursivité est essentielle), une famille qui contient des polynômes dont on ne peut démontrer dans A qu’ils n’ont pas de racines.

Cet algorithme est-il une démonstration rigoureuse dans un système formel ?

Pourquoi pas ? C'est la théorie de la récursivité qui est utilisée.

Enfin, puis-je tirer de ton message #14 qu'on ne peut pas enlever les guillemets autour de "démonstration", donc qu'il ne s'agit pas d'une vraie démonstration ? Y a-t-il seulement un sens à travailler dans la théorie de lN, où démontrer se réduit à exhiber par des techniques très particulières des axiomes de la théorie de lN ?

J’avais écrit mon message 14 avant de lire le document, et bien sur qu’il s’agit d’une vraie démonstration, et comme des « axiomes de la théorie de IN » sont « vrais » dans IN, il me semble bien que cela a du sens d’en exhiber quand on le peut.

Je rappelle aussi que s’il existe un polynôme P pour lequel l’existence de racine est indécidable dans A, alors P n’a pas de racine dans IN.
-----