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

Est-ce que ça existe?

L'auteur de ce sujet a trouvé une solution à son problème.
Auteur du sujet

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.

+0 -0
Staff

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 ?

Ce n’est pas en répétant « Hom, Hom », qu’on démontre des théorèmes sérieux - Siegel Mon Twitter

+3 -0

Cette réponse a aidé l'auteur du sujet

Si tu te places dans des raisonnements constructivistes, (sans le principe du tiers exclus), démontrer l'impossibilité de la non-existence d'une démo de $T$ n'est plus équivalent à démontrer $T$ : c'est très facile de comprendre cette idée en faisant un peu de théorie des types.

(Je n'ai pas d'exemple sous la main).

Mais en soi si tu prends n'importe quelle preuve non constructiviste de l'existence d'un truc (ce qui revient à démontrer qu'il est impossible qu'il n'existe pas truc), en soi tu démontres "il est impossible de ne pas avoir de démo de «il existe truc»".

Sans le tiers exclus, ça donne "il est impossible de ne pas avoir de démo prouvant $T$" avec $T =$ «il existe truc».

Édité par Grob'

+1 -0
Auteur du sujet

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$.

+0 -0
Staff

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.

Édité par Holosmos

Ce n’est pas en répétant « Hom, Hom », qu’on démontre des théorèmes sérieux - Siegel Mon Twitter

+0 -0

Mais il faut dire qu'il n'est pas très courant d'avoir des propositions indécidables.

Holosmos

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)

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$.

Berdes

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)

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.

Holosmos

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.

Édité par Grob'

+0 -0
Staff

(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 ?

Ce n’est pas en répétant « Hom, Hom », qu’on démontre des théorèmes sérieux - Siegel Mon Twitter

+0 -0

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…

Édité par Grob'

+0 -0
Staff

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.

Ce n’est pas en répétant « Hom, Hom », qu’on démontre des théorèmes sérieux - Siegel Mon Twitter

+0 -0

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

+0 -0
Auteur du sujet

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})$.

Grob'

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.

+0 -0
Staff

À 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 …

Ce n’est pas en répétant « Hom, Hom », qu’on démontre des théorèmes sérieux - Siegel Mon Twitter

+0 -0
Auteur du sujet

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.

+0 -0

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…

Édité par Grob'

+0 -0
Staff

Cette réponse a aidé l'auteur du sujet

Salut,

Je suis tombé là-dessus tout à l'heure : https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_de_L%C3%B6b suite à la lecture de ceci : https://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8mes_d%27incompl%C3%A9tude_de_G%C3%B6del#Cons.C3.A9quences_imm.C3.A9diates_du_second_th.C3.A9or.C3.A8me_d.27incompl.C3.A9tude

Je ne suis pas certain d'avoir bien compris de quoi il retournait, mais il me semble que c'est lié - dans une certaine mesure - à ce que tu évoques.

J'ai l'impression, toutefois, qu'il s'agit là d'une tautologie, en tout cas c'est ce que laisse présager cette phrase :

Un autre exemple d'application simple, mais assez surprenante, du second théorème d'incomplétude est le théorème de Löb, qui affirme que, dans une théorie T qui satisfait les hypothèses utiles, prouver dans T un énoncé sous l'hypothèse que cet énoncé est prouvable dans la théorie, revient à prouver l'énoncé. Autrement dit cette hypothèse est inutile.

Wikipédia

Édité par Algue-Rythme

+1 -0
Auteur du sujet

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 à :

Il existe des théories non contradictoires démontrant leur propre incohérence

Wikipédia

+0 -0
Vous devez être connecté pour pouvoir poster un message.
Connexion

Pas encore inscrit ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte