Pensez à lire la Charte avant de poster !

$\newcommand{\K}{\mathbf K}$


Les-Mathematiques.net - Cours de mathématiques supérieures
 Les-Mathematiques.net - Cours de mathématiques universitaires - Forum - Cours à télécharger

A lire
Deug/Prépa
Licence
Agrégation
A télécharger
Télécharger
253 personne(s) sur le site en ce moment
E. Cartan
A lire
Articles
Math/Infos
Récréation
A télécharger
Télécharger
Théorème de Cantor-Bernstein
Théo. Sylow
Théo. Ascoli
Théo. Baire
Loi forte grd nbre
Nains magiques
 
 
 
 
 

Que doivent faire les fondements ?

Envoyé par Maxtimax 
Que doivent faire les fondements ?
il y a sept semaines
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 !

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Que doivent faire les fondements ?
il y a sept semaines
Merci pour le spoiling.

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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a sept semaines
Attention, justement elle ne parle pas d'unification - enfin "unification" c'est un des points qu'elle met dans les rôles de fondements (deux points plus précisément : "Generous Arena" - "arène généreuse" - et "Shared Standard" - "standard commun"), mais absolument pas l'entièreté de ce qu'elle considère comme "fondationnel"

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 winking smiley

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

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Que doivent faire les fondements ?
il y a sept semaines
Fonder veut dire "donner des règles de base explicites". Par exemple le jeu de go et le jeu d'échecs sont fondés.

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

Citation
christophe c
C'est d'autant plus important que nous travaillons tous dans des théories contradictoires,

Où est cette preuve que ZFC |- 0=1?
Moi je veux la lire.



Edité 2 fois. La dernière correction date de il y a sept semaines et a été effectuée par Foys.
Re: Que doivent faire les fondements ?
il y a sept semaines
Foys : certes, mais la problématique dépasse "acceptable" - Maddy se pose la question de "ce qu'on veut/ce dont on a besoin pour faire nos maths sans être gêné.e"
(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)

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell



Edité 1 fois. La dernière correction date de il y a sept semaines et a été effectuée par Maxtimax.
Re: Que doivent faire les fondements ?
il y a sept semaines
@Max: je vais lire, je l'ai d'ailleurs téléchargé (on dirait qu'il a été tapé à la machine à écrire)...

@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 $<<$ grinning smiley $>>$, je réécris sans :

$ \forall R\exists a$ (prendre $a:=R$ grinning smiley ) $ \dots $


Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a sept semaines
@Maxtimax Je n'arrive pas à télécharger ton texte :(

J'ai une erreur 404
Re: Que doivent faire les fondements ?
il y a sept semaines
20-sided-dice : effectivement j'ai le même problème, il a l'air d'avoir été retiré confused smiley

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

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Que doivent faire les fondements ?
il y a sept semaines
Sinon le voilà en pièce jointe.
Pièces jointes:
ouvrir | télécharger - What_do_we_want_a_foundation_to_do_Compa.pdf (133.9 KB)
Re: Que doivent faire les fondements ?
il y a sept semaines
Personnellement en tout cas, j'inverserais les mots: l'unification doit "se préoccuper" des fondements, en particulier les grumeaux restés trop en aval, pour bien unifier.

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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a sept semaines
avatar
Bonsoir,

Le document est extrait de ce livre.

Bien cordialement,

Thierry
Re: Que doivent faire les fondements ?
il y a six semaines
J'ai traficoté avec chrome pour en faire une traduction en français par google, que j'attache et vais maintenant lire (j'ai essayé de casser les paragraphes avec des sauts de lignes)

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Pièces jointes:
ouvrir | télécharger - enfrancaisFourniparMaxFoundations.tex (64 KB)
Re: Que doivent faire les fondements ?
il y a six semaines
Bon je n'ai bien sûr pas tout lu, mais j'ai un peu l'habitude de ces textes donc sais vite où aller chercher des indices que l'auteur traite le problème en profondeur ou pas.

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:

Citation

Il n'y a pas d'ensemble de tous les groupes ou ensemble de toutes les catégories pour la même raison qu'il n'y a pas d'ensemble de tous les ensembles: les ensembles sont formés dans une série transfinie d'étapes, et il n'y a pas d'étape à laquelle tous (ou tous ceux qui sont groupes ou tous qui sont des catégories) peuvent être collectés.


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.

Citation

La première objection est que la théorie des catégories traite de catégories illimitées, comme la catégorie de tous les groupes ou la catégorie de toutes les catégories ou la catégorie de tous les X mathématiques, mais rien de tel ne peut être trouvé dans l'univers des ensembles.

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

Citation

Grothendieck a surmonté ce problème en posant une séquence sans cesse croissante d '«univers locaux» et en notant que toute activité théorique de catégorie peut être réalisée dans un assez grand d'entre eux. En termes de théorie des ensembles, cela consiste à ajouter des cardinaux inaccessibles,

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

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
De mon point de vue (peut-être peu intéressant mathématiquement, mais bon) : pour se poser la question "quel rôle veut-on attribuer aux fondements des mathématiques ?", je prendrai un angle encore un poil différent. Je dirais que la réponse est "évidente" (évidemment, elle ne l'est pas, je fais exprès) : on veut donner un cadre unique, unifié, de toutes les mathématiques. Ben, oui, dit comme ça, c'est évident au point de devenir bête... mais ça déplace la question. Si l'on veut unifier les mathématiques, autant se demander, c'est quoi les mathématiques ? La réponse est tout aussi peu évidente ici, mais je pense qu'il faut se la poser, cette question.

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.

"En mathématiques, on ne comprend pas les choses, on s'y habitue." - von Neumann
Re: Que doivent faire les fondements ?
il y a six semaines
@ Christophe
Je n'arrive pas à ouvrir ton fichier enfrancaisFourniparMaxFoundations.tex (64 KB).
Pourrais-tu le convertir en PDF ? Merci.
Re: Que doivent faire les fondements ?
il y a six semaines
Personnellement, de toute façon, et je pense qu'on n'est pas encore sorti de cette époque archaïque, il est probable que les gens habitués à me lire sur le forum seront sous-pessimistes, qui consiste à rechercher la consistance en même temps que la contradiction. C'est de la shcizophrénie pure et simple!

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" grinning smiley ) 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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
@Chaurien, mais il te suffit de le renommer avec l'extensin ".txt", c'est en fait ce que j'ai fait dans l'autre sens pour quele forum l'accepte (il ne prend pas les ".txt").

Et oui, si tu veux je le convertirai (mais ça me prendra un peu de temps car il est mal formaté)

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
Merci, je n'y avais pas pensé, et pourtant je fais couramment du tex->txt pour poster ici.
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.
Re: Que doivent faire les fondements ?
il y a six semaines
Merci, bin, de toute façon, j'ai trouvé ça "pas mal traduit".

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
Je vais essayer de compléter ce que j'ai dit au dessus avec quelques exemples "typiques" qui invalident les slogans usuels qu'on prononce pour affirmer des oppositions entre bords.

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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
Christophe (à propos des messages avant le dernier) : il peut être bon de noter que, indépendamment de si tu as raison ou pas sur le fond, je n'ai jamais entendu personne d'autre définir "fondements" comme tu le fais.
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 winking smiley
(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 grinning smiley ), 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 winking smiley ), 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)

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell



Edité 1 fois. La derni&egrave;re correction date de il y a six semaines et a &eacute;t&eacute; effectu&eacute;e par Maxtimax.
Re: Que doivent faire les fondements ?
il y a six semaines
Citation
christophe c

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)$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à
Je n'ai jamais aimé cet exemple issu de la récursivité parce que dans cette dernière on ne manipule pas vraiment des affirmations mais des instructions (faites ceci-cela et faites ces copies ...). Le lambda calcul avait été effectivement inventé par Church pour servir de fondement logique. Mais il (précisément: sa version non typée) a été presque aussitôt déchu de ce rôle pour cette raison (les combinateurs de point fixe n'étant pas vraiment durs à trouver).

Citation
christophe c
Ne pas confondre son caractère DEPLAISANT avec son caractère non constructif

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é? ).



Edité 2 fois. La derni&egrave;re correction date de il y a six semaines et a &eacute;t&eacute; effectu&eacute;e par Foys.
Re: Que doivent faire les fondements ?
il y a six semaines
Que doivent faire les fondements ?

Ben voyons, les fondements, c'est fait pour s'asseoir dessus, non ?
xax
Re: Que doivent faire les fondements ?
il y a six semaines
avatar
3.1/ J'ai lu que Coquand dit que ce qui est emmerdant, c'est la démo par l'absurde.
Je soupçonne d'ailleurs que la correspondance démo-programme c'est un truc satellitaire de l'absurde.
xax
Re: Que doivent faire les fondements ?
il y a six semaines
avatar
@GaBuZoMeu tu confonds avec les questions d'ordre sémantique.

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.
Re: Que doivent faire les fondements ?
il y a six semaines
Citation
xax
3.1/ J'ai lu que Coquand dit que ce qui est emmerdant, c'est la démo par l'absurde.
Je soupçonne d'ailleurs que la correspondance démo-programme c'est un truc satellitaire de l'absurde.
Il y a des solutions ad-hoc (Diaconescu, mais on suppose donnés des mécanismes encore moins constructifs comme l'axiome du choix) ou des nnouveaux paradigmes comme la réalisabilité classique.
xax
Re: Que doivent faire les fondements ?
il y a six semaines
avatar
Le Diaconescu qui exhibe le tiers-exclu avec l'axiome de choix ? La réalisabilité classique je connais et si c'est récent je suis trop à la rue pour me représenter ça. Je ressens juste que c'est important.
Re: Que doivent faire les fondements ?
il y a six semaines
Oui, en gros dans ZFC par exemple, on part du fait que pour tous $x,y \in \{0,1\}$, il est intuitionnistiquement prouvable que $x=y$ ou $x\neq y$ (*)(car un objet $u$ appartient par définition à $\{0,1\}$ si et seulement si $u=0$ ou $u=1$ puis on distingue les cas $x=y=0$, $x=1$ et $y=0$, $x=0$ et $y=1$ et $x=y=1$).
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..



Edité 4 fois. La derni&egrave;re correction date de il y a six semaines et a &eacute;t&eacute; effectu&eacute;e par Foys.
Re: Que doivent faire les fondements ?
il y a six semaines
Citation
Maxtimax
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

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 grinning smiley )

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
Citation
foys
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é?

@foys je t'ai déjà dit que besoin d eA = non(A)? grinning smiley

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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
Tes axiomes je (ou Foys, ou d'autres, certainement, sur le forum) les constate, mais beaucoup de gens (je pense notamment à des débutant.e.s en logique, ou plus généralement en maths) ne les constatent pas, c'est pour ça que je disais ça winking smiley
Et je pense qu'il faut y penser, et ne pas faire semblant que tout le monde a le background pour extraire lesdits axiomes

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Que doivent faire les fondements ?
il y a six semaines
T'inquiète, j'y pense, j'ai commencé rédiger un article, où j'intègre:

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 écrire:



Citation

supposons F. Alors pour tous blabla et donc aussi blabla sont satisfaites. Donc par extensionnalité blabla. Donc a=b. Donc blabla. Donc au final, blabla entraîne blabla

et non pas


Citation

supposons F. Alors pour tous blabla et donc aussi blabla sont satisfaites.Donc par extensionnalité blabla. Donc a=b. Donc blabla. Donc au final, blabla entraîne blabla


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 grinning smiley ) $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).

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi



