Énoncés équivalents
Je me suis posé une question presque autant philosophique que mathématique, et j'aimerais avoir vos avis.
On va parler de l'axiome du choix, mais ma question de fond n'a aucun rapport avec lui, il va juste me servir d'illustration.
Si l'on veut démontrer, dans ZF, que tout espace vectoriel admet une base, normalement on utilise le lemme de Zorn, qui est équivalent à l'axiome du choix. On utilise le lemme de Zorn ici, et pas la formulation standard de l'axiome du choix, parce que vu ce qu'on veut démontrer, le lemme de Zorn est clairement plus pratique. Mais doit-on s'attendre à ce qu'il existe une démonstration du même résultat qui utilise effectivement la formulation standard de AC ? Idem pour tous les autres énoncés équivalents.
Je lis en ce moment une preuve du théorème de métrisabilité de Nagata-Smirnov. À un moment, on utilise le principe de Zermelo, lui aussi équivalent à AC. Et j'ai trouvé un paquet d'énoncés équivalents à AC. Si la réponse à ma question ci-dessus s'avérait positive, ça donnerait lieu à quelque chose d'assez intéressant, je trouve : en effet, le théorème de métrisabilité est un théorème de topologie générale, et le théorème de Krull est apparemment un énoncé équivalent à AC mais qui s'exprime en termes d'anneaux et d'idéaux. Si le théorème de métrisabilité devait être prouvable à partir du théorème de Krull, ça voudrait dire qu'il y a un lien "non trivial" (et peut-être pas encore découvert ?) entre la topologie générale et l'algèbre commutative, et ça signifierait qu'il y a encore des choses à apprendre et à découvrir en prenant un autre point de vue.
Si on oublie mon exemple avec l'axiome du choix et ses énoncés équivalents.
S'il existe une preuve de $A \Longrightarrow B$ et une preuve de $A \Longleftrightarrow A'$, doit-il forcément exister une preuve de $A' \Longrightarrow B$ ? Dans le sens, une preuve de $A' \Longrightarrow B$ qui n'utilise pas $A \Longleftrightarrow A'$, parce que sinon on peut forcément écrire $A' \Longrightarrow A \Longrightarrow B$, ce qui n'a pas beaucoup d'intérêt pour moi dans le contexte (trouver une démonstration entièrement nouvelle).
Je ne sais pas si je suis très clair, mais j'ai confiance :-D
On va parler de l'axiome du choix, mais ma question de fond n'a aucun rapport avec lui, il va juste me servir d'illustration.
Si l'on veut démontrer, dans ZF, que tout espace vectoriel admet une base, normalement on utilise le lemme de Zorn, qui est équivalent à l'axiome du choix. On utilise le lemme de Zorn ici, et pas la formulation standard de l'axiome du choix, parce que vu ce qu'on veut démontrer, le lemme de Zorn est clairement plus pratique. Mais doit-on s'attendre à ce qu'il existe une démonstration du même résultat qui utilise effectivement la formulation standard de AC ? Idem pour tous les autres énoncés équivalents.
Je lis en ce moment une preuve du théorème de métrisabilité de Nagata-Smirnov. À un moment, on utilise le principe de Zermelo, lui aussi équivalent à AC. Et j'ai trouvé un paquet d'énoncés équivalents à AC. Si la réponse à ma question ci-dessus s'avérait positive, ça donnerait lieu à quelque chose d'assez intéressant, je trouve : en effet, le théorème de métrisabilité est un théorème de topologie générale, et le théorème de Krull est apparemment un énoncé équivalent à AC mais qui s'exprime en termes d'anneaux et d'idéaux. Si le théorème de métrisabilité devait être prouvable à partir du théorème de Krull, ça voudrait dire qu'il y a un lien "non trivial" (et peut-être pas encore découvert ?) entre la topologie générale et l'algèbre commutative, et ça signifierait qu'il y a encore des choses à apprendre et à découvrir en prenant un autre point de vue.
Si on oublie mon exemple avec l'axiome du choix et ses énoncés équivalents.
S'il existe une preuve de $A \Longrightarrow B$ et une preuve de $A \Longleftrightarrow A'$, doit-il forcément exister une preuve de $A' \Longrightarrow B$ ? Dans le sens, une preuve de $A' \Longrightarrow B$ qui n'utilise pas $A \Longleftrightarrow A'$, parce que sinon on peut forcément écrire $A' \Longrightarrow A \Longrightarrow B$, ce qui n'a pas beaucoup d'intérêt pour moi dans le contexte (trouver une démonstration entièrement nouvelle).
Je ne sais pas si je suis très clair, mais j'ai confiance :-D
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Ou bien je prouve $A' \implies A' \land A$ puis j'utilise que $A' \land A \implies A$ et je conclus; ça te va ça ?
"Utiliser quelque chose dans une preuve" ou encore "deux preuves sont essentiellement pareilles" ce sont des notions qu'on n'arrive pas (encore) à formaliser proprement, si ce n'est strictement ("la formule machin n'apparait littéralement pas dans cette preuve") mais ça ça n'intéresse personne (en tout cas pas dans ce contexte)
Après, si tu parviens à préciser tes attentes en termes de longueurs de preuves, des investigations techniques pourraient te donner satisfaction, mais ce n'est pas tout à fait ce qu'on peut appeler "aisé".
Je te rappelle aussi comment marche la science et pourquoi il ne faut pas "trop" se fier à la présentation taxonomique qui est faite de tel ou tel système d'axiomes.
A l'origine l'humain raisonne dans une théorie qui est contradictoire en procédant à l’identification suivante:
$$ [u\in \{x\mid R(x)\} ] = [R(u)] $$
qui précède toute forme de fondement autre, y compris logique.
La crise des fondements a été causé par le fait que toutes les phrases sont équivalentes dès lors qu'on y ajoute les axiomes de la logique intuitionniste (donc a forciori ceux de la logique classique)
L'axiome du choix, naturel, et pouvant s'exprimer sans accepter d'office tout le reste PEUT AUSSI devenir redondant, si on accepte le reste, même sa partie ZFC bridée.
Le lemme de Zorn généralement présenté comme un équivalent de l'axiome du choix, ne l'est QUE parce qu'on admet ausi quelques autres axiomes. Mais il puise sa source beaucoup plus dans la découverte des ordinaux et surtout des axiomes d'existence de cardinaux suffisamment grands (même si impliqués déjà par ZF) que dans la notion de choix.
Pour être précis à ce propos:
soit $f$ qui a toute famille libre $e$ associe un vecteur $f(e)$ non dans $Vect(e)$. Alors, DANS ZF, et ce sans axiome du choix tu prouves qu'il y a une base. MAIS pour ça faut "pouvoir aller assez loin", ie on part de la famille vide, libre et on itère ordinalement jusqu'à "ne plus pouvoir". L'existence d'un moment où on ne peut plus résulte de l'axiome de l'ensemble des parties et n'a rien à voir avec l'axiome du choix dans son principe.
Ce que je veux, c'est une preuve entièrement nouvelle. Une preuve de $A' \Longrightarrow B$ qui n'utilise jamais $A$. Enfin, je veux savoir si c'est systématiquement possible, où si c'est "normal" que même si $A \Longrightarrow A'$ et $A \Longrightarrow B$, il puisse ne pas exister une preuve de $A' \Longrightarrow B$ qui "ne passe pas par A".
Dans le sens, démontre-moi que tout espace vectoriel admet une base sans jamais utiliser le lemme de Zorn. N'importe quel énoncé équivalent, une preuve aussi longue et complexe que tu veux, mais lemme de Zorn 100% proscrit, débrouille-toi sans.
Christophe : quand tu dis "on itère ordinalement"... est-ce que dans ZF sans choix, tu peux me démontrer un théorème qui affirme qu'une démonstration par récurrence sur les ordinaux c'est licite ?
Moi je répondaid à la question que (je pense/j'ai l'impression) tu te poses vraiment, à savoir "y a-t-il une preuve de A' implique B" qui n'utilise ”fondamentalement” pas ”A' implique A" ?"
Si ce n'est pas ta question, alors ce que dit Christophe suffit (élimination des coupures pour aller plus loin), mais si c'est bien ta question (en tout cas ça a souvent été la mienne) alors c'est plus compliqué; au sens où ce que christophe propose ça ressemble à
"tu as un preuve $(P_0,...,P_n)$ de $A\implies B$, une $(Q_0,...,Q_m)$ de $A'\implies A$ et au lieu de dire ' ah c'est bon je les mets à la suite l'une de l'autre', tu dis 'bah $(Q_0,..., Q_m, R, P_0',..., P_n')$ en est une de $A'\implies B$' " où $R$ est un truc technique (ou pas, ça va dépendre des présentations) et $P_i'$ est quasiment $P_i$.
Donc formellement ça donne bien une preuve qui n'utilise jamais stricto sensu $A'\implies A$, mais "moralement" elle l'utilise quand même. Ce que je disais c'est que ce "moralement" est difficile (impossible ?) à formaliser; alors que c'est lui qui a tendance à intéresser les gens, pas le strict (le strict intéresse rarement les gens)
Si on a $A \Longrightarrow B$ et $A \Longleftrightarrow A'$, on sait (de par les règles de logique élémentaire) que $A' \Longrightarrow B$. Mais peut-on écrire une preuve de $A' \Longrightarrow B$ qui ne se sert JAMAIS de $A$.
Si tu m'écris $A' \Longrightarrow A \Longrightarrow B$, la preuve ne contiendra aucune idée nouvelle. Idem si tu me mets des étapes intermédiaires là-dedans. Parce qu'en faisant ça, tu finiras toujours par utiliser $A \Longrightarrow B$ pour prouver $A' \Longrightarrow B$, et ce n'est pas ce que je veux : fondamentalement, la preuve ne contiendrait pas d'idée nouvelle.
Peut-on montrer que tout EV admet une base en invoquant soit une fonction de choix, soit un bon ordre, mais sans JAMAIS invoquer/utiliser une famille libre maximale ?
Dans notre exemple :
La version "Zorn" de "tout ev admet une base" consiste à prendre la famille des familles libres et d'utiliser Zorn pour dire qu'il doit exister un élément maximal, qui est donc une base.
La version "AC standard" du même résultat, je ne sais pas à quoi elle ressemblerait. Il faudrait une fonction de choix sur un certain ensemble, telle que l'image de cet ensemble par cette fonction de choix soit une base. L'argument est suffisamment différent et j'espère qu'on n'aurait pas besoin d'utiliser Zorn pour conclure ici.
Et la version "Krull" serait de trouver une structure d'anneau sur je ne sais quoi, sortir un idéal astucieux, utiliser le théorème, et paf trouver une base je ne sais comment sans jamais utiliser les éléments propres aux autres preuves.
D'un point de vue logique, on sait que $A' \Longrightarrow B$ est vrai, la partie difficile étant d'en trouver une nouvelle preuve.
Le problème c'est, comme je l'ai dit, que décréter quand "deux preuves sont essentiellement différentes" ou "essentiellement pareilles" c'est très compliqué. C'est un truc qu'on fait à l'arrache entre nous pour discuter. D'ailleurs tu remarqueras que c'est beaucoup plus simple de dire que c'est essentiellement pareil (il suffit d'exhiber un "chemin" qui mène de l'une à l'autre) que de dire que c'est essentiellement différent (il faut réussir à expliquer ou à intuiter qu'il n'y a pas de moyen abracadabrantesque de passer de l'une à l'autre)
Un truc qui se "rapproche" de cette question (mais qui est encore très très très très très loin de ce genre de considérations) c'est la théorie homotopique des types. Dans cette théorie types (ce qui correspond intuitivement aux ensembles de la théorie des ensembles) et propositions c'est pareil; et prouver une proposition $P$ c'est exhiber un élément $p: P$. Dans ce cas $p$ est vu comme une preuve de $P$. Le truc intéressant c'est que pour $a: A, b : A$ on peut former le type $a=_A b$ de "l'égalité entre $a$ et $b$". Un élément de type $a=_A b$ peut être vu comme une preuve que $a= b$ . En particulier si tu as une proposition $P$ et deux preuves $p,q: P$, tu peux te demander "si $p=q$"; ce qui dans ce cadre se traduit par "est-ce que le type $p=_P q$ a un élément/ est habité ?"
Dans certains cas on peut prouver que non, et donc que les preuves $p$ et $q$ sont "vraiment différentes". Mais bon, actuellement ça va pas être sur des trucs de la complexité que tu imagines avec Zorn/AC
Mais du coup, la théorie des types répond au moins partiellement à la question que je me pose, et ça c'est intéressant. A force, je vais finir par ne faire plus que de la logique et plus du tout de maths...
Tu travailles toujours en admettant des trucs. Je te le redis AC et Zorn ne sont pas équivalents. Ils ne le deviennent que grace à des axiomes supplémentaires.
Que ce soit Hott ou autre chose, si tu limites les axiomes utilisés (Hott n'est qu'une théorie comme une autre), tu peux espérer avoir des réponses à ce que tu demandes dans le sens suivant:
"Ai-je AC=>Base" dans LA théorie truc? (1)
"Ai-je Zorn=>Base" dans LA théorie truc? (2)
Bien entendu, la situation qui t'intéresse est celle où on a "non" pour (1), et "oui" pour (2).
Mais j'attire ton attention sur le fait que la première motivation, peu consciente, est AVANT TOUT la longueur de la preuve comme je te l'ai déjà dit.
Ce qui te plait dans Zorn =>Base c'est que c'est court alors qu'une preuve de AC=>Base sera longue. Evidemment ça fait "pas très subtil" de s'intéresser aux longueurs, c'est peu à la mode, mais ça n'en est néanmoins bien les choses déclenchant les ressentis à l'origine de ta question.