Démonstration non constructive de l'existence d'une démonstration

Bonjour à tous,

Je viens de me poser une question assez étrange : est-ce qu'il est déjà arrivé que l'on démontre l'existence d'une démonstration d'un théorème de manière non constructive (c'est-à-dire sans expliciter cette démonstration).

Il est courant de démontrer l'existence d'un objet mathématique sans l'expliciter. Par exemple, le théorème des valeurs intermédiaire nous indique l'existence d'une valeur $c \in [a; b]$ telle que $f(c) = x$ sous les hypothèses que f soit continue et que $x \in [f(a); f(b)]$, mais il ne nous donne aucune information sur la valeur de $c$.

Du coup, je me demandais si des matheux avaient déjà fait la même chose, mais avec une démonstration. L'idée serait de prendre un théorème $T$ et de démontrer qu'il existe $D$ une démonstration qui prouve $T$, ou encore de démontrer l'impossibilité de l'absence d'une démonstration qui prouve $T$. Tout cela sans expliciter un $D$ possible.

Même si ça paraît un peu perché, ce serait super badass et donc forcément intéressant.

Edit : en fait, je viens de me rendre compte que ce n'est pas possible. La preuve de l'existence d'une démonstration d'un théorème est elle-même une démonstration du-dit théorème. Mais ça n'enlève pas ma question de savoir si il y a déjà eu une démonstration qui se base sur ce genre de réflexion. Par exemple : on suppose qu'il n'existe pas de démonstration au théorème $T$, bla bla bla on arrive à une contradiction, donc il existe un démonstration de $T$, donc $T$ est vrai.

Par exemple : on suppose qu'il n'existe pas de démonstration au théorème T, bla bla bla on arrive à une contradiction, donc il existe un démonstration de T, donc T est vrai.

Ce qui revient à faire une démonstration par l'absurde, non ?

