Bonsoir LeHibou.
Je me demande comment une propriété mathématique peut être vraie sans être démontrable.
On a un système d'axiomes.
Si on considère la première catégorie elle affirme qu'une proposition P est indémontrable. Ce qui veut dire que la proposition nonP n'est pas contradictoire avec les axiomes. On peut donc rajouter soit P soit nonP au système d'axiomes sans avoir de contradiction.
Après on peut considérer que P est vraie pour des raisons qui ne relèvent plus des mathématiques mais de la croyance.

Ceci étant dit je ne connais pas grand chose sur le sujet.

salut

je donne mon interprétation :

au final ce qui compte c'est la cohérence de la théorie (constituée d'axiomes et de théorèmes) à laquelle on ajoute une nouvelle proposition

lorsqu'on considère qu'une propriété est vraie mais indémontrable c'est qu'on ne dispose pas des outils dans la théorie pour montrer qu'elle est vraie (ou qu'elle est fausse) donc il nous manque quelque chose ...

et tout ce qu'on fait c'est qu'on a constaté (peut-être sur des exemples) qu'elle est (à priori) vraie parce qu'on n'a jamais trouvé d'exemples où elle est fausse.
on peut alors l'ajouter à la théorie puisqu'elle ne semble pas la contredire !

pour le deuxième cas je dirai que c'est presque la même chose sauf qu'on n'arrive simplement pas à se décider sur sa valeur de vérité et que l'ajouter elle ou sa négation ne permet toujours pas de déceler une quelconque incohérence dans la théorie ...

bon je sais pas si ça va t'aider à te décider dans ton indécision !!

Merci beaucoup verdurin et carpediem

En continuant mes recherches sur le sujet, je suis tombé sur un très long thread sur un site ami sur ce même sujet :

Pas plus de réponse définitive, ça date de 2005, mais je ne suis pas certain qu'on ait progressé depuis.

Et pour le plaisir, je vous partage ce résultat qu j'avais lu il y a des années dans le livre de Grégory Chaïtin "Hasard et complexité en mathématiques" :

Dans les hypothèses du 1er théorème de Gödel, le cardinal de l'ensemble des propositions logiques est Aleph¹,
et le cardinal de l"ensemble des  propositions logiques décidables est "seulement" Aleph⁰.

Autrement dit, "presque" toutes les propositions logiques sont indécidables !

Il y a des nuits où ça m'empêcherait "presque" de dormir

DSL je n'ai pas trouvé comment faire un vrai beau Aleph majuscule...

, ça ne fonctionne pas ?

Ulmière, comment as-tu fait pour générer ce magnifique Aleph  ?
Je ne le trouve ni dans les caractères spéciaux accessibles par le , ni dans l'assistant _LTX...

Il existe bien plus de commandes latex que ce que l'éditeur propose, et bien plus encore que ce qui fonctionne sur le site.

La commande est simplement \aleph et elle affiche la première lettre de alphabet hébreu.



Mais ce ne fonctionne pas avec l'alphabet arabe

Aleph, Beth, Guimel... Ça me rappelle quelque chose

Salut LeHibou,

Je me suis posé la question récemment et voici la conclusion à laquelle je suis parvenu (en refouillant dans mes souvenirs de théorie des modèles et par ci par là sur google).

Déjà, c'est vrai qu'on voit difficilemment à priori quel sens pourrait avoir le "vrai mais indémontrable".

Il me semble que "vrai" signifie que l'énoncé est vérifié (au sens intuitif) par une structure (un ensemble muni de certaines fonctions en gros).

Quand on dit qu'une proposition est indécidable dans une théorie, cela signifie que la dite théorie (décrite par ses axiomes) n'implique pas (avec les règles de déduction classiques) la proposition.
Autrement dit, il n'est pas vrai que tout modèle de la théorie vérifie la proposition.
Et c'est justement une stratégie de démo en théorie des modèles: être capable d'exhiber un modèle qui vérifie la proposition et un autre qui ne la vérifie pas; pour pouvoir conclure qu'un énoncé est indécidable.
Cela est dû au Théorème de complétude de Gödel (une des versions): Un énoncé est une loi (vrai dans tout modèle) d'une Théorie T si et seulement si cet énoncé est formellement déductible des axiomes constituant T.

Par exemple, en théorie des groupes, le fait que l'inverse de l'inverse d'un élément soit l'élément est une loi.
Par contre, la commutativité est indécidable. Cela signifie qu'avec juste les axiomes de groupes, on ne peut conclure que est vrai en général. Pourquoi? Car on peut trouver un modèle (un groupe donc) vérifiant cela (Z/3Z) et un autre ne le vérifiant pas (S3).
Tu peux donc former deux théories non contradictoires (une théorie est non-contradictoire si et seulement si elle admet un modèle ; ce qui est le cas ici pour les 2 théories): groupes commutatifs et groupes non commutatifs.

Et c'est bien de ça dont il s'agit avec le 1er théorème d'incomplétude de Gödel. Pour peu que la théorie satisfasse certaines conditions (dont la cohérence), il sera toujours possible de former des énoncés (exprimable avec les termes de la théorie) indécidables.

Maintenant, pourquoi certains disent-ils que Gödel dit que des énoncés sont "vrais" mais indécidables?
Parce qu'il se trouve que l'une des conditions pour que le théorème d'incomplétude s'applique est que la Théorie contienne l'arithmétique de Peano (en vrai c'est un peu plus faible que Peano mais passons).
Or, la preuve de Gödel, me semble-t-il (je ne l'ai pas examinée en détail), consiste à construire une proposition exprimable dans Peano et la tester dans un modèle particulier de l'arithmétique: le modèle standard de l'arithmétique de Peano. C'est en gros les entiers naturels au sens intuitif, donc avec nos pommes toussa toussa.
Et cette proposition est vraie dans le modèle standard. Vu qu'on est sur un modèle spécifique, la vérité d'un énoncé est "facilement" vérifiable.
Mais il construit ensuite un autre modèle (non standard donc; on peut montrer qu'il en existe d'autres que le standard ...) où l'énoncé qu'il a fabriqué est faux. Cet énoncé est donc indécidable avec les axiomes de l'arithmétique de Peano, car il existe un modèle où il est vrai et un autre où il est faux.

Donc quand on dit "il existe des énoncés vrais mais indémontrables", c'est sous-entendu par rapport au modèle standard des entiers; celui avec lequel on pense intuitivement. Et c'est, je pense, la raison pour laquelle on ne mentionne pas (ou rarement) que c'est relativement à ce modèle qu'on parle de "vérité".

Donc en résumé, ces énoncés ne sont pas "vrais" ou "faux" au sens général (ie pour tout modèle de la théorie): c'est bien l'objet du 1er théorème d'incomplétude. Et en conséquence directe, on peut former 2 théories cohérentes avec respectivement l'énoncé et sa négation. Mais en arithmétique classique (ie dans le modèle standard), certains de ces énoncés sont bien "vrais". Mais cette "vérité" n'est pas une loi; ie est fausse dans d'autres modèles.