./7889> Bon voilà, derrière tout ça il y a en profondeur une histoire de vérification algorithmique.

Soit (P) une proposition arithmétique universelle, de la forme "Pour tout entier n, P(n)", où, pour chaque n, P(n) est vérifiable en temps fini (ya un algorithme qui termine, toussa toussa).

Supposons que (P) soit indémontrable, alors le programme qui cherche un contre exemple à (P) en faisant une boucle infini ne s'arrêtera jamais, et cela constitue une preuve de la véracité de (P).

Donc pour une telle proposition (P),
(P) indécidable => (P)
(P) indécidable => "(P) indécidable" est indécidable.

De même toute proposition arithmétique existentielle (P), où P(n) est testable en temps fini, est fausse si elle est indécidable, et son indécidabilité est alors elle même indécidable.



Les hypothèses ne s'appliquent pas :
- à l'axiome du choix, l'hypothèse du continu, etc... : on ne peut pas faire un programme qui boucle sur les ensembles ; ce ne sont pas des propriétés arithmétiques.
- à un truc comme le théorème de goodstein, ou la suite de Syracuse : P(n) n'est pas vérifiable en temps fini

Par contre elle s'appliquent :
- à la conjecture de Goldbach
- et sans doute aussi à l'hypothèse de riemann