Que doivent faire les fondements ?
Bonjour,
Je vous partage juste ce texte très intéressant de Penelope Maddy, sur la question des fondements des mathématiques; et la "tension" dont on peut entendre parler entre théorie des ensembles, catégories, et plus récemment, HoTT.
Elle prend une perspective que j'aime beaucoup : plutôt que de prendre pour donné le mot "fondements", elle tente de le décortiquer - et pose la question que beaucoup prennent pour acquise : "quel rôle veut-on que nos fondements jouent ?".
Elle répond en déterminant un certain nombre de rôles que la théorie des ensembles remplit, et pour laquelle elle a été créée, et évalue dans quelle mesure les autres fondements proposés y répondent.
Elle remarque qu'en fait (mais là je vous spoile), dans les deux cas (catégories et HoTT), la volonté d'avoir de nouveaux fondements n'était pas là parce que la théorie des ensembles ne remplissait pas ces rôles, mais parce que de nouveaux rôles potentiels de fondements ont été trouvés.
Finalement, sa conclusion est (en gros) que le terme "fondements", et le débat sur "quels sont les bons fondements" sont mal posés - les questions qu'il vaut mieux se poser sont "quels sont les rôles que doivent jouer des bons fondements, et dans quelle mesure les fondements proposés les remplissent-ils ?"
Bonne lecture !
Je vous partage juste ce texte très intéressant de Penelope Maddy, sur la question des fondements des mathématiques; et la "tension" dont on peut entendre parler entre théorie des ensembles, catégories, et plus récemment, HoTT.
Elle prend une perspective que j'aime beaucoup : plutôt que de prendre pour donné le mot "fondements", elle tente de le décortiquer - et pose la question que beaucoup prennent pour acquise : "quel rôle veut-on que nos fondements jouent ?".
Elle répond en déterminant un certain nombre de rôles que la théorie des ensembles remplit, et pour laquelle elle a été créée, et évalue dans quelle mesure les autres fondements proposés y répondent.
Elle remarque qu'en fait (mais là je vous spoile), dans les deux cas (catégories et HoTT), la volonté d'avoir de nouveaux fondements n'était pas là parce que la théorie des ensembles ne remplissait pas ces rôles, mais parce que de nouveaux rôles potentiels de fondements ont été trouvés.
Finalement, sa conclusion est (en gros) que le terme "fondements", et le débat sur "quels sont les bons fondements" sont mal posés - les questions qu'il vaut mieux se poser sont "quels sont les rôles que doivent jouer des bons fondements, et dans quelle mesure les fondements proposés les remplissent-ils ?"
Bonne lecture !
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Bin, ça me donne l'occasion de ronchonner.
Le mot "fondement" est simple et peu problématique. Donc je suis contre sa démarche à cette dame.
Depuis des lustres, je propose que ce soit le mot "unification" beaucoup plus expert comme réceptacle de tels débats qui soit utilisé. En gros, cette dame écrit un livre que, si je l'avais écrit, on obtiendrait peut-être le même texte en tout point à ce ci près qu'avant la compilation, il aurait appliqué un "menu-edit-remplacre-fondement-by-unification"
Je rappelle que le fondement de la science théorique est invariable: prouver formellement tout ce qu'on dit, et laisser bien visibles les axiomes (ie les hypothèses faites, TOUT COMPRIS).
La suite n'est plus dans les fondements, mais dans les affaires pratiques de comment classer, répertorier, faire fructifier cette obligation. C'est d'autant plus important que nous travaillons tous dans des théories contradictoires, donc ce ne sont pas les conclusions (ce qui est prouvable) qui compte, mais les preuves elles-mêmes.
Et ça ne m'étonne pas que HoTT et le catégorisme soit déclaré comme n'ayant pas eu comme but initial d'être refondant par cette dame car effectivement on voit bien quand on papote et se dispute que c'est "revendicatif".
Or la recherche n'est pas revendicative.
Il est chaque fois d'ailleurs utile de rappeler que ZF(C) ne fonde rien du tout, puisque ZF** (enfin au choix des axiomes près, ie du bridage de la compréhension) EST le substrat dans lequel les gens s'expriment (all science et même all comprises), il n'y a donc pas de "sens" à prétendre le déloger (ce serait comme dire qu'on retire le vide d'une pièce pour y mettre quelques chose. Quand on met un truc, on remplit le vide, on ne le "déloge pas").
** j'entends par là le fait d'exécuter un $\forall x$ sur une collection et rien d'autre***.
*** ZF n'a rien fait d'autre que "forcer" les gens à assumer, ie s'ils remplacent les occurrences de $u_i\in x$ par $R(u_i)$, ils doivent le dire**** et pas le passer en catimini. Ce n'est pas un fondement, c'est une prise de conscience.
**** le choix conventionnel pour le dire est d'avoir "fait exister" $e:=\{y\mid R(y)\}$ et prétendre appliquer un truc vrai pour tout $x$ à $e$, mais ce n'est pas offensif ni profond.
En l'occurrence elle ne défend pas du tout l'idée que les catégories soient fondationnelles, et sa conclusion à ce sujet est que la théorie des ensembles remplit bien son rôle ;-)
Tu devrais lire tout de même, si tu veux en considérant que le mot anglais "foundations" ne se traduit pas par "fondements", ou en prétendant que c'est un mot différent, et ça restera intéressant, malgré ton point de vue sur la question des fondements
Pour les maths n'importe quel système de règles de réécriture capturant toute la récursivité fournit un fondement acceptable (à défaut d'être pratique, mais ce dernier point appartient à une problématique distincte).
Où est cette preuve que ZFC |- 0=1?
Moi je veux la lire.
(sachant qu'en principe les maths autres que la logique et la TDE, en pratique, n'ont pas grand chose à faire des fondements spécifiques, à quelques exceptions près)
@Foys, je parle de la "vraie" théorie*** dans laquelle on travaille. ZF est une sorte de version polie, rien d eplus (dont on ne sait pas si elle est ou n'est pas consistante d'ailleurs)
***
$$ \forall R\exists a\forall x: [(x\in a) \iff (R(x))] $$
comme avec les dollars, je ne pouvais pas faire de smiley $<<$ :-D $>>$, je réécris sans :
J'ai une erreur 404
Tu peux le lire ici (attention, on a l'impression qu'il faut s'enregistrer pour le télécharger mais tu peux juste descendre et il sera là)
Mais j'en reste à fonder c'est expliquer à un enfant de 8ans la règle du jeu. Et donc poser la théorie originelle et attendre maturité pour différencier.
Le document est extrait de ce livre.
Bien cordialement,
Thierry
La fin du milieu du texte montre que c'est une auteure sérieuse et qui a travaillé la documentation, mais hélas avec une compréhension très limitée me semble-t-il de la TDE. On a l'impression qu'elle reproduit un exposé vugarisé qu'elle a entendu en interviewant des set theorists. Ca ne préjuge de rien, mais laisse de côté toute la partie de l'anlyse qui pourrait être attendue.
J'imagine qu'ensuite elle montrera plus de compréhension des catégories et de HoTT, mais une fois de plus, on a "la problématique" étudiée par un partisan et connaisseur d'un bord.
Voici les deux citations:
Une erreur aussi grostesque est généralement l'indice que le reste du texte n'apportera pas de "substance mathématique" au débat, car il est difficile de faire plus faux et plus dérapage de débutant que ça.
A nouveau cette grave erreur de débutant!!! Ca survient au milieu du texte environ où la transition va se faire fin de l'analyse TDE, début de l'analyse Catégories+HoTT
Et puis là, elle s'enfonce. tout ceci est parfaitement trivial et Grothendieck n'a rien surmonté du tout à ce niveau. Heuresement pour lui que les travaux qu'il a laissés à la postérité contiennent autre chose.
Théoriquement un auteur qui maitrise le sujet ne devrait jamais écrire ces sottises. Cela ne veut pas dire qu'elle ne le connait pas, mais que ces indices jettent un certain discrédit sur sa compréhension des choses qu'elle discute.
On retrouve l'éternelle faute de la distinction "petite/moyenne/grande catégorie" qui à mon sens pénalise beaucoup les débutants qui se focalisent affectviement, même si c'est 20mn sur ce non sens, et perdent, même 20mn, c'est 20mn de perdue de trop.
Je ne veux pas être trop affirmatif, je n'ai pas tout lu. J'ai aussi constaté cette manie de dégrader son propre texte à cause d'une espèce de protocole qui veut qu'on mette des citations, manie qui, si on s'y force "juste pour suivre" les règles académiques ont tendance à obscurcir et dégrader la structure. C'est bien la politesse de citer des gens, mais c'est anti-scientifique dans de nombreux cas.
Quand j'aurais lu la partie sur les catégories (qu'hélas, pour le coup je ne connais pas mieux voire bcp moins bien que l'auteure) je posterai. Mais quel dommage qu'ait figuré ces 2 grosses fautes dans son texte, car à coup sûr, un TDiste qui lit s'arrête (à tort ou à raison) aussitôt les avoir lu en pensant avoir affaire à un de ces éternelles philosophes qui parlent sans savoir (je dis bien A TORT ou à raison).
Je pense que dire "c'est l'ensemble des théorèmes qu'on peut déduire de ZFC" serait une réponse évidente mais trop simpliste. On ne peut pas rendre trop simpliste dans l'autre sens non plus, et dire que c'est toutes les déductions de la logique classique. Est-ce que "j'ai un chromosome Y, donc je suis presque sûrement un homme" c'est des maths ? Il y a des maths en dehors de la logique classique, il y a des maths en dehors de ZFC... mais du coup les maths c'est quoi ? Un ensemble de déductions faites à partir d'axiomes formels dans un langage logique formel ? Je suis sûr que vous trouverez encore quelque chose à critiquer à cette définition, c'est là tout l'intérêt de la chose. Mais si on prend ça comme définition, les fondements dont on a besoin sont clairs : il faut un langage logique, des règles de déduction, des axiomes logiques, des axiomes "pour démarrer les maths" et ainsi ne plus faire de la logique pure. Auquel cas n'importe quel théorème exprimé dans un certain langage formel, en utilisant les règles d'un système de logique donné, serait des mathématiques. Est-ce que c'est ça qu'on veut ? Moi, je ne sais pas. Je sais que ce que je fais, je veux que ce soit "des maths", mais décrire toutes les maths ? Au secours.
Je n'arrive pas à ouvrir ton fichier enfrancaisFourniparMaxFoundations.tex (64 KB).
Pourrais-tu le convertir en PDF ? Merci.
1/ On veut des contradictions, ie des théorèmes, c'est à dire des garanties que tel et tel truc mène au paradis
2/ On veut le faire dans des théories qui ne sont pas contradictoires, autrement dit on veut "ne pas obtenir de contradictions"
Tant qu'on n'aura pas atteint l'époque où les scientifiques auront dépassé cette idiotie, on aura des débats stérils de ce genre.
3/ Je prends quelques exemples:
3.1/ l'auteure du texte déclare que ZF apporte beaucoup, que les recherches ont été approfondies et qu'on a fourni une mesure du risque à travers la consistency-strength des axiomes et théories.
3.2/ Très bien, mais si ZF est contradictoire, ça nous fait une belle jambe...
3.3/ Les obsédés du typage le considèrent comme "un gros truc" en termes de contraintes garantissant la consistance. A ça, deux commentaires:
3.3.1/ "Le gros truc" en question étant prouvé dans ZF (à la rigueur pour certains alinéas dans Peano :=ZF-) idem. C'est du vent. Par ailleurs, que se dépêche de faire quelqu'un qui type? Se placer en pensée "au dessus du truc" (autrement dit "détyper" :-D ) pour faire mieux que ses petits copains qui, s'lis ont le malheur de la jouer loyale et rester "dans le type" ne seront paa inspirés. On a à nouveau cette dualité "beurre et argent du beurre".
3.3.2/ La contrainte garantit bien évidemment un système beaucoup trop faible. Ca ne veut pas dire que c'est inintéressant, mais, c'est une spécialité très très spécifique (en gros, conscient que Brouwer et cie sont des équations diophantiennes expriment des trucs à pixels assez fins, MAIS EN NOMBRE FINI, le développement d'outils adaptés est une ambition tout à fait légitime, comme l'est le développement de programmes s'exécutant en temps polynomial et effectuant des trucs fins.
3.4/ Mais attention à ne pas faire comme en physique, un genre de "prise de pouvoir" sociologique qui stériliserait les choses et ralentirait énorménet la recherche, un peu comme En France la géométrie algébrique a occupé trop de place dans les Etats-majors recrutant.
4/ Un rappel me semble aussi profitable: en maths il y a réellement deux applications: l'optimisé pratique et le "par principe".
4.1/ PGCD(a,b), ce n'est pas PGCD(b,r :=reste ..), c'est PGCD(a-b,b).
4.2/ Si l'on veut OPTIMISER on remarquera qu'on peut DEVINER la suite de l'exécution et donc modifier le programme etça c'est une science difficile et appliquée qui ne mérite en aucun cas parfois le mépris qu'on lui inflige, MAIS C EST AUSSI SPECIFIQUE, c'est à dire qu'on ne peut pas faire que ça, et maintenir des définitions hybrides désorientantes au motif de s'embrasser à distance avec les appliquaurs.
4.3/ Pour ces même raisons, $p$ est premier quand for i:=2 to p-1 do if i | p then ExitWith "CRASH" else NeRienFaire done ne renvoie pas d'exception "crash" et non pas quand begin i:=2; while $i\times i\leq p$ do if i | p then ExitWith "CRASH" else i:=i+1 done n'en renvoie pas
5/ On peut multiplier à perte de vue les exemples où chaque boutique, avec ses préoccupations tente de préempter des choses et ça ne sert personne, car bien souvent complique à la fois la recherche mais aussi la transmission des acquis.
6/ De mon point de vue fonder n'est pas recherche la consistance d'une théorie, mais positionner un protocole EXTREMEMENT simple d'arbitrage des preuves qui puisse être très vite acquis par l'enfant.
7/ On oublie trop que c'est ce qu'a fait ZF (d'où toutes les maths exprimées dedans sans même que les gens s'en rendent compte), mais là encore, il faut être très clair, pas "ZF qui est vrai" (ça ne veut rien dire), mais "ZF qui est supposé" (c'est à dire en polarité négative) et en fait assez variable.
8/ A mon sens le reste est du blabla. De toute façon ce qui compte ce sont les preuves et non leurs conclusions et les chercheurs sérieux ont plutôt intérêt à connaitre les preuves des lemmes qu'ils manipulent je pense (sinon, on est devant de l'amateurisme Syracusien à la petite semaine, à s'amuser à tirer à la Kalachnikov pour voir la taille des trous dans le mur). Ce n'est pas parce qu'on va remplacer
$$a=b=c=d=\dots =w$$
par un chemin homotopique continu allant d'une entité bellement dessinée "a" vers l'entité idem "w" qu'on va faire avancer "les fondements", ce sont là des considérations relevant de la recherche aguerrie et des experts, tout comme les histoires de consitency-strength.
Et oui, si tu veux je le convertirai (mais ça me prendra un peu de temps car il est mal formaté)
Inutile donc de perdre du temps, j'ai récupéré ce texte mais j'ignore si je vais y comprendre quelque chose.
Bon courage.
1.1/ L'axiome du choix serait un anti-constructif objet.
1.2/ Non, dans bien des cas, il permet au contraire des raccourcis qui ne seraient pas permis sans, et donne des existences effectives là on il faudrait taffer pour en trouver. Les groupes de tresses de Dehornoy (certes utilisant AUSSi d'autres ingréients mais pas plus consrtuctifs), le théorème des zéros de Hilbert où Zorn etc, donne directement une solution, etc.
2.1/ Les théories contradictoires sont non constructives.
2.2/ C'est tout l'opposé, elles permettent parfois des constructions auxquels les gens n'auraient pas pensé spontanément. L'énoncé $\forall f\exists x: f(x)=x$ peut donner l'impression qu'on aura du mal à trouver un point fixe, alors qu'avec $e: x\mapsto f(x(x))$, vous avez immédiatement un point fixe parfaitement effectif avec $e(e)$. Ne pas confondre son caractère DEPLAISANT avec son caractère non constructif: certes on en voudrait un autre, mais on a celui-là
3.1/ Un preuve prouvant l'existence d'un objet est généralement capable de produire une preuve constructive qui va l'exhiber.
3.2/ Non!! Ce n'est pas vrai que pour les théories extrêmement faibles et "triviales" (non pas pour l'humain, mais à supposer qu'on dispose d'autant de temps qu'on veut). Evidemment qu'un théorème d'arithmétique se dépliera (en temps long tout de même) en exhibition de l'objet du fait qu'on "essentiellement" identifié $\epsilon_0$ comme la sup de la puissance arithmétique. En pratique, cependant, l'algorithme est hyperexponentiel.
Mais surtout, ça procède d'un très mauvaise vision des maths, et d'ailleurs c'est rigolo, souvent perçue trop platoniquement par ceux-là même qui critique le platonisme. Par exemple, il n'y a pas d'entiers, mais pour ceux-là, qui ont tendance à croire qu'il y en a, ils n'ont pas conscience que les preuves d'existence peuvent être obtenues de façon telles qu'on attestera seulement l'existence de l'objet dans tout univers vérifiant les axiomes. Or les entiers n'existent pas, seuls existent les entiers de l'univers truc, et ça dépend irrémédiablement de Truc.
3.3/ Un exemple simple: soit $(P>Q) :=$ il existe une preuve $r$ dans ZFC que $P\to (\exists Inaccessible(E): E\models Q)$. Soit $T$ l'ensemble des $P$ tels qu'il n'existe pas de suite $P_0:=P>P_1>P_2>..$ infinie descendante.
Intuitivement on pourrait croire que si l'univers est "bien fait" et assez gros, il existe un inaccessible $E$ tel que $\forall P\in T: E\models P$. C'est un exercice basique de 2 lignes de prouver que non. Il existe donc $P\in T$ tel qu'aucun inaccessiible (donc a priori aucun univers aussi gros soit-il) ne $\models P$.
Quel est ce $P$ dont on vient d'otenir l'existence en 2 lignes?
4.1/ C'est la frontière classique / intuitionniste qui joue un grand rôle.
4.2/ Absolument pas. Le raisonnement par l'absurde n'ajoute strictement rien de plus que ce qu'on appelle en informatique une procédure d'interruption des fins de boucles inutiles.
Exemple:
begin a:= true ; for i := 2 to p-1 do if i divise p then a:= false else Nop done return a end
est améliorée par
f(p):= begin a:= true ; for i := 2 to p-1 do if i divise p then begin a:= false; Stop(i) end else Nop done return a end
g(p) := try f(p) EnCasDeStop(x): renvoyer x
4.3/ Il en va très exactement de même de l'axiome ((A=>faux)=>faux)=>A: en effet partant d'une preuve qui supposant (A=>faux) conclut faux, vous la parsez pour trouver où vous utilisez l'hypothèse A=>faux.
4.3.1/ Si vous ne l'utilisez pas, c'est que vos autres hypothèses sont contradictoires.
4.3.2/ Si vous l'utilisez,
4.3.2.1/ ou bien vous fournissez à l'hypothèse (A=>faux) une garantie construite précédemment de A. Il vous suffit alors de récupérer cette garantie
4.3.2.2/ (délégation) ou bien vous utilisez quelque part que (A=>faux)=>B dont vous retrouvez en conclusion de quel hypothèse explicite il est de façon à le rendre redondant.
4.4/ De manière générale, c'est juste la possibilité d'interrompre (et heureusement qu'on peut) AVANT un calcul de $f(x)$ l'exécution d'une garantie afin de prendre connaissance de $x$. Tout bêtement, ça répare l'oubli de la non commutativité de $(f,a)\mapsto f(a)$ qui a donné lieu, dans un premier temps "un peu naif" à l'idée qu'on ne pouvait pas "piquer" son argument à $f$.
4.2/ Le VRAI PROBLEME est la capacité de dupliquer des ressources, choses qui n'a strictement pas de parenté avec la vraie vie.
4.2.1/ Dans un exemple où Anatole m'a prouvé en 5mn que tout anneau tel que $\forall x\exists n>1: x^n=x$ est commutatif, il a réutilisé au moins 2 ou 3 fois l'hypothèse PRINCIPALE
4.2.2/ Quand vous prouvez qu'il n'y a pas de surjection de $E$ sur $P(E)$, vous réutilisez DEUX FOIS de manière absolument irréductible l'hypothèse, ie de $f(a)=\{x\mid x\in f(x) \to Paradis\}$, vous déduisez:
$a\in f(a)\to ( a\in f(a) \to Paradis)$ donc
$[a\in f(a) $ ET $a\in f(a)] \to Paradis$
donc EN ADMETTANT que $a\in f(a) $ implique $[a\in f(a) $ ET $a\in f(a)]$
$a\in a \to Paradis$
Et c'est pas fini. De là, vous avez seulement obtenu $a\in f(a)$. Qu'il va falloir recloner pour gagner le paradis.
4.2.3/ Quand vous prouvez que $9$ est un nombre entier fini, vous devez CLONER 9 fois vos axiomes.
5/ Je compléterai, voilà, je pense avoir évoqué quelques points peu , enfin trop peu engagés dans les débats "politiques", mais qui sont techniquement les plus importants.
En particulier, citer "il n'existe pas d'ensemble de tous les ensembles" comme une "erreur de débutant" est illusoire vis à vis de l'état de la communauté mathématique.
A nouveau, complètement indépendamment de si le reste de ce que tu racontes est justifié ou pas;
et de même considérer qu'elle ne discute pas de fondements, alors que, consensuellement, si, c'est faire une erreur sur le sens des mots (même si tu penses que "fondements" devrait avoir un autre sens, et même si tu peux le "justifier" : ce n'est pas comme ça que les mots marchent)
Et finalement, pour aborder le fond, il ne faut pas non plus oublier que tu te bases sur des axiomes ("toute théorie intéressante est contradictoire", "on cherche des contradictions", "toute phrase écrite a un sens", etc. ) qui ne sont pas consensuels (d'ailleurs je réitère que je n'ai jamais vu personne d'autre les utiliser) et donc en particulier il faudrait peut-être que tu penses à les annoncer comme tels ;-)
(même si bien sûr, comme selon ta doctrine, un lecteur ou une lectrice te lisant les classe comme axiomes : tout ce qui n'est pas justifié est supposé)
Il serait bon qu'un jour tu prennes le temps d'écrire ça, proprement (pas éparpillé dans 10 000 posts du forum :-D ), avec en préambule tes axiomes (qu'on n'ait pas à les lister nous-mêmes, même si en principe on peut : soit généreux ;-) ), et en séparant précisément les parties philosophie (justification de pourquoi toute phrase a un sens par exemple) des parties maths ($e: x\mapsto f(x(x))$, $p:= e(e)$, alors $f(p)= p$). Ce sera plus clair pour tout le monde.
(ou bien que tu trouves d'autres gens qui racontent en substance des choses similaires et qui l'ont écrit)
Ce qui est déplaisant est cette manie de forcer la main des gens sans preuve, en les accusant d'avoir peur ou d'être faibles.
Et faut arrêter de prétendre que les gens sont en désaccord par faiblesse psychologique. Le vrai monde N'EST PAS CONTRADICTOIRE (y a pas d'éléphant rose qui apparaît devant moi en une fraction de seconde). Donc on a besoin d'outils FIABLES c'est-à-dire NON CONTRADICTOIRES pour l'explorer (les résultats qui établissent la très grande difficulté à s'assurer de ça sinon son impossibilité et a maintenir un système décemment expressif ne modifient pas ce besoin; les développeurs de la NASA envoient dans l'espace des objets à plusieurs centaines de millions de dollars: ils ont des restrictions draconniennes sur le contenu de leus programmes interdisant la Turing-complétude notamment: est-ce de la puérilité? ).
Ben voyons, les fondements, c'est fait pour s'asseoir dessus, non ?
Je soupçonne d'ailleurs que la correspondance démo-programme c'est un truc satellitaire de l'absurde.
Cela permet de dire élégamment à la fois des choses qui seraient effacées du forum sinon et aussi sans trop vexer ceux qui font ça dans leur vie privée, par exemple qu'un homme politique peut s’asseoir sur un yaourt sans l'écrabouiller.
Noter aussi que "$a\neq b$" abrège $\neg (a=b)$ qui lui-même abrège $(a=b)\Rightarrow\perp$ (**)
Ensuite on prend $F$ un énoncé quelconque (dans lequel la lettre $x$ n'est pas libre) et $\varphi$ une fonction de choix de $\{0,1\}$, i.e. une fonction telle que pour toute partie non vide $X$ de $\{0,1\}$, $X\in dom(\varphi)$ et $\varphi(X)\in X$. Posons $A:=\left \{x \in \{0,1\} \mid x=0 \Rightarrow F \right \}$ et $B:=\left \{x \in \{0,1\} \mid x=1 \Rightarrow F \right \}$. On a $1\in A$ et $0\in B$ donc $A$ et $B$ sont non vides, posons $a:=\varphi(A) \in A$ et $b:=\varphi(B) \in B$.
On exploite (*).
Si $a=b$ alors comme $a\in \{0,1\}$, $a=0$ ou $a=1$. Si $a=0$, on a $F$ car $a\in A$ (cf définition de $A$) et si $a=1$, $a=b\in B$ donc on a a nouveau $F$.
Si $a\neq b$ (a.k.a. $a=b \Rightarrow \perp$ d'après (**) ): supposons $F$. Alors pour tous $x\in \{0,1\}$, $F$ et donc aussi $x=0\Rightarrow F$ et $x=1\Rightarrow F$ sont satisfaites. Donc par extensionnalité, $A=B=\{0,1\}$. Donc $a=b$. Donc
$\perp$. Donc au final, $a\neq b$ entraîne $F\Rightarrow \perp$.
Finalement on a montré $F \vee (F\Rightarrow \perp)$ ce qui est le tiers exclu..
La preuve que tu me comprends parfaitement, c'est que tu "constates" mes axiomes.
Je suis d'accord que c'est toujours mieux de les lister de manière numérotée, mais si je pouvais je le ferai, j'aurais tendance à dire que pourle moment, j'ai surtout identifié quoi ne pas y mettre.
Au fond tu me dis "annonce ce que tu dis comme des axiomes", or je pense que n'importe qui me lisant voit que ce sont "mes axiomes".
Bon il y a quelques exceptions, concernant le début où je maintiens que l'éternel argument pour bisounours qu'il n'y a pas d'ensemble de tous les ensembles est une erreur en tant que par seule présence dans un texte voulant parler de fondement. C'est du gaspillage d'encre et une incompréhension profonde du fonctionnement de la science qui se fiche éperdument de la suite de signes $\{x\mid x\notin x\}$ et ne la considère pas comme un problème à condition de dire ce qu'on en fait.
En ce sens, les épistémologistes qui laissent ne serait-ce passer qu'une micro-nano-goutelette de sensibilité à ce dessin typographique sans contenu problématique, qui plus est quand c'est pour justifier, fallacieusement, qu'une prétendue autre démarche aurait "surmonté" ce "grave problème méritent qu'on referme le livre qu'ils écrivent à l'instant même où on voit cette blague écrite.
Ce n'est pas tellement un axiome qu'une éthique ici. Et je le répète, je n'accuse personne de malhonnteté, je dis juste que quand ce n'est pas malhonnête, c'est de l'incompétence épistémo-scientifique (à distinguer de l'épistémo-histoire où il est tout à fait naturel de signaler que ça a ému les gens à un moment à l'instar (quasiment en tout point) de la preuve "ontologique"
Bon, je m'en vais lire et me délecter des posts de foys (je vois que la contribution de GBZM est digeste :-D )
@foys je t'ai déjà dit que besoin d eA = non(A)? :-D
Je suis sérieux. Je ne conteste ps ce que tu dis, en rien. Mais je ne vois pas où est le problème. Et après avoir parlé de la vocation non opératoire de la science pour justifier qu'on ait rejeté le LC (ie opposition platonisme / opératoire), tu le ré-évoques pour justifier qu'on a besoin de fiabilité: j'ai du mal à te suivre.
C'est bien pour ça que j'insiste sur le sérieux et la compétence de fond sur ces problèmes et condamne (sans vouloir traiter de faible ou de peureux, comme tu le dis, pardon si la forme stytlistique que j'utilise en donne l'impression) les modes de s'évanouir face à $A:=non(A)$.
J'ai l'impression que tu es entre les deux. Si tu me dis qu'on se restreint au polynomial (ou légèrement plus) pour éviter les non tes terminaisons non voulues d'algorithme, ce n'est vraiment pas moi qui vais te contredire puisqu'au contraire, je n'ai fait que l'expliciter et ranger ça sous le statut de spécialité. J'ai l'impression que sous le prétexte que je dis que les spécialistes du sécurisable (ie du taf dans les théories faibles) forment UNE PARTIE seulement de la science, tu m'accuses de vouloir les rabaisser. Pas du tout!!! Ce que je dis est qu'il ne sont pas spécialisés dans les autres domaines, plus platoniciens, voire, pour certains domaines, à la limite de l'ambition de frôler la folie via tentative de "toucher" à Dieu (enfin l'espèce de Dieu de l'infini si tu préfères), où là, disons-le, et tu sais que je les respecte puisque ce sont mes pairs, la prétention de sécurité est tout sauf élevée.
J'avoue même être un peu étonné de ton gout pour le sécurisé, le typage et COQ, je t'aurais vu plus platonicien, pluss à flirter avec les gens qui veulent aller papoter avec woodin ou Solovay, mais in fine, je m'aperçois que j'avais un préjugé gratuit, car il est tout à fait vrai que tu ne montrais pas de signes spécialement "platoniste", et que c'est vers la CCH que tu t'es formé récemment (moi, la voyant comme une opportunité de purisme expressif, et adapté à étudier les théories contradictoires, j'ai involontairement projeté ça sur l'idée que j'avais de tes gouts, mais maintenant il me revient qu'effectivement tu interviens souvent en "contre-magie" si j'ose dire.
Et je pense qu'il faut y penser, et ne pas faire semblant que tout le monde a le background pour extraire lesdits axiomes
1/ Preuve de la conservativité de l'ajout d'un symbole opérant le choix non extensionnel au dessus de ZF+CD (je veux rester discret, car ça fait 10 lignes et la première partie des longues recherche d'un ami (JLKrivine) qui s'est "trompé" en préjugeant que ça devait peut-être un peu difficile te donc a "grillé" de la réalisabilité dessus
2/ plusieurs pages pour traduire ce que m'a pporté alesha
3/ Probablement plusieurs pages de discussions philo-technique pour tenter d'établir un peu un résumé de mes "validations définitives de position" d'avant (j'ai un peu avancé récemment avec le confinement, mais ça reste encore instable, je ne viens seulement que de découvrir que $)a=b) = -(b=a)$, je ne vais pas l'y inclure.
Ca devrait être prêt et sur HAL avant fin juin vu que c'est récréatif chez moi, pas une obligation corvéeuse que je me fais. J'y réintègrerai ta correction sur les anneaux d'alileurs
@foys et xax, comme je viens de le dire à Max, là encore c'est "une erreur" de percevoir l'axiome du choix comme le héros de la réalisation du RPA. Mais bien plus fréquentes et graves sont les erreurs de Coquand et de toute la communauté qui fait de la CCH sans avoir de connaissance en TDE (on a LC = TDE, et bien des erreurs sont commises par déportation destinée à créer des oppositions artificielles d'ailleurs)
Le génis de la lampe d'Aladin dans cette affaire, c'est l'axiome d'extensionalité. L'axiome du choix n'y joue un rôle qu'à peu près nul et "notationnel".
Foys aurait donc dû écrire:
et non pas
En fait, l'axiome d'extensionalité est "essentiellement" faux, et presque prouvablement, c'est de cet ADN qu'on a tiré sa puissance. LE RPA,lui, par contre, n'est rien, je l'ai un peu détaillé au post de ce matin. Quand à la TDE, déjà, c'est un peu "étrange" et artificiel d'y prouver le RPA, car il est en fait impliqué (ce sera la partie de mon article from Alesha) (ie DEDUCTIBLE) de la TDE, même intuitionniste.
L'intuitionnisme trouve sa fondation dans une assymétrie infligée aux phrases. Elle étudie le positionnement d'un joueur opposé à un n=unique adversaire, mais qui a le droit de dupliquer autant qu'il veut ses copies de lui-même. Ce n'est pas "une logique" au sens où en fait, on voudrait l'entendre, c'est plutôt un protocole asymétrisant certains contextes pour les adapter à ce qu'on veut.
Le RPA n'y est pas faux, il est caché sous l’asymétrie. Pas plus que tu ne peux inverser une application BILINEAIRE allant de $(E^*) \times (E^*)$ dans $\R$, tu ne peux récupérer $A$ à partir d'une preuve de $(A\to Tout)\to ((A\to Tout) \to Tout)$, car tu as "au moins" deux endroits où tu as utilisé l'hypothèse $A\to Tout$. La seule chose que tu peux récupérer mais la logique intuitionniste ne l'implémente pas c'est une sorte de "superposition quantique" entre deux objets différents (et possiblement très différents) qui, dans le passé, ont habité $A$, et ça n'avance pas beaucoup.
Dans l'argument que t'a signalé foys, la fonction choix (a priori pas méchante :-D ) $f$ est interdite de choisir $f(A)\neq f(B)$ quand $A\subset B$ et $B\subset A$ et c'est l'axiome d'extensionalité qui l'exige, ce n'est pas du tout un problème de difficulté de choisir un élément dans $A$ ainsi qu'un élément dans $B$, c'est un problème de "faire semblant de pas savoir que ces deux ensembles sont réclamés égaux par l'extensionalité, alors qu'à l'évidence ils sont différents (ils se comportent juste de la même manière au regard de qui ils acceptent d'être appelés leurs éléments).
*** prouvablement normalisable, car normalisable tout court, ça peut être intéressant pour moi.
Tout à fait, mais tout de même avec une précision. L'axoime d’extensionnalité dit (pour tout le monde):
$$[(A\subset \ et\ (B\subset A)\ et\ (A\in X)] \to (B\in X)$$
(il n'y a pas de égal en TDE)
C'est extrêmement fort, car ça dit qu'un X pour décider si A lui appartient ou pas, non pas connait A (ça l'induirait en erreur), mais uniquement les éléments de $A$. (Un peu comme si un appel informatique $f(g)$ ne pouvait s'exécuter qu'après que $f$ ait visité tous les $g(h)$, afin non pas de connaitre $g$, mais de connaitre son comportement).
Ca n'a pas loupé :-D dans des recherches comme celles de Krivine par exemple, ça s'est avéré un appel au père Noel tellement exorbitant qu'il a fini par mener à des "contradictions intra-paradigmatiques")
Il est à noter aussi que le tiers exclus et l'axiome du choix sont EQUIVALENTS** (sur le fond) VIA l'axiome d'extensionnalité, ce qui ne le rend pas inintéressant puisqu'il "met le doigt là où ça fait mal". Mais il est trop fort, il a tendance à envoyer sur $0=1$ toute hypothèse un peu fine.
** tu n'as signalé qu'un des deux sens, le médiatique à cause du boucan années 2000 des catégoriciens, mais l'autre est en fait le plus significatif car s'exécute avec $J$ (ie le combinateur tel que $\forall x: Jx:=x$, pardon pour mes notations), via :
$$A(E):=\{x\mid x\in Ordinaux\ et\ NoSurjectionDeSur(x,E)\}$$
Vu que c'est dans le sujet, je poste évidemment ici:
1/ Alors un "non" catégorique (et sans jeu de mot :-D ) : la voie d'accès à la logique intuitionniste c'est la logique intuitionniste elle-même, bref, tout cours potable et détaillé. Sa compréhension la plus parfaite est celle donnée par la CCH (correspondance d eCurry Howard). Quelle que soient les qualités des topos, le côté intuitionnisme chez eux est extrêmement artificiel et viole le principe de Girard (pertinent) disant (en simplifiant) que
$$ (A\to_{Intuitionnisme} = ([A^\infty] \multimap $$
(Vois $\multimap$ comme $\to$)
Mieux vaut voir un topos comme une imitation de la théorie des ensembles, mais où on a retiré les fonctions qu'on voulait (avec une marge de manœuvre à peu près totale). De ce fait la logique intuitionniste arrive "comme un sauveur" de l'outil, et non comme émergeant de l'outil. Si tu retires des trucs, il va aussi falloir retirer les preuves qu'ils sont là :-D
C'est très puissant. Je dis un truc totalement au hasard, mais ça te donne une idée de la puissance. Je décide capricieusement de retirer toutes les fonctions non constantes. Ca fait du monde!!!! Bin si je veux récupérer une théorie à peu près utilisable, va ptet bin falloir que je retire aussi pas mal de garanties que les fonctions ne sont pas toutes contantes :-D (J'ai pris un truc farfelu très peu probablement réalisable par les topos, je suis béotien en topos, j'ai juste découvert leur nature grace à un théorème dû à un autre intervenant (Alesha)).
2/ Connes se trompe (ou ne dit pas ce que Lapin lui fait dire). En général, il se trompe peu, mais ça arrive (j'ai écouté quelques discours). Il mélange TQ et topos, et fantasme un peu à cheval sur les 2. Or la TQ n'autorise pas plus LA DUPLICATION A GAUCHE qu'elle ne l'autorise A DROITE. Les topos ne servent a priori à rien dans l'étude de la TQ (ce qui n'exclut pas que de temps à autre un quidam ponde des liens artificiels dans article), car la TQ c'est avant tout que les phrases ne sont pas idempotentes (or en LI, elles le sont).
Par ailleurs, les topos ont un besoin congénital (c'est dans leur ADN catégoriel) de flèches. La TQ est allergique au flèches et c'est un des grand problèmes ouvert actuel. Ceci provient ce que les flèches peuvent tourner de manière CONNEXE, ie il n'y a pas de séparation entre "=>" et "<=" en TQ: même composante connexe. A moins d'inventer des topos sans flèche :-D (Alors même qu'ils ont viré justement tout le reste et qu'il ne reste que leur flèche pour être exressifs, les objets n'étant que des "ordinaux" (c'est spécifique aux topos) sans les flèches). A noter que la LI aussi a un très profond besoin de flèches. La LI sans flèche crève de faim très vite.
Quel intérêt d'aller s'enfermer dans des catégories étriquées alors que "pour une fois" on a un dispositif parfaitement clair et formel, calculable, et qui n'est pas contradictoire. A moins de vouloir le mimer de manière empotée en le répétant (par exemple, en dotant la catégorie de pouvoir magiques qu'on rajoute gratuitement à titres d'hypothèses, mais dans ce cas pourquoi ce tournage en rond inutile), autant l'utiliser tel qu'il est.
A la rigueur, je peux comprendre la volonté de recherches de super-consistances quand il s'agit de théories potentiellement contradictoires, mais quand on a une théorie qui ne l'est pas (l'implémentation théorique du LC ne dépasse guère Peano), là, j'avoue... :-S
Quant à l'aspect "machine", bien sûr que si si selon moi c'est une nécessité. La CCH c'est JUSTEMENT CA (le fait qu'une preuve est un circuit de machine "qui va marcher"). Donc sans les machines, on perd l'ADN même de la CCH. Si c'est juste pour se toucher le marron avec des airs snobs et complexes à parler de type dépendant de dépendant de polymorphes, et ceci et de cela, la CCH n'a aucunement besoin de servir d'excuse. On peut faire des catégories, ça marche très bien :-D
C'est lui qui m'avait fait remarquer que la topologie servait parfaitement de sémantique pour la logique intuitionniste. Je ne le savais pas avant.
Je pense personnellement que Max détecte à travers ce ressenti un truc très simple, que je vais caricaturer:
- l'algèbre est consistante
- l'analyse est contradictoire.
L'analyse est parfaitement structurée, mais est "essentiellement" contradictoire (même si ça ne se voit pas "comme ça" à l'heure actuelle, car on a bridé ZF pour que les contradictions ne soient pas a priori immédiates et déjà trouvées). Du coup, évidemment, on ne peut pas l'aborder comme l'algèbre.
J'en profite pour commenter un témoignage de Foys, lui-même grand savant (Max en est un futur).
Rebelotte: expressivité VS consistance.
Il n'y a pas mieux placer que les théoriciens des ensembles pour savoir que croire ou ne pas croire à ZF n'a pas de sens. Woodin et Shelah le confirmeraient sans problème.
Krivine qui a abandonné la TDE "dure et platonicienne" mais a toujours maintenu sa forme il y a 30ans s'exprime comme suit (source = moi, je l'ai bien entendu et il me parlait à moi): "mais la lune, le soleil, tout ça, n'existe pas, ce ne sont que des illusions, des constructions. Par contre ..."
Ce qu'il se passe est simple: on a une correspondance canonique entre expressivité et consistency-strength, totalement absolue et indépassable, c'est aussi bête que ça. il y a donc une forme "d'erreur" à espérer tirer de l’expressivité sans payer le prix de l'augmentation du risque de contradiction.
En plus l'avantage, là, c'est que ce sont des théorèmes très simples qui les imposent. Ca pourrait se diffuser. Dommage.
Je prends un exemple: il y a une propriété "fermée" (la fermeture indique presque la compacité, sauf que là c'est dans $\N^\N$ hélas, donc non), de l'ensemble d'énoncé du langage de Peano, par exemple, qui garantit qu'il est le seul à l'avoir. Autrement dit, par exemple (mais c'est général), il suffit de dire que ce que vous trouvez évident (ie pour Peano que $\forall R$ définissable (suite de signes) $[\forall xR(x)] \in A \iff $ il existe $n\in \N: [R(n)\in A] $ ) et même dont vous parlez informellement tout le temps sans en avoir vraiment conscience existe pour faire monter strictement le risque de contradiction (l'existence de A suffit à prouver cons(Peano)).
C'est absolument systématique, et ça porte de le nom de procédé diagonale, ie vous passez des $x\mapsto Something(a,x)$ à la diagonale
$$ x\mapsto Something(x,x) $$
rien de plus.
Ca s'appelle ou devrait s'appeler détyper :-D
Voilà entre autre les raisons qui font du typage une augmentation de consistance, mais une perte d'expressivité, mais aussi une information claire qui est que le détypage est une condition nécessaire à l'augmentation d'expressivité (c'est un théorème que j'ai prouvé pour un autre contexte, si j'ai le courage, j'en mettrai une preuve)
Je donne une sorte de "pseudo-preuve" à toi et Foys, vraiment pseudo hein.. :-D
J'ai remarqué que Foys est sensible à l'argument que si $A = [(!A) \to \perp]$ alors tout collapse. Or, il est senbie aussi au fait que ce coup-ci, on n'a pas dupliqué sans l'assumer une ressrouce, ce qui pourrait a priori sembler une sorte d'argument qu'il n'y a pas d'espoir à accepter d'affaiblir la logique plutôt que brider la compréhension langagière (ie le fait que toute fonction est un élément ou que toute collection est un ensemble)
Bon, il n'en est en fait rien, c'est juste du transfert.
1.1/ Tout d'abord, comment "fait-on" exister $(!A$$ (qui signifie "à volonté $A$", ou qu'on peut noter suggestivement $A^\infty$ )
1.2/ Réponse (si on ne veut pas juste le supposer), avec un background ordinal :-D : on part de $u_0:=A$, puis $u_{i+1}:= inf(u_i \otimes u_i,1)$ et aux étapes limites on prend l'inf. On s'arrête quand ça ne bouge plus. Certes, très bien, mais on vient carrément de supposer qu'il y a strictement plus d'ordinaux que de phrases :-D
2.1/ Il est donc intéressant de montrer que c'est une idée "érronée": considérons un petit paradigme dans lequel la naturalisme godélien est respecté, ie $A^+$ signifie "il existe un modèle de $A$" et on considère qu'au niveau $0$ rien n'est consistant, ie $A^+$ est faux pour tout $A$ au niveau $0$.
2.2/ Soit $W$ la phrase qui affirme $\forall X: [X\to X^+]$. Soit $a$ le plus petit niveau ordinal d'un modèle de $W$. comme $W\to W^+$, il suit qu'il existe un niveau $<a$ avec un modèle de $W$, contradiction. Donc aucun niveau ne tolère $W$, autrement dit pour tout niveau $a$, il existe $A(a)$ tel que $A$ est vrai et $A^+$ est faux à ce niveau. La croissance fait que $a\mapsto A(a)$ est une injection de ON dans l'ensemble des phrases.
3/ Il n'y a aucun moyen de sortir de ce cercle, l'expressivité c'est ce que font depuis longtemps les platoniciens (set theorists plus spécifiquement), c'est "dégrader" le fait que $[a=a$ et $a\neq a]$ => Tout ce qu'on veut. Alors, la zoologie et évidemment amusante, ça va de Ramsey aux grand cardinaux (avec chaque fois, c'est important de le noter, des THEOREMES qui disent "si on fait ça, alors tous les théorèmes des matheux deviennent triviaux*** car blabla) mais de toute façon, on n'en sort pas. L'analyse est infinitiste. Et l'étape suivante, qui n'a pas été trouvée qui au lieu de se contenter de $a==a$, mais $a\neq a$, avec l'inconvénient que c'est bien ordonné, est une étape où on "réussira" $(a,b)==(b,a)$ "mais" $a\neq b$. (Déhiérarchisation, y a plus "le chef" qui résout le problème de l'arrêt de ses subalternes)
*** c'est connu mais complexe, je ne connais plus les hypothèses, mais je l'ai évoqué récemment sur un exemple, le théorème des zéros où une procédure EFFECTIVE marche .. à coup de père noel exagérément sollicité (autrement dit: sollicité un peu, il donne unepreuve facile non constructive, sollicité beaucoup il donne un alog hypersimple SANS PREUVE, et pas sollicité du tout, il donne probablement le même algo similaire, mais avec des preuves usinez à gaz que seuls les algébristes chevronnés gèrent). On le voit aussi très bien sur le fait que l'ensemble vérité de l'arithmétique (et même de l'univers ZF, c'est le même principe) est récursivement réductible à l'ensemble des colorations très simples qui admettent un Ramsey homogène (ie $\forall x\exists y\forall z$ ne s'écrit plus comme ça ou avec des témoins de skolem (le tau de Bourbaki), mais s'écrit $\{(a,b,c) \mid \forall x<a\exists y<b\forall z<c: ..\}$ est Ramsey positif (la relation est NP et je n'ai pas "tiré fort", on peut le faire avec des relations P)
B-)-
Heureusement, je viens d'aller chez le coiffeur, et la coupe à raz me redonne un aspect un peu sérieux même si "mafieux"
J'en étais rendu, en les coupant moi-même au rasoir à risquer la camisole en pleine rue, les gens de mon quartier se mettaient à me parler comme si j'étais vraiment le simplet du village (à cause de la coupe, vraiment incroyablement pas crédible) bon certes, avec un grand sourire, j'avais l'air de bcp les amuser, donc camisole peu risquée (en plus à Paris avec l'indifférence..)
mais tu n'avais pas déjà un problème de "foie gras" cc ?