Merci pour vos réponses. Je me suis un peu renseigné sur le sujet et en fait (sous réserve que j'ai bien compris), même s'il est rare en math de ne pas accepter les démonstrations non constructive, on ne peut pas vraiment le faire sur les démonstrations. Le fait qu'il n'existe aucune démonstration de $non T$ ne veut pas forcément dire que $T$ est vrai. Dans un cas comme ça, soit $T$ est démontrable, soit $T$ ne l'est pas. Du coup, c'est quand même contre-intuitif que l'absence de démonstration de $T$ et l'absence de démonstration de $non T$ ne soit pas exclusifs.

Si je comprends bien (et en se plaçant dans une théorie consistante), $T$ vrai implique qu'il n'existe pas de démonstration de $non T$, en revanche l'absence de démonstration de $non T$ n'implique pas la véracité de $T$.

C'est bien cela

Mais il faut dire qu'il n'est pas très courant d'avoir des propositions indécidables. Si jamais tu arrives à montrer qu'une démonstration de non T implique l'absurde, alors tu as déjà un bon argument quant à la véracité de T. Même si ça ne démontre pas T, la plupart des matheux te diront que ça suffit pour travailler avec (on peut, en effet supposer alors T).

edit : j'ai un peu peur de dire des bêtises. J'aimerai bien que quelqu'un confirme.

Je dirais que ça dépend beaucoup de la théorie dans laquelle tu travaille. En théorie des groupes, la proposition $\forall a,b, a+b=b+a$ est indécidable (si c'est vrai, le groupe est abélien, sinon, le groupe est non-abélien, mais il existe des groupes abéliens et des groupes non-abéliens, donc quand on travail avec "n'importe quel groupe", cette proposition est indécidable)

Ici, si on suit mon exemple $T=\forall a,b, a+b=b+a$, montrer qu'il n'existe pas de démonstration de $non T$ c'est construire un groupe abélien. Ça ne veut pas dire que tous les groupes sont abéliens. (Donc ce que tu dis est juste)

Et là je dirais que ça dépend de ce que tu entends par "démontrer qu'une démo de non T implique l'absurde", et du contexte.

(si c'est vrai, le groupe est abélien, sinon, le groupe est non-abélien, mais il existe des groupes abéliens et des groupes non-abéliens, donc quand on travail avec "n'importe quel groupe", cette proposition est indécidable)

Je t'avoue que je suis étonné. Est-ce qu'on peut exhiber un exemple de tel groupe ?

L'exemple des groupes n'a rien a voir avec l'indecidabilité. Si tu travailles avec n'importe quel groupe, c'est que tu n'as pas défini l'opération +, donc tu ne peux rien dire sur ses propriétés.

Bon, alors dans la théorie suivante :
Langage : +, -, 0 (et =, mais je me place dans une logique qui donne toujours un sens au =)
Axiomes :
$\forall x, x + 0 = x$
$\forall x, y, z, (x + y) + z = x + (y + z)$
$\forall x, x + (-x) = (-x) + x = 0$

…La proposition $T = \forall x, y, x + y = y + x$ est indécidable. Indécidable dans le sens où elle ne peut pas se déduire des axiomes.
Pour démontrer cette indécidabilité, on doit créer deux structures, l'une respectant les axiomes et $T$, l'autre respectant les axiomes et $non T$.
On pourra prendre par exemple $\mathbb Z$ et $\mathcal{M}_2 (\mathbb{R})$.

(Et non, si l'on prend n'importe quel groupe, à priori, soit il est abélien, soit il ne l'est pas).

…Par contre le théorème de Lagrange est vrai dans cette théorie…

D'accord, donc il ne s'agit pas vraiment d'un certain groupe qui n'est ni abélien ni non abélien …

Dans tous les cas, à part les personnes travaillant dans le domaine de la logique, je connais assez peu de maths où on tombe facilement sur une proposition indécidable.

En même temps, faut savoir dans quelle logique on travaille quand on fait des maths qui sont pas dans le domaine de la logique…

Dans ZF t'as l'axiome du choix. Pour ZFC, j'ai trouvé cet article Wiki, qui donne mine de rien des exemples dans pas mal de domaines différents des maths

Dit-moi si je me trompe, mais si tu n'as que 0 dans ton langage, la propriété $\forall x, y, x + y = y + x$ est toujours vrai d'après les axiomes 1 et 3 (à moins que $-0$ et $0$ soient différents).

Et d'ailleurs, je vois pas en quoi $(\mathcal{M}_2(\mathbb{R}), +)$ n'est pas un groupe abélien. L'addition de matrice se fait membre à membre, donc le fait qu'un ensemble de matrice muni de la loi $+$ soit abélien est équivalent au fait que l'ensemble sous-jacent soit abélien ou non.

À mon avis il ne s'agit pas du groupe $\mathcal{M}_2(\mathbf{R})$ mais ${\rm GL}(2,\mathbf{R})$ muni de la multiplication.

Sinon j'aimerais bien que tu détailles pourquoi $x+y=y+x$ est vrai d'après les axiomes 1 et 3 …

En fait, je me suis emporté pour l'axiome 3 . Avec uniquement 0 dans le langage, $x + y = 0 + 0 = 0$ et $y + x = 0 + 0 = 0$. En fait, ce que je veux montrer par là, c'est qu'il manque quelque chose dans ses axiomes : savoir dans quel ensemble on travaille.

Parce que finalement, si on énonce la propriété pour tous les groupes, elle est simplement fausse (il y a au moins un contre-exemple) et pas indécidable.

Effectivement, au début j'avais écris $GL_2(\mathbb{R})$ et par innatention j'ai "corrigé"… ><'

Non, il ne manque rien dans mon langage. Le langage, c'est les symboles de constante, de fonctions, de relations. On n'y donne pas tous les éléments, seulement ceux qui ont une importance axiomatique (sinon on pourrait pas avoir plusieurs modèles différents dans ta théorie).
Ce que veut dire ce 0 c'est que pour dire qu'une structure est un groupe, il faut donner un sens à l'élément neutre (et donc extirper un élément qui aurait ce sens).

Attention aussi à ne pas mal interpréter !
La propriété "tout groupe est abélien" est fausse, comme tu le souligne.
Maintenant, je prend un groupe. La propriété "il est abélien" est indécidable : selon le choix du groupe que tu as fait, elle peut être vraie ou fausse.

il manque quelque chose dans ses axiomes : savoir dans quel ensemble on travaille.

Non. Une théorie c'est un ensemble d'axiomes. Un modèle de cette théorie, c'est une structure (= un ensemble avec des relations et des lois de compositions) dans laquelle tu peux donner sens à tous les éléments du langage, et dans lesquels les axiomes de la théorie sont vrais. Une théorie n'est jamais équivalente à son modèle (d'ailleurs très peu de théories ont un seul modèle)…

Quand tu fais des raisonnements sur des espaces vectoriels, que tu démontres le théorème du rang, t'en a rien à foutre de quels ensembles tu as. La seule chose que tu veux c'est des ensembles soient des espaces vectoriel (donc qui vérifient les axiomes de ta théorie).

C'est même là la force des axiomes : tu pars de quelques propriétés, sans te demander sur quels ensembles ces propriétés agissent, et ensuite tu en démontre d'autres (qu'on appelle théorème).
Après, tu peux appliquer ces théorèmes que tu as démontrés dans des cas particuliers, où ton ensemble vérifie tes axiomes…

Le théorème de Löb répond plutôt bien au questionnement que j'avais.

Par contre, sur le deuxième théorème d'incomplétude, j'ai préféré (pour des raisons de santé mental) m'arrêter à :