Voici le wiki anglais à propos de ce théorème.
Il dit que le théorème original est technique mais qu'il peut se formuler ainsi :
The formal theorem is written in highly technical language. It may be paraphrased in English as:[citation needed]
Any effectively generated formal system capable of expressing elementary arithmetic cannot be both consistent and complete. In particular, for any consistent, effectively generated formal theory that proves certain basic arithmetic truths, there is an arithmetical statement that is true,[2] but not provable in the system
Comme le soutenait Alain Connes, c'est Vrai qui est utilisé, pas indécidable.
Ceci étant, je trouve qu'il n'y a pas d'incompatibilité entre les deux.
Le fait de dire indécidable signifie juste pour moi que certaines des assertions en question qui échappent à la démonstration sont vraies, d'autres fausses et que toutes sont indémontrables
Par voie de conséquence, dire qu'il existe des assertions vraies indémontrables est un sous groupe d'assertions indécidables.
Bon,...., je passe mais ce débat me semble bien avoir tout sons sens et je reste en phase avec la vision d'Alain Connes.
-----