Edité 1 fois. La derni&egrave;re correction date de il y a six semaines et a &eacute;t&eacute; effectu&eacute;e par christophe c.
xax
Re: Que doivent faire les fondements ?
il y a six semaines
avatar
Bon merci beaucoup Foys et Christophe, j'ai lu avec attention, comme souvent vous êtes d'une remarquable générosité dans vos explications. Bon vu mon niveau de compétence je vais pas prendre parti, mais peut-être simplement que Foys travaille sur des systèmes réels et dans ce cas le goulot de la CCH est peut-être un passage obligé (je dis ça comme ça c'est peut-être une connerie).
Re: Que doivent faire les fondements ?
il y a six semaines
Il n'y a pas d'opposition technique entre nous, je crois surtout que je n'avais "pas vu" (du fait de sa maitrise de l'infinitisme et des autoréférences, plus affichée que d'autres experts du forum) juste qu'il "préfère" l'encadrement par des règles de garanties de consistance assez basse, et le fait qu'il ait acquis le lambda-calcul ici même (enfin pendant la période où il venait AUSSI ici en parler) m'a induit en erreur sur son intention de s'envoyer des gros kiffs à coups de points fixes itérés. Peronnellement, tu me proposes un terme fortement normalisable***, je pars en disant "non merci", et j'ai un peu trop appliqué ça à mon camarade en face qui lui les aime, je pense, c'est tout.

*** prouvablement normalisable, car normalisable tout court, ça peut être intéressant pour moi.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
En fait je ne crois pas à ZF mais je crois à la consistence de ZF (oui c'est bizarre mais j'assume). Donc je me sers de ces théories pour établir des certitudes, mais aussi en raison de leur pouvoir expressif insurpassable (la pratique de logiciels non basés sur ZFC vous fait bien sentir les outils qu'ils vous manque. Au passage il n'y a pas d'extensionnalité dans COQ, c'est pour ça que j'ai pensé spontanément à citer cette propriété. La preuve ci-dessus est l'adaptation d'un fichier que j'avais écrit pour moi-même. Pour ta remarque sur le fait que c'est "faux", je pense que l'extensionnalité fait partie de l'identité des théories des ensembles, sans ça ce ne sont plus des ensembles i.e des contenants mais plutôt des prédicats ou autre chose). Je ne sais pas ce que font les spécialistes comme Woodin, ou Shelah ou autres (mes connaissances de théorie des ensembles au delà des définitions sont très limitées).
Re: Que doivent faire les fondements ?
il y a six semaines
Citation
Foys
Pour ta remarque sur le fait que c'est "faux", je pense que l'extensionnalité fait partie de l'identité des théories des ensembles

Tout à fait, mais tout de même avec une précision. L'axoime d’extensionnalité dit (pour tout le monde):

$$[(A\subset B)\ 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é grinning smiley 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)\}$$

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
En réaction à Jean-Louis dans [www.les-mathematiques.net]

Vu que c'est dans le sujet, je poste évidemment ici:

1/ Alors un "non" catégorique (et sans jeu de mot grinning smiley ) : 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} B) = ([A^\infty] \multimap B) $$

(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à grinning smiley

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 grinning smiley (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 grinning smiley (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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
On peut faire de la CCH dans les catégories cartésiennes fermées, ça permet de retirer l'aspect "machine" qui n'est pas une nécessité. On peut faire ça dans des catégories plus générales (ex: monoïdales symétriques) pour récupérer la logique linéaire (un fragment en tout cas).
Re: Que doivent faire les fondements ?
il y a six semaines
On ne fera jamais de CCH, selon moi, autrement qu'en faisant du lambda-calcul pur, bien "cashement". Pourquoi vouloir se limiter?

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... confused smiley

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 grinning smiley

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
Pour les lecteurs qui ne viendraient pas ici par le fil auquel j'ai réagi je mets ce lien vers l'explication très concise de GBZM: [www.les-mathematiques.net]

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.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
Je réagis à une phrase de Max dans u nautre fil, car elle illustre comment la recherche voit de bons éléments s'orienter pas forcément vers le plus fécond pour elle.

Citation
Maxtimax
Pas au sens "un anneau est une structure", mais au sens "on recherche des structures communes dans l'univers, des schémas récurrents", des choses qui sont.
Cette recherche de structure je ne la retrouve pas en analyse. J'ai l'impression que tout y est chaotique

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

Citation
Foys
En fait je ne crois pas à ZF mais je crois à la consistence de ZF (oui c'est bizarre mais j'assume). Donc je me sers de ces théories pour établir des certitudes, mais aussi en raison de leur pouvoir expressif insurpassable (la pratique de logiciels non basés sur ZFC vous fait bien sentir les outils qu'ils vous manque. Au passage il n'y a pas d'extensionnalité dans COQ, c'est pour ça que j'ai pensé spontanément à citer cette propriété.

[...]

. Je ne sais pas ce que font les spécialistes comme Woodin, ou Shelah ou autres (mes connaissances de théorie des ensembles au delà des définitions sont très limitées).

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 grinning smiley

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)

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
Bah je sais pas si c'est ça (tu sais peut-être mieux expliquer mes sentiments que moi - je dis ça sans ironie, me connaissant ce ne serait pas surprenant) mais si oui, sache que je n'en suis pas encore à ton niveau, je préfère travailler dans des trucs consistants grinning smiley

"Mathematics, rightly viewed, possesses not only truth, but supreme beauty"-Russell
Re: Que doivent faire les fondements ?
il y a six semaines
Tu as un niveau incomparablement plus élevé que le mien, identifier des sentiments "intellectuels" n'est pas la même activité.

Je donne une sorte de "pseudo-preuve" à toi et Foys, vraiment pseudo hein.. grinning smiley

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 grinning smiley : 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 grinning smiley

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)

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
Un lancé de fleurs en ce vendredi ensoleillé :

Citation
Maxtimax
sache que je n'en suis pas encore à ton niveau

Citation
CC
Tu as un niveau incomparablement plus élevé que le mien

smoking smiley
Re: Que doivent faire les fondements ?
il y a six semaines
Je précise que je ne drague pas maxtimax, il serait horrifié s'il me voyait, et le confinement m'a fait prendre des kilos, vraiment malvenus et différentiels.

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

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Re: Que doivent faire les fondements ?
il y a six semaines
Citation
CC
et le confinement m'a fait prendre des kilos

mais tu n'avais pas déjà un problème de "foie gras" cc ?
Re: Que doivent faire les fondements ?
il y a six semaines
Hélas oui. On va se régaler quand on me mangera.

Signature: aide les autres comme toi-même car ils SONT toi, ils SONT VRAIMENT toi
Seuls les utilisateurs enregistrés peuvent poster des messages dans ce forum.

Cliquer ici pour vous connecter

Liste des forums - Statistiques du forum

Total
Discussions: 143 249, Messages: 1 414 339, Utilisateurs: 26 477.
Notre dernier utilisateur inscrit ponyo.


Ce forum
Discussions: 2 298, Messages: 46 731.

 

 
©Emmanuel Vieillard Baron 01-01-2001
Adresse Mail:

Inscription
Désinscription

Actuellement 16057 abonnés
Qu'est-ce que c'est ?
Taper le mot à rechercher

Mode d'emploi
En vrac

Faites connaître Les-Mathematiques.net à un ami
Curiosités
Participer
Latex et autres....
Collaborateurs
Forum

Nous contacter

Le vote Linux

WWW IMS
Cut the knot
Mac Tutor History...
Number, constant,...
Plouffe's inverter
The Prime page