Non mais évidemment que la syntaxe de HoTT peut être codée dans ZF, ce n'est pas du tout la question... que tout ce qui est syntaxique puisse s'écrire dans ZF, je ne l'ai jamais remis en question et ce serait idiot de le faire.. mais HoTT n'est pas une "théorie du premier ordre", en tout cas telle qu'elle est écrite, c'est là que vient mon "défi".
Ensuite pour les vidéos franchement t'exagères. Science4All fait de la vulgarisation, évidemment qu'il va pas t'apprendre grand chose si tu fais des maths...
Christophe : encore une fois, tu me fais dire des choses que je n’ai jamais dites ni pensées !
Évidemment que remplacer le signe $\in$ par $:$ ne change rien. Le but de mon message était de souligner que $\mathbb{N}\in 2$ possède un sens en théorie des ensembles mais pas en théorie des types.
faudra que tu m'expliques alors pourquoi quelques messages plus haut tu disais que c'était une "faute scientifique" d'essayer de l'avoir
La réponse est contenue dans le post où je le dis justement. Collapse trop tendancieux quand on prétend FONDER. Une fois de plus, je rappelle que ma critique ne porte absolument pas sur le travail réalisé, en particulier, je ne mets aucunement en cause les progrès de la recherche en géométrie et topologie algébrique et je n'ai pas l'once d'un micro gramme de doute envers les qualités de Voedovski et compagnie.
Qu'on prouve des théorèmes de la forme (univalence => X) n'est absolument pas mon sujet ici. Parfois j'ai l'impression non pas de ne pas être compris, mais de ne pas être lu (ce qui ne serait pas scandaleux). Mais attention, si on répond à des trucs sortis de contexte, ça finit par tourner en rond.
Je le redis, ma prolixité provient de:
1/ L'amateurisme et la non-expertise d'un certain nombre de gens qui CROIENT et ESPERENT des merveilles, espérances qu'ils tirent des PUBLICITES (incontestables, je peux mettre d'autres videos, ou renvoyer un lien vers des articles "image des maths - CNRS"). Ces gens seront très déçus une fois (si ça arrive) initiés
2/ La pub mensongère (prétendre parler de fondements)
3/ L'impression (pas si involontaire) que donnent les experts en laissant croire à ces gens que ce n'est pas fait dans ZF (ils requalifie leur utilisation de ZF comme un ZF métamaths, et pensent ainsi "changer les affaires", mais les néophytes pensent eux REELLEMENT que ce n'est pas construit ensemblistement)
4/ La complication volontaire (500 pages), qui participe à la chimère.
En aucun cas, je ne critique l'actyivité mathématique en soi qui tourne autour de ça. (Revoir le lien que j'ai mis vers le gars de la Rochelle qui a fait un pdf humoristique "sympa" pour dénoncer (plus que gentiment) ces 4 phénomènes).
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Le but de mon message était de souligner que $\N\in 2$ possède un sens en théorie des ensembles mais pas en théorie des types.
Je te fais dire EXACTEMENT ce que tu viens de dire toi-même, à savoir que $(\N\in 2)=NoSens$. Crois-tu que ça change quelque chose de dire qu'une suite de caractère n'a pas de sens, plutôt que de dire qu'une suite de caractères a la valeur $NoSens$?
Crois-tu que HoTT soit le premier système qui ne taffe pas dans $\{vrai; faux\}$?
Je t'ai compris, en tout cas, je le pense sincèrement, mais je pense que c'est toi qui m'attribue une difficulté à te comprendre. La logique valuée à 3 valeurs : vrai; faux; non sensé a des règles de fonctionnement parfaitement syntaxiques et récursives. Ce n'est pas parce que tu vas déclarer ça "métamaths" et que tu vas y changer quelque chose OPERATOIREMENT. En outre, ça fait longtemps qu'on a fait bien mieux et qu'on a structuré de façon réfléchie les valeurs que peuvent prendre les phrases, et en aucune façon, on s'est arrêté au rudimentaire ajout de $NoSens$.
Encore une fois, je pense qu'il est important d'insister sur l'importance de l'opératoire, surtout pour une théorie qui se permet de défendre une super-extensionalité éjectant les différences entre 2 relations non isomorphes, sous peine d'y voir une sacré incohérence cynique interne.
Encore une théorie de l'âme qui NIERAIT FORTEMENT toute forme d'extensionalité, je veux bien qu'elle pourrait se prévaloir d'associer un peu de culte aux mots isolés. Mais surement pas une théorie qui s'attache à identifier les structures isomorphes.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
christophe c écrivait :
> Crois-tu que ça change quelque chose de dire qu'une suite de caractère n'a pas de sens,
> plutôt que de dire qu'une suite de caractères a la valeur $NoSens$ ?
Oui.
> Crois-tu que HoTT soit le premier système qui ne taffe pas dans $\{vrai; faux\}$ ?
Peux tu prouver QU'OPERATOIREMENT il y a un e différence entre dire "N:2" n'a pas de sens et dire (N:2)=NoSens.
À un moment il faut être sérieux ce n'est pas en jouant sur les mots ou les expressions que tu vas changer quelque chose. Précisément, peux-tu me signaler un logiciel de calcul qui " ne sait pas quoi faire et fait exploser l'ordinateur et ftout un incendie à ton apart quand tu entres 3/0"?
J'ai l'impression que tu ne sais pas que les maths sont robustes. Il y a le récursivement enumerable et le reste. Personne n'a jamais écrit que l'ensemble des theoremeS de HoTT n'est pas récursivement enumerable jusqu'à present sur le forum. Si tu m'affirmes que c'est le cas on parlera technique. En attendant j'attends ta preuve.
Si HoTT taffe dans vrai faux (je pense que tu te trompes mais bon) il utilise la logique classique et à pas mal de retard compare aux topos et autres systèmes. Je suis donc étonné par ta réponse.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
christophe c écrivait:
> Peux tu prouver QU'OPERATOIREMENT il y a une différence entre dire "N:2" n'a pas de sens et
> dire (N:2)=NoSens.
Même s’il n’y avait aucune différence opératoire (ce que je pense), pour moi il est préférable qu’une théorie interdise l’énoncé $\N\in 2$.
Entre deux théories opératoirement équivalentes, je préfère mettre de côté celle qui autorise un énoncé comme $\sin \in \exp$.
Dans une perspective de fondation des maths, c’est très important de se demander : veut-on qu’en maths l’énoncé $\N\in 2$ soit valide ?
> Si HoTT taffe dans vrai faux (je pense que tu te trompes mais bon) il utilise la logique classique
> et à pas mal de retard compare aux topos et autres systèmes. Je suis donc étonné par ta réponse.
Je t'ai signalé un théorème. Pas une opinion. Apparemment, tu parles en néophyte (ou alors, je ne sais pas, montre que tu sais de quoi tu parles?)
Même s’il n’y avait aucune différence opératoire (ce que je pense), pour moi il est préférable qu’une théorie interdise l’énoncé $\N \in 2$.
Entre deux théories opératoirement équivalentes, je préfère mettre de côté celle qui autorise un énoncé comme $sin\in exp$
Ah mais tu lis mal ce que j'ai écrit. Je ne nie pas pas du tout, et même respecte entièrement ça. Pour la énième fois, je te redis que tout à fait d'accord pour UNE théorie. Pas pour une théorie fondatrice, par contre.
Je te rappelle aussi pour la énième fois que je n'ai rien contre HoTT, les topos ou les catégories en tant qu'outils de recherche, éventuellement unificateurs***, mais que je cherche à détromper (et je m'agace d'être un peu seul au nom d'une tradition consistant à toujours dire du bien de tout dans notre petit monde scientifique) des gens qui seraient happés par les publicités (je le répète mensongères) affirmant le caractère fondateur de maths de ces travaux.
Dois-je encore répéter qu'on est sur de la recherche qui plus est en algèbre (on entend très peu de pub en provenance de l'analyse), c'est à dire en calcul récursif ne nécessitant que très peu d'axiomes (on recherche essentiellement à décider si certaines équations diophantiennes ont ou pas de solutions), que c'est un questionnement dit de niveau $0$ (ie ne parlant que des parties très simples de $\N$). Les calculs de groupes d'homotopie vivent essentiellement à ce niveau et il n'y a rien d'étonnant à ce qu'un effort de programmation les intègre.
Si tu souhaites échanger, il serait peut-être bon que tu précises un peu tes compétences en logique, car je ne sais pas à quelle "vitesse abréger et sous-entendre".
Il y a aussi quelque chose que je trouve suspect: je ne m'adresse plus forcément qu'à toi. Il y a une senteur mathématique constructive qui rend suspect l'objectivité (même une fois débarrassé de la pub) du projet. Une hégémonie qui voudrait que seule les maths du niveau $0$ (ie l'arithmétique) soit digne de crédit m’inquiéterait beaucoup.
Certes la compacité permet souvent de se ramener à du $\forall \exists$ sur $\N$, mais de très nombreux champs de recherches posent des questions totalement non constructives et même pas équivalentes à quoique ce soit qui vivent au niveau $0$. Par exemple, les probas (qui ne sont pas du tout un champ non appliqué) ne puisent que très peu de leurs résultats de fond au niveau $0$. Evidemment comme pour toute théorie non récursive, foys, par exemple, pourrait répondre "pas grave, on n'a qu'à demander à COQ si $ZF\vdash CeciCela$. Mefin si la conclusion est ce genre de pirouette, c'est idiot.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Remarque: je mets au défi de trouver sur google ou internet un doc de quelques pages qui décrit formellement, sans blabla et sans aucune ambiguité ni imprécision tout ça.
J'ai bcp navigué, bcp vérifié, pour l'heure je n'ai croisé que de la pub, du délayage partiel, des introductions qui se terminent avant de commencer. Même l'axiome d'univalence ($isomorphe\to egalite$) n'est nulle part, et pour lui-même énoncé de manière cash par quelqu'un.
Déjà, en soi, ce type de manque d'informations (alors que c'est censé exister depuis des années) semble attester de gène et de choses plus guidées par le désir que par l'aboutissement.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Comment ça ? C'est l'axiome 2.10.3 dans le livre. L'énoncé c'est : étant donnés deux types $A,B$, l'application $idtoequiv : (A=_U \to (A\simeq $ est une équivalence.
$A=_U B$ c'est le type égalité dont on a déjà parlé, "être une équivalence" est défini plus tôt dans le livre, et l'application $idtoequiv$ est définie dans le lemme 2.10.1, soit juste au-dessus. Il faut ne pas chercher loin pour décréter qu'il n'est énoncé nulle part...
J'ai trouvé une discussion https://mathematicswithoutapologies.wordpress.com/2015/05/13/univalent-foundations-no-comment/ assez semblable à la nôtre entre matheux chevronnés (dont Tao) qui semble confirmer mes craintes. Il y aurait bien une sorte de campagne d'UN DOMAINE pour imposer sa norme informatique. Bon, il est vrai que c'est aussi aux autres de développer leur produit, ils ne peuvent pas "trop" se plaindre de COQ s'ils ne proposent pas d'alternative.
Je suis très étonné que les gens n'utilisent pas caml, bien plus simple à mon goût (et un vérifieur de preuve s'y programme en un après-midi). Mais bon..
@max, je présume que tu parles du livre collaboratif qui fait 500 pages ? Tu l'as remis en lien récemment ou tu en parles de mémoire (je l'ai feuilleté il y a plusieurs mois, mais je ne sais plus trop où il est sur le forum). Et merci!!
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Globalement, je le redis, je parle cette fois de l'aspect "discipline d'utilisation d'un logiciel", COQ ne me parait pas acceptable (même si on peut y supposer ZFC de manière artificielle, comme on peut supposer ce qu'on veut dans ZFC), et mon avis semble partagé dans le lien. Trop de discipline (même si la boite de nuit offre une petite porte au fond pour aller au restau, ou faire un tennis) n'est pas bon. Un bon logiciel ne demande pas aux utilisateurs de typer, il type lui-même, et en plus, il ne doit pas refuser de typer quoique ce soit. L'idéal est bien entendu de ne rien typer, mais caml offre un bon compromis. Toute la science n'est pas obsédée par l'homotopie, ni par la forte consistance offert par le typage (qui ne dépasse pas le niveau Peano, même avec des types dépendants)
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
@max: détrompe-moi éventuellement (mais j'irai chercher "le livre" comme tu dis, mais je dois sortir). On est bien d'accord (je me fiche des types) qu'il dit tout et rien de plus que "isomorphe => égal"? (Il fait des quotients pour le dire non publicitairement). Parce que si je dois me tartiner la gène (pour mes yeux et ma dyscalculie) de sauter 3 kilos de typage pour lire l'essentiel, je vais galérer.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
De mon téléphone je vais voir Terminator suis fatigué et ai trop utilise mes lunettes donc tu peux prendre ton temps.
Cependant si tout ce pataquès est bien ce que je pense qu'il est il ne va pas vivre longtemps à cause d'un théorème très classique utilisant les grands cardinaux: tout modèle de ce paradigme sera forcément petit (et en utilisant mon axiome (appelé axiome de Hamkin)) on aura même que tout modèle de ce paradigme est dénombra :-D
J'espère donc bien ne rien avoir loupé (car je n'ai pu récupérer que des infos impressionnistes). Ça apprendra aux gens à crier trop vite victoire :-D
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Oui, je parle de ce livre, tu peux le trouver en pdf ici (à ma surprise, même en "vrai" il coûte relativement peu cher pour un livre de maths... )
Il dit un peu plus que ça, mais une de ses conséquences est que isomorphe implique égal.
Si tu comprends un peu l'homotopie, il dit qu'une certaine application entre deux espaces est une équivalence d'homotopie, où un de ces espaces est l'espace dont les points sont les preuves que $A=B$, et l'autre est l'espace des isos $A\to B$ (donc l'espace des preuves que $A$ est isomorphe à $B$); cette application étant évidemment celle qui à une preuve que $A=B$ associe la preuve naturelle que $A$ est isomorphe à $B$.
Et je me répète : Shulman a prouvé que ça a un modèle dans tout $(\infty,1)$-topos, donc dans des trucs a priori pas dénombrables (sauf si tu dis que tout univers est contenu dans un univers qui le croit dénombrable, mais dans ce cas...)
De mon téléphone. Merci. Non mais pour dénombrable bien entendu y a des conditions de propreté (absence d'indidcernables méchants), mais évidemment pas juste Loweinhem Skolemm non plus :-D
Un truc du genre "il n'y a qu'un nombre dénombrable d'importants dont tous led autres sont de simples puissances par exemple enfi. Je me comprends mais de toute façon j'attends d'avoir vu les détails techniques avant de me prononcer. Je préférerais avoir tort. Sinon ça montrerait trop à quel point chaque spécialité vit dans sa bulle
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
@max: je sors du ciné je recommande évidemment Terminator :-D (belle série au fond, assez mythique je trouve), et on sait prouver un phénomène similaire pour les graphes orientés. Je serais étonné que les catégories échappent à ça (une catégorie est juste un ensemble doté d'une loi associative (et où fait jouer à 0 un rôle "unfefined")). Je regarderai de plus près. Je crois que ce paradigme, qui en gros fait vivre la non duplication d'hypothèse sans le dire comme ça au niveau de l'appartenance et de l'égalité qui je crois provenait initialement de Martin Loef a pris "un gros risque" en ajoutant l'univalence. Mais bon je me trompe peut être.
En gros on n'a rien dans rien. Si des gens sont contents et "le désirent" (sans compter d'éventuels aigris ça c'est toujours possible) et vu la "conservation de l'énergie" en maths et ce en grande partie parce qu'on a ajouté cet axiome (et non évidemment à cause des types qui existent depuis même avant ZF) qui semblent identifier un peu magiquement les choses voulues telles alors il est fort probable qu'on soit face à une opération un peu similaire métaphoriquement parlant à l'ajout de V=L (exemple).
Il existe de nombreux arguments via grands cardinaux qui DÉMONTRENT qu'il ne peut pas exister de bonnes théories identifiant ce qui est isomorphe. Même l’extensionnalité en contexte mal fondé pose un problème de "magie itérée" et ce n'est que l'isomorphisme de graphes simples.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Une chtite info positive pour les visiteurs silencieux (vue ma fréquence de posts dans ce fil aujourd'hui, je me sens coupable d'avoir 20 ip/post).
Comme manifestement j'imagine qu'il y a des tonnes de lecteurs qui doivent se dire "pfff, cc sucre les fraises mais dans le mauvais sens, il est trop gentil, y a pas besoin d'ensembles pour voir qu'il y a plein d'objets isomorphes et pourtant différents et dès le CE2", je me permets de préciser en non expert de catégories que deux objets (dans une catégorie) entre lesquels il existe au moins une flèche qui est un isomorphisme (googlez j'ai la flemme) sont INDISCERNABLES dans ladite catégorie, ie, aucune propriété écrite avec des forall , connecteurs et les adjectifs catégoriques ne les distingue.
C'est bien entendu dans ce contexte que le paradigme prétend s'épanouir. Sinon, evidemment il contredirait même les premiers axiomes du CE2.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Salut cc, j'essaye de comprendre un peu ta conception des mathématiques. On claironne habituellement le slogan : Dans ZFC, tout est ensemble. On veut dire par là que tous les objets d'un modèle de ZFC sont du même "type" que l'on appelle ensemble, contrairement à NBG par exemple, où l'on distingue deux types, ensembles et classes, ou contrairement à une théorie où l'on considère des ensembles et des urelements qui ne satisfont pas nécessairement l'extensionnalité. Dans ZFC, on peut considérer qu'il y a aussi des classes, mais ce ne sont pas des objets du modèle, mais les relations à une variable libre, qui correspondent dans certains cas à des ensembles (i.e. l'ensemble des x tels que, etc), autrement dit des assemblages de signes qui appartiennent au langage formalisé.
Et toi tu dis : Tout est ensemble. Autrement dit, tu te places d'emblée dans un univers d'objets mathématiques (que tu ne définis pas, mais que tu caractérises vaguement par "objets égaux à leur illusion". Cet univers contient tout, aussi bien les modèles de ZFC, que les assemblages de signes et autres propositions que l'on veut bien définir, valeurs de vérité, etc. qui nous conviennent, et l'on peut appeler tous ces objets ensembles si on le désire. Et noter a $\in$ b ou b a ou encore b(a) dans le langage que l'on aura choisi (constitué aussi d'ensembles).
Avant d'aller plus loin et de m'égarer, j'attends ta confirmation que c'est à peu près ça.
Oui, mais c'est beaucoup plus simple en fait. Peu importe que ça s'appelle "ensemble" ou autrement. Je réagis dans ce genre de fil AVANT TOUT pour souffler sur des bulle de savon, des chimères et des esbrouffe. Et c'est dans ce cadre que je choisis mes mots.
Je ne parle pas de ZFC, et pour moi, ça n'a pas de sens de dire "dans ZFC, tout est ensemble". ZFC est un ensemble d'axiome, donc dans ZFC, il y a des ... axiomes.
Je parle bien en amont de ça, à savoir des fondements DE LA SCIENCE. Je rappelle que "Science = maths + hypothèses sur le monde réel". Donc il n'y a d'emblée pas à distinguer entre maths et science quand on parle de fondement.
Ensuite, il s'agit de regarder les choses comme elles sont, et de comprendre quel rôle ZFC joue là dedans, donc je précise un peu son rôle, car, une fois de plus, je rappelle que quand des militants prétendent "détrôner" ZF et le remplacer par je ne sais quelle usine à gaz absconse que presque personne ne comprend, avant de dire un truc faux, ils font bien pire, ils déclarent la guerre à des moulins à vent.
Que se passe-t-il donc, entrez ZFC et les fondements scientifiques. Bin la réponse est presque très simple:
1/ En maths il n'y a pas d'implicites (plus précisément les implicites sont des fautes, même s'il y en a)
2/ Les matheux font ce qu'ils veulent et ne se placent pas dans un système plutôt qu'un autre. Il écrivent des preuves avec des "donc" et des références "far" (métaphore: pointeur far). POINT BARRE;
3/ il est donc complètement stéril et contre-productif de prétendre avec une arrogance inouie les "dresser" pour qu'ils écrivent tout dans un système précis que Machin ou Truc aurait passé 2 ans de sa vie à programmer et dans lequel, sauf à coder de façon interminable, on ne peut à peu près rien faire sauf à recevoir une grosse formation orientante et stérilisante.
4/ Dans ce contexte, ce qui est important n'est pas la théorie dans laquelle on travaille mais le recensement des axiomes (aussi appelés admis, hypothèses, etc) de leur preuve. Par tel dans tel article de probas, tu recenses les admis (les composants non justifiés), tu regardes si ça vaut le coup d'en avoir déduit la conclusion X et c'est tout. Evidemment, si l'auteur de l'article a bien fait les choses, il a DEJA par lui-même recensé ce qu'il admet quelque part dans le texte et il n'y a pas grand chose à faire. D'autres fois, faut que ce soit les lecteur ou le referee qui dise (attention, tu as aussi admis ci, ça et ça)
5/ Quel est le rôle de ZF là dedans. Bin c'est très simple. Sans rien faire (ni codage ni traduction autre que mot à mot), les matheux (et sans s'en rendre compte) ont déjà admis uniquement des choses qui sont ou bien des hypothèses explicites ou bien des hypothèses-axiomes pointant vers des références où c'est prétendu déjà prouvé (mais localement au texte, c'est hypothésé) et enfin ... des axiomes de ZF(C). Autrement dit, il SE TROUVE SCIENTIFICO-MATHEMATIQUO-sociologiquement que les matheux "ne parviennent même pas" à écrire des preuves dont les admis NE SONT PAS DANS ZFC.
6/ Et ce n'est pas parce qu'ils ont été dressés à utiliser ZF, c'est juste qu'être matheux, c'est taffer avec des hypothèses concernant des petites collections. Mais il y a une chose qu'il faut bien comprendre: ce ne sont que des hypothèses.
7/ ZF n'est pas un fondement de la science. C'est juste un FAIT INEVITE et probablement inévitable que quand un scientifique décide de ne pas prouver un truc, c'est parce qu'il estime (sans le savoir) que c'est "évident" et IL SE TROUVE qu'il n'existe pas de matheux sur Terre, pour l'instant (et d'ailleurs pas non plus de scientifique) qui considère comme évident des énoncés qui ne sont pas dans ZFC. (Et de très loin, la plupart ne parviennent même pas à sortir de Z(C))
8/ Voilà, c'est tout. Je ne suis pas idéologue, je ne fais que le constat très simple que le fondement en amont de la science est parfaitement connu et inamovible depuis la nuit des temps (au langage près, qui lui peut évoluer) et il s'énonce ainsi:
8.1/ Tout doit apparaitre, pas "d'argument caché", pas "d'axiomes implicites".
8.2/ Quand les théorèmes sont archivés à l'académie des sciences mondiales, les axiomes écrits en blanc sur blanc doivent être facilement et AUTOMATIQUEMENT IDENTIFIABLES (recensables plutôt), aurtement dit, la preuve est archivée avec le théorème. (Bon même s'il y a par ci et parlà des fascicules de résultats)
9/ Maintenant tu veux probablement une explication de pourquoi "ensemble". En fait, comme je le dis souvent, ce n'est rien d'autre, là aussi qu'un constat. Il serait d'ailleurs plus exact de parler de fonctions plutôt que d'ensembles (et même plutôt d'applications). La raison est parfaitement simple: le langage est composé de mots (que l'on peut considérer comme "des lettres") séparés par des ESPACES. Et tout est fonction. Autrement dit:
<<Mot1 Mot2>>
se traduit juste en Mot1(Mot2). De même que :
<<Mot1 Mot2 Mot3>>
se traduit juste en (Mot1(Mot2))(Mot3)
Je ne te fais perdre de temps avec les trivialités consistant à gérer les parenthèses, c'est une autre affaire (ce sont des raccourcis)
Là aussi, ce n'est pas une opinion, c'est un constat factuel langagier bête et méchant.
Bien des gens voudraient pérenniser qu'un verbe n'est pas un sujet et que par exemple Medor mange est une phrase où on identifie bien le verbe. Hélas, il est IMMEDIAT que tu seras embêté avec la phrase Manger détruit qui a un sens parfaitement habituel dans la vie courante.
Ca se respecte, mais ce n'est pas du tout important.
Si tu te demandes pourquoi "ensemble" et non pas "fonction", c'est juste parce que PAR CONVENTION, les gens considèrent qu'un texte doit contenir des phrases. Par exemple, il n'est pas agréable de lire 3+4. On préfère lire 3+4=8.
C'est pourquoi au lieu de noter $\{x\mid x+5\}$, on préfère écrire $x\mapsto x+5$, mais que par contre, au lieu de noter $x\mapsto (x+5 = x^2)$, on préfère noter $\{x\mid x+5=x^2\}$. Mais ceci n'est qu'une différence poétique liée à ce qu'on veut que l'assemblage qui ne nécessite pas un environnement immédiat complétant est la phrase.
Ce FAIT langagier c'est lui ET LUI SEUL qui fait que tout est ensemble. Dans cette histoire, ZF n'a fait qu'obéir aux gens à la suite de la crise des fondements, mais il n'est en rien un cadre qui s'impose, il est juste un cadre que les gens MALGRE EUX ont décidé de ne pas dépasser. Mais j'insiste bien que "ne pas dépasser" ne veut pas dire "pousser au max de sa puissance". Ceux qui le poussent au max, ce sont les théoriciens des ensembles professionnels.
Il est donc complètement débile, puisqu'on taffe, qu'on le veuille ou non dans ZF (et même un petit fragment) de dire qu'on a trouvé telle et telle usine à gaz qui en sort. Ce n'est pas tout simplement honnête et c'est inventer un moulin à vent contre qui crier victoire. Et ça désinforme bêtement les néophytes.
Maintenant, comme je l'ai souvent fait, et tu peux relire ma réponse à xax, je rappelle que nous taffons dans une théorie CONTRADICTOIRE et non pas dans ZF. On a simplement tendance à l'oublier parce comme je l'ai dit ci-dessus, les gens "n'éprouvent pas le besoin" d'étudier les grosses collections, mais elles sont là point barre.
Il se trouve juste que c'est LA LOGIQUE qui est elle-même IMPACTEE. Et c'est "tant mieux". La physique nous a confronté depuis 150ans à des phrases égales à leur négation, mais les matheux font hypocritement comme s'ils n'étaient pas au courant. La science s'applique. Les preuves servent de garanties par l'entremise d'interventions humaines matérielles fragiles. Nos axiomes logiques rejettent la charge de l'affectation de valeurs se trouvant dans $\{vrai; faux\}$ sur l'être humain habillé en bleu de travail qui va soulever des cailloux et déplacer des parping, ou couper des fils de nylon avec un cutter.
Rien dans les formalismes que nous utilisons ne vient discerner cette interface d'une interface divine infaillible. Il n'est pas donc pas du tout étonnant que $0\neq1$ puisse être ébranlé par de gros cardinaux et que $e:= \{x\mid x\notin x\}$ soit tel que son poids situe la phrase $e\in e$ au milieu de l'intervalle $[vrai; faux]$
Parmi les gens qui ont décidé d'étudier les grosses collections (qui font vaciller la solidité du vide logique, car valent $1/0$ et non pas juste $\infty$) à ma connaissance le seul "honnête homme" est Quine avec NF. Lui au moins n'a rien rejeté et juste proposé une autre partie, qu'il a parié fructueuse de l'unique et inamovible théorie contraidctoire (en logique classique) fondatrice qu'est : $\forall R\exists a \forall x: ((x\in a)\iff (x\in R))$
Remarque HS: NBG n'a qu'une seule sorte d'objets, simplement les gros sont définis par
$$x\mapsto (\forall y: x\notin y)$$
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Je vais directement au point que je comprends le moins : comment peux-tu dire que nous travaillons dans une théorie contradictoire, et non pas dans ZF ? Ca me dépasse.
C'est très simple: quand tu travailles dans T, n'importe quel badaud de passage peut dire que tu travailles dans T', dès lors que $T'\supset T$. :-D
Plus sérieusement, contrairement à ce qu'affirment les gens qui n'y connaissent manifestement pas grand chose en fondements, dont la TOTALITE des auteurs du livre collaboratif HoTT (dont je viens de lire l'introduction et qui n'est qu'à peine moins erronées que les introductions des profs de CPGE lambda en logique en année 1) , ZF n'est pas un "fondement".
Un théorème prouvé dans ZF, comme un théorème prouvé dans la théorie TX comme un théorème prouvé dans HoTT, etc, c'est un énoncé de la forme A=>B où A est une conjonction des axiomes utilisés par la théorie (ZF,TX,HoTT, TrucMuche).
Les matheux ne s'amusent pas à dire à chaque instant "sachez msieurs-dames qu'il existe $x$ tel que $\forall y: (y\in x\iff R(y)),$ et que je vais prendre un tel $x$ que je vais nommer $a$, et donc dorénavant blabla a blabla"
Ils écrivent tous "with $a:=\{x\mid R(x)\}$ blabla a blabla"
Et la plupart du temps d'ailleurs*** écrivent "with $b:=\{x\in c\mid R(x)\}$ blabla b blabla" ce qui les situe immédiatement dans $Z$ plutôt que $ZF$ (je rappelle $Z\subset ZF$)
MAIS: ce n'est pas ZF qui les guide (à la rigueur on pourrait "mieux tricher" en disant que c'est $Z$ qui les guide, mais bon), c'est eux tout seuls qui "pensent".
Tu n'as peut-être pas lu le début du fil où je rappelle que de toute façon, on a en amont de tout le reste l'égalité "en dur" définitionnelle dans toute la science:
qui se moque comme d'une guigne que les gens ne vont utiliser ça qu'avec des expressions "gentilles". Il faut bien comprendre que c'est une égalité en dur AVANT la logique. (Pour te représenter la structure, tu quotientes par la relation (elle s'appelle beta-équivalence)). Par exemple, HoTT est une triste tentative usine à gaz de mettre un système de typage bien connu et complexe pour brider violemment, ZF n'est pas vraiment "une tentative", mais plutôt un constat que les gens ne sont jamais tentés (ou pas souvent) d'utiliser de grosses collections, mais tout ça, c'est dérisoire. On fait tous la même chose et les pros taffent essentiellement, au plus haut dans $P(\R)$.
En espérant t'avoir éclairé. J'ajoute une chose. Comme il a été démontré (je retrouverai les références du théorème), la partie utilisée par HoTT est triviale, ie les maths subtiles se situent au niveau non normalisable (ce qui est en fait évident, d'ailleurs, pas tellement besoin de preuves "complexes" puisque le normalisable est la zone des programmes qui terminent, donc sont inutilisables**). Ca représente pas loin de 40ans de retard sur les développement sérieux et pertinents en CCH. Autrement dit, en allant chercher des alliés pour leur pub, et en programmant COQ, ce petit groupe a complètement oublié de taffer. Ils réussissent l'exploit de mettre ensemble deux trivialisations stérilisantes:
1/ programmes qui terminent (donc de peu d'intérêt fondateur)
2/ Non intégration de la découverte de Timothy Griffith qui intègre le RPA dans la CCH.
à quoi il faut ajouter
3/ une hyper-extensionalité (l'univalence) qui est très exactement le "mauvais sens" pour comprendre le fond des choses (là aussi des théorèmes robustes l'établissent, ce n'est pas une opinion)
4/ et un logiciel difficile d'emploi pour le tout venant.
** par essence "fondation" = "OS" = "programmes qui bouclent". Le jour où tu es en train de taper un article t'es vachetement content si unix ou windows décide de terminer :-D :-D
*** je rappelle que $\{x\in a\mid P\}$ est une abréviation de $\{x\mid x\in a$ et $P\}$ (contrairement là aussi à des usages, mal compris, cherchant des distinctiions là où il n'y en pas)
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Mais on ne peut utiliser l'expression {x | R(x)} qu'après avoir démontré (ou s'être assuré) que R(x) est collectivisante, non ? (ou alors comme nom commode de la classe propre, avec lequel on ne peut écrire que quelques opérations ensembliste)
Je vais ouvrir un fil et te faire une formation accélérée aux vraies de chez vraies fondements :-D "on n'a le droit de" n'a pas cours en science :-D (la science c'est pas la Corée du nord)
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Non, car ce qui compte c'est ce que tu prouves. Si tu prouves que $a\in \emptyset$ implique $RH$, tu ne seras pas publié. Mais c'est tout.
De même si tu prouves le théorème de Brouwer comme suit:
1/ je prends $a:= (x\mapsto f(x(x)))$
2/ Je calcule $f(a(a))$ et vous remarquez que c'est $a(a)$.
3/ J'ai mon point fixe $p:=a(a)$ pour $f$.
Mais qu'est-ce que tu auras alors fait? Et bien c'est simple, tu auras utilisé un outil (EXISTANT BEL ET BIEN) qui est "trop fort"
Quand l'usine te répondra pour acheter ou pas ton produit et l'exécuter, elle ne t'enverra pas de chèque, mais "Cher, Monsieur, nous vous remercions, mais nous n'avons hélas pas les moyen de nous fournir en $x\mapsto x(x)$. aussi votre produit partiel ne nous sera d'aucune utilité, car aucun de nos sous-traitant ne dispose de la pièce dont vous déclarez qu'il faut la mettre à droite de $\circ$.
Ce qui compte ce sont les preuves. Si tu n'utilises pas un axiome dans ta preuve, personne ne te dira que sous prétexte qu'il fait partie d'une théorie dont il est membre et qu'on rejette cette théorie, on rejette ta preuve.
Sinon, la plupart des articles seraient retoqués au nom du fait qu'on ne sait pas si ZF est consistant ou pas.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Mais ça tu ne le sais qu'après. Ou plus précisément TOUT théorème exhibe SA théorie contradictoire (ses hypothèses +la négation de sa conclusion). L'intérêt c'est la preuve.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
D'accord, mais tu as l'air de dire qu'utiliser l'expression {x|x=x} est possible et ne pose pas de problème. Mais dès que j'écris "soit a = {x|x=x}", c'est fini, mon argument n'a plus aucun intérêt, et ça, je le sais immédiatement.
Je ne comprends pas ta question. Si tu déclares $a := \{x\mid x=x\}$, il n'y a pas de problème, tu as juste créé une abréviation et tu as $\forall x: ([x\in a]=[x=x])$.
Si tu écris une preuve en utilisant ces "gros" ensembles là, mais tous propres, tu fais une démonstration dans NF (le système de Quine). C'est tout.
Si tu mélanges et obtiens une contradiction avec par exemple 4 ensembles autorisés par ZF et 5 ensembles autorisés par NF et bien ça va juste dépendre de l'intérêt de ta preuve, rien n'indique a priori qu'elle sera inintéressante.
Comme le rappelait Martial récemment, en 2014 (il a mis l'article en lien) il a été prouvé que NF est consistante (moyennant la consistance de ZF + peut-être quelques modérés gds cardinaux, je n'ai pas encore lu).
De toute façon, là, on sort du sujet. Ce que je dis est juste que ce sont les preuves et non pas les théories qui comptent. Par exemple je sais prouver sans dupliquer les hypothèses que $\forall a:[(\forall x: ((x\in a) =x\ontin x)) \to (0=1)]$. Et bien la preuve est très nettement plus longue que l'habituel argument diagonal. Essaie de le faire en exercice tu verras, ce n'est pas si facile et pourtant tu es fort.
D'une manière générale, il n'est jamais bon "d'interdire", comme l'a fait par exemple 708 (mais aussi bien d'autres gens!!!) en disant "je n'ai pas le droit d'écrire que". En effet, n'importe qui prouve immédiatement, mais surtout plus gravement LUI-MEME, prouve que c'est faux, puisqu'il l'écrit en disant qu'il n'a pas le droit de l'écrire.
Je me répète: le fondement de la science ce n'est pas une théorie, c'est le logiciel de recensement de ce qui est utilisé, qui lui doit être correct et surtout chiadé.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
2/ Non intégration de la découverte de Timothy Griffith qui intègre le RPA dans la CCH.
En fait on peut "déléguer" ce genre de tâche (et produire des programmes de type $[\forall p,q:énoncés, ((p\to q) \to p ) \to p ]\to E$) où $E$ est l'énoncé cible) donc est-ce si gênant?
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
C'est quoi, ces fameuses phrases égales à leur négation ?
Il n'y en a pas(*), c'est christophe c qui fait du militantisme (pour qu'on l'aide à démontrer que ZF est contradictoire ?) B-)
Il existe certes des programmes $T$ qui affichent après exécution, "le texte affiché par $T$ affirme quelque chose de faux" (**)mais leur assimilation à leur production (voire à un énoncé mathématique en bonne et due forme) est un abus de langage (un lambda terme n'est pas "égal en dur" à ses réductions).
[size=x-small](*) $\neg A$ contient au moins un symbole de plus que $A$, à savoir "$\neg$".[/size]
[size=x-small](**) @christophe c: plutôt que des phrases plus authentiquement gödéliennes ("F(100110110) =>X" où 100110110 est l'encodage de la phrase entre guillemets), c'est toujours ce type d'exemple qui apparaît dans tes textes de promotion de l'inconsistance de ZF[/size]
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
@Foys : il y a tout de même une grosse différence entre exécuter une preuve ou le RPA est juste mis en hypothèse et une preuve où il est réalisé. Même si la preuve elle même ne change pas c'est un peu dommage de mettre en hypo ce qu'on sait réaliser (et c'est trompeur).
@GA : en TQ je suppose que c'est évident pour toi et en TDE exemple : (edans e) où e est l'ensemble des X tels que x pas dans x.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Je rappelle que contrairement à un préjugé la CCH gère toute la logique (y compris classique donc) et que un oubli initial idiot autrement un simple accident à fait qu'on a d'abord développé la réalisation intuitionniste. Mais c'est complètement contingent. C'edt juste dû à une habitude de présenter les procédures informatiques avec une seule sortie car "fonctions". Mais c'est accidentel. Une procédure prend des var read et des var write autant qu'elle veut et elle écrite dans les write. Le coup du "return toto" (avec l'adresse de à qui on retourne non précisée dans les langages évolués) est juste contingent.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
@Foys: je n'ai JAMAIS promu l'inconsistance de ZF, je cherche à la prouver ça n'a rien à voir (et je n'ai pas réussi comme tu sais :-D ).
Je ne crois pas que ma vision des fondements en soit influencée, pour la bonne et simple raison que je promeux comme tu dis les théories inconsistantes. Ce serait fort de café de m'attribuer l'idée saugrenue que je cherche à casser ZF pour mieux l'aimer au titre que j'aimerais que les contradictoires :-D
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Mon problème est pourtant simple : si je me base sur ton abréviation qui me semble imprudente et que j'écris l'innocente proposition
$ \{x\mid x=x\}$ = $\{x\mid x=x\}$
je me retrouve à dire tout et son contraire !
Toto = Toto (axiome égalité)
$\forall$x (x $\in$ Toto $\Leftrightarrow$ x = x) (abréviation cc)
$\exists$x$\forall$y (y $\in$ x $\Leftrightarrow$ (y $\notin$ y et y $\in$ Toto)) (schéma compréhension)
$\forall$y (y $\in$ a $\Leftrightarrow$ (y $\notin$ y et y $\in$ Toto)) (règle introduction constante)
$\forall$y (y $\in$ a $\Leftrightarrow$ y $\notin$ y)
a $\in$ a $\Leftrightarrow$ a $\notin$ a
Je dis tout ...
... et son contraire !
@GG : Ben j'ai envie de dire que tu as démontré que si $\exists x\forall y (y\in x \Leftrightarrow y \not \in y \ et \ y =y)$ alors $faux$. C'est un résultat connu, et on ne va pas le publier dans Annals of the Great Forum mais bon :-D !
@GA : en TQ je suppose que c'est évident pour toi et en TDE exemple : (edans e) où e est l'ensemble des X tels que x pas dans x.
Je suis intéressé par des phrases égales à leur négation en TQ et des phrases égales à leur négation en maths. Pour les maths, OK. Est-ce qu'il faut comprendre que tu veux dire les choses suivantes (j'essaie de résumer mais je ne dis pas que je suis d'accord) :
1) Il n'y a aucun problème moral à utiliser le schéma de compréhension non restreint, c'est juste qu'il est connu qu'avec ça on démontre facilement le faux.
2) En fait, notre langage, ontologiquement et intrinsèquement, nous oblige à considérer que tout est ensemble (et que tout est fonction) et le schéma de compréhension non restreint est naturel dans notre langage. C'est en ça que nous travaillons toutes et tous dans une théorie contradictoire. En mode slogan : "langage = théorie des ensembles avec schéma de compréhension non restreint" où on entend que l'égalité est au sens "non opératoirement différent" (i.e. on ne peut pas distinguer la pratique de ces deux choses).
3) $ZF(C)$ est un des seuls (ou est le meilleur ?) ensembles de règles de conduite que l'humanité a trouvé pour éviter de démontrer trop de choses fausses et ça marche... pour l'instant.
Mais, si tout cela est vrai, rien ni personne ne fonde rien, n'est-ce pas ? Pas plus $ZF$ que $NF$ ou que $HoTT$ ?
Bon et pour la TQ, ben je veux bien voir aussi. Je suis d'accord avec ce qu'a dit Foys dans un autre fil : en TQ, une phrase est un sous-espace (fermé) d'un Hilbert, sa négation est son orthogonal, et donc il ne peut y avoir égalité que si le Hilbert est nul. C'est un peu comme "le vide est égal à son complémentaire dans l'ensemble vide". Et alors ?
Merci Georges, voilà une récapitulation à laquelle c'est un plaisir de répondre.
Je trouve que tes points 1 et 2 résument plutôt bien ma position, même si comme tu t'en doutes, il y aurait à préciser pas mal de choses surtout à l'adresse de gens "à l'ancienne" qui pourraient mal comprendre les choses TELLES QUELLES.
Je n'approuve en revanche pas du tout le point 3. Je ne crois pas que l'humanité "ait trouvé ZF" pour ensuite s'y plier. L'humanité (comme tu dis) a juste CONSTATE que personne n'a jamais ADMIS comme axiome AUTRE CHOSE qu'un tout petit fragment de ZF(C). Une chtite psychanalyse vite faite de Zermelo et Frankael a ensuite suffi à mettre de l'encre sur du papier pour dire "ok, bin msieurs-dames, ne vous fatiguez plus à écrire que vous admettez ceci et cela, on l'a fait pour vous, ce sera réputé admis dans chacun de vos articles".
La question ensuite de savoir si on y prouve des choses "vraies" n'a pas vraiment de sens, car on y prouve des choses à propos du monde des objets mathématiques où la vérité est triviale, mais ça ne garantit rien sur le monde réel qui n'est pas égal à son illusion (à ses apparences si tu préfères). De plus, je ne crois pas un instant qu'il y ait en profondeur qui que ce soit qui considère autrement un théorème $P$ de ZF, que comme un théorème absolu disant $ZF\to P$. Certes, il y a des inconditionnels, mais bon, ils sont très minoritaires.
De même pour n'importe quelle autre théorie. Comme il n'y a pas d'entiers, de mots, de phrases, etc, bref rien de mathématique en dehors des modèles de ZF (pour l'heure), de même que comme il n'y a pas d'algorithme non calculable (pour l'heure aussi : thèse de Church), en particulier, comme il n'y a pas de modèles qui habite en dehors de tout modèle de ZF, évidemment que les gens ont une certaine à penser que si $ZF\to P$ alors $P$ est vrai, mais c'est au nom d'une conviction extrêmement précise qui est que les choses dont parle $P$ sont toutes dans la réunion des $M$ quand $M$ parcourt les modèles de ZF. Je ne dirais donc pas que c'est un "faute de mieux", mais une réelle "conviction factuelle" des gens. Même s'ils n'en sont pas conscients (hélas, ce qui provoque parfois des malentendus)
Oui, j'avais vu que Foys faisait remarquer qu'un état quantique PUR est un sev d'un Hilbert. On est bien d'accord. Mais les morceaux d'objets étendus spatialement ne sont pas dans des état purs, ils sont gérés actuellement (et ontologiquement mal) avec le même formalisme que les mélanges statistiques classiques d'états purs (et souvent, à tort, considérés comme saisis par leur matrice densité (celle du groupe statistique entier). Un superposition CLASSIQUE (ie $a+non(a)$) est une phrase égale à sa négation:
Alors attention, c'est un peu subtil car le $+$ ici n'est ni le $ou$ classique de l'ignorance ni le $+$ quantique. Mais ce n'est pas grave, je pense que tu comprends. La cohabitation subtile entre les différents opérateurs binaires émergeant de la TQ n'est pas du tout finie d'être étudiée et pose de gros problèmes de statut (la téléportation quantique en donne un des meilleurs exemples, en montrant que le $ou$ classique lui-même est indiscernables, dans certaines contextes du "et" quantique)
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
@Georges Abitbol, excuse-moi, mais tu dis que j'ai démontré Si .... alors faux. Où vois-tu le "si" ? J'ai démontré "faux" en n'utilisant que des axiomes et l'abréviation de cc.
Oui, j'avais vu que Foys faisait remarquer qu'un état quantique PUR est un sev d'un Hilbert.
Euh, si Foys disait ça, je ne serais pas d'accord. Pour moi (et j'espère ne pas me tromper), l'ensemble des phrases est un sous-treillis ($\sigma$-complet orthocomplémenté) du treillis des sous-espaces fermés d'un Hilbert, et on appelle état une application de $\{phrases\}$ vers $[0,1]$ qui vérifie les mêmes axiomes que "mesure de probabilité" dans la théorie de l'intégration. Maintenant, le théorème de Gleason affirme que tout état est égal à $F \mapsto Tr(AP_F)$ où, pour tout sous-espace fermé $F$, $P_F$ est le projecteur orthogonal dessus et où $A$ un opérateur positif de trace $1$. Un état est dit pur si $A$ est le projecteur orthogonal sur une droite vectorielle (un tel opérateur est positif, de trace $1$). Alors, quand tu affirmes citer Foys comme ci-dessus, ou que tu dis
les morceaux d'objets étendus spatialement ne sont pas dans des état purs [...] sont [...] souvent, à tort, considérés comme saisis par leur matrice densité
ben j'ai envie de dire que soit je ne suis pas d'accord du tout (au vu de ce que j'ai écrit ci-dessus) ou alors je ne comprends pas ce que tu veux dire.
Je sais absolument pas ce que veut dire ton $+$ (qui ne serait pas le "+ quantique" - je ne sais pas ce que c'est non plus). Si je prends deux phrases (deux sous-espaces) je peux prendre le sous-espace (adhérence de la) somme ; si je prends deux projecteurs orthogonaux, je peux prendre leur somme (mais ce n'est pas souvent un projecteur, et si l'un des deux espaces est l'orthogonal de l'autre, alors la somme des projecteurs est bien un projecteur car c'est... l'identité).
La cohabitation subtile entre les différents opérateurs binaires émergeant de la TQ n'est pas du tout finie d'être étudiée et pose de gros problèmes de statut (la téléportation quantique en donne un des meilleurs exemples, en montrant que le ou classique lui-même est indiscernables, dans certaines contextes du "et" quantique)
La téléportation quantique, c'est bien le fait de savoir transmettre exactement un état à condition de savoir transmettre quelques bits classiques ? Quel rapport avec la choucroute ?
Réponses
Ensuite pour les vidéos franchement t'exagères. Science4All fait de la vulgarisation, évidemment qu'il va pas t'apprendre grand chose si tu fais des maths...
Évidemment que remplacer le signe $\in$ par $:$ ne change rien. Le but de mon message était de souligner que $\mathbb{N}\in 2$ possède un sens en théorie des ensembles mais pas en théorie des types.
La réponse est contenue dans le post où je le dis justement. Collapse trop tendancieux quand on prétend FONDER. Une fois de plus, je rappelle que ma critique ne porte absolument pas sur le travail réalisé, en particulier, je ne mets aucunement en cause les progrès de la recherche en géométrie et topologie algébrique et je n'ai pas l'once d'un micro gramme de doute envers les qualités de Voedovski et compagnie.
Qu'on prouve des théorèmes de la forme (univalence => X) n'est absolument pas mon sujet ici. Parfois j'ai l'impression non pas de ne pas être compris, mais de ne pas être lu (ce qui ne serait pas scandaleux). Mais attention, si on répond à des trucs sortis de contexte, ça finit par tourner en rond.
Je le redis, ma prolixité provient de:
1/ L'amateurisme et la non-expertise d'un certain nombre de gens qui CROIENT et ESPERENT des merveilles, espérances qu'ils tirent des PUBLICITES (incontestables, je peux mettre d'autres videos, ou renvoyer un lien vers des articles "image des maths - CNRS"). Ces gens seront très déçus une fois (si ça arrive) initiés
2/ La pub mensongère (prétendre parler de fondements)
3/ L'impression (pas si involontaire) que donnent les experts en laissant croire à ces gens que ce n'est pas fait dans ZF (ils requalifie leur utilisation de ZF comme un ZF métamaths, et pensent ainsi "changer les affaires", mais les néophytes pensent eux REELLEMENT que ce n'est pas construit ensemblistement)
4/ La complication volontaire (500 pages), qui participe à la chimère.
En aucun cas, je ne critique l'actyivité mathématique en soi qui tourne autour de ça. (Revoir le lien que j'ai mis vers le gars de la Rochelle qui a fait un pdf humoristique "sympa" pour dénoncer (plus que gentiment) ces 4 phénomènes).
Je te fais dire EXACTEMENT ce que tu viens de dire toi-même, à savoir que $(\N\in 2)=NoSens$. Crois-tu que ça change quelque chose de dire qu'une suite de caractère n'a pas de sens, plutôt que de dire qu'une suite de caractères a la valeur $NoSens$?
Crois-tu que HoTT soit le premier système qui ne taffe pas dans $\{vrai; faux\}$?
Je t'ai compris, en tout cas, je le pense sincèrement, mais je pense que c'est toi qui m'attribue une difficulté à te comprendre. La logique valuée à 3 valeurs : vrai; faux; non sensé a des règles de fonctionnement parfaitement syntaxiques et récursives. Ce n'est pas parce que tu vas déclarer ça "métamaths" et que tu vas y changer quelque chose OPERATOIREMENT. En outre, ça fait longtemps qu'on a fait bien mieux et qu'on a structuré de façon réfléchie les valeurs que peuvent prendre les phrases, et en aucune façon, on s'est arrêté au rudimentaire ajout de $NoSens$.
Encore une fois, je pense qu'il est important d'insister sur l'importance de l'opératoire, surtout pour une théorie qui se permet de défendre une super-extensionalité éjectant les différences entre 2 relations non isomorphes, sous peine d'y voir une sacré incohérence cynique interne.
Encore une théorie de l'âme qui NIERAIT FORTEMENT toute forme d'extensionalité, je veux bien qu'elle pourrait se prévaloir d'associer un peu de culte aux mots isolés. Mais surement pas une théorie qui s'attache à identifier les structures isomorphes.
> Crois-tu que ça change quelque chose de dire qu'une suite de caractère n'a pas de sens,
> plutôt que de dire qu'une suite de caractères a la valeur $NoSens$ ?
Oui.
> Crois-tu que HoTT soit le premier système qui ne taffe pas dans $\{vrai; faux\}$ ?
Hors sujet : HoTT « taffe dans vrai-faux »
À un moment il faut être sérieux ce n'est pas en jouant sur les mots ou les expressions que tu vas changer quelque chose. Précisément, peux-tu me signaler un logiciel de calcul qui " ne sait pas quoi faire et fait exploser l'ordinateur et ftout un incendie à ton apart quand tu entres 3/0"?
J'ai l'impression que tu ne sais pas que les maths sont robustes. Il y a le récursivement enumerable et le reste. Personne n'a jamais écrit que l'ensemble des theoremeS de HoTT n'est pas récursivement enumerable jusqu'à present sur le forum. Si tu m'affirmes que c'est le cas on parlera technique. En attendant j'attends ta preuve.
Si HoTT taffe dans vrai faux (je pense que tu te trompes mais bon) il utilise la logique classique et à pas mal de retard compare aux topos et autres systèmes. Je suis donc étonné par ta réponse.
> Peux tu prouver QU'OPERATOIREMENT il y a une différence entre dire "N:2" n'a pas de sens et
> dire (N:2)=NoSens.
Même s’il n’y avait aucune différence opératoire (ce que je pense), pour moi il est préférable qu’une théorie interdise l’énoncé $\N\in 2$.
Entre deux théories opératoirement équivalentes, je préfère mettre de côté celle qui autorise un énoncé comme $\sin \in \exp$.
Dans une perspective de fondation des maths, c’est très important de se demander : veut-on qu’en maths l’énoncé $\N\in 2$ soit valide ?
> Si HoTT taffe dans vrai faux (je pense que tu te trompes mais bon) il utilise la logique classique
> et à pas mal de retard compare aux topos et autres systèmes. Je suis donc étonné par ta réponse.
Renseigne-toi mieux dans ce cas.
Je t'ai signalé un théorème. Pas une opinion. Apparemment, tu parles en néophyte (ou alors, je ne sais pas, montre que tu sais de quoi tu parles?)
Ah mais tu lis mal ce que j'ai écrit. Je ne nie pas pas du tout, et même respecte entièrement ça. Pour la énième fois, je te redis que tout à fait d'accord pour UNE théorie. Pas pour une théorie fondatrice, par contre.
Je te rappelle aussi pour la énième fois que je n'ai rien contre HoTT, les topos ou les catégories en tant qu'outils de recherche, éventuellement unificateurs***, mais que je cherche à détromper (et je m'agace d'être un peu seul au nom d'une tradition consistant à toujours dire du bien de tout dans notre petit monde scientifique) des gens qui seraient happés par les publicités (je le répète mensongères) affirmant le caractère fondateur de maths de ces travaux.
Dois-je encore répéter qu'on est sur de la recherche qui plus est en algèbre (on entend très peu de pub en provenance de l'analyse), c'est à dire en calcul récursif ne nécessitant que très peu d'axiomes (on recherche essentiellement à décider si certaines équations diophantiennes ont ou pas de solutions), que c'est un questionnement dit de niveau $0$ (ie ne parlant que des parties très simples de $\N$). Les calculs de groupes d'homotopie vivent essentiellement à ce niveau et il n'y a rien d'étonnant à ce qu'un effort de programmation les intègre.
Si tu souhaites échanger, il serait peut-être bon que tu précises un peu tes compétences en logique, car je ne sais pas à quelle "vitesse abréger et sous-entendre".
Il y a aussi quelque chose que je trouve suspect: je ne m'adresse plus forcément qu'à toi. Il y a une senteur mathématique constructive qui rend suspect l'objectivité (même une fois débarrassé de la pub) du projet. Une hégémonie qui voudrait que seule les maths du niveau $0$ (ie l'arithmétique) soit digne de crédit m’inquiéterait beaucoup.
Certes la compacité permet souvent de se ramener à du $\forall \exists$ sur $\N$, mais de très nombreux champs de recherches posent des questions totalement non constructives et même pas équivalentes à quoique ce soit qui vivent au niveau $0$. Par exemple, les probas (qui ne sont pas du tout un champ non appliqué) ne puisent que très peu de leurs résultats de fond au niveau $0$. Evidemment comme pour toute théorie non récursive, foys, par exemple, pourrait répondre "pas grave, on n'a qu'à demander à COQ si $ZF\vdash CeciCela$. Mefin si la conclusion est ce genre de pirouette, c'est idiot.
J'ai bcp navigué, bcp vérifié, pour l'heure je n'ai croisé que de la pub, du délayage partiel, des introductions qui se terminent avant de commencer. Même l'axiome d'univalence ($isomorphe\to egalite$) n'est nulle part, et pour lui-même énoncé de manière cash par quelqu'un.
Déjà, en soi, ce type de manque d'informations (alors que c'est censé exister depuis des années) semble attester de gène et de choses plus guidées par le désir que par l'aboutissement.
$A=_U B$ c'est le type égalité dont on a déjà parlé, "être une équivalence" est défini plus tôt dans le livre, et l'application $idtoequiv$ est définie dans le lemme 2.10.1, soit juste au-dessus. Il faut ne pas chercher loin pour décréter qu'il n'est énoncé nulle part...
Je suis très étonné que les gens n'utilisent pas caml, bien plus simple à mon goût (et un vérifieur de preuve s'y programme en un après-midi). Mais bon..
@max, je présume que tu parles du livre collaboratif qui fait 500 pages ? Tu l'as remis en lien récemment ou tu en parles de mémoire (je l'ai feuilleté il y a plusieurs mois, mais je ne sais plus trop où il est sur le forum). Et merci!!
Cependant si tout ce pataquès est bien ce que je pense qu'il est il ne va pas vivre longtemps à cause d'un théorème très classique utilisant les grands cardinaux: tout modèle de ce paradigme sera forcément petit (et en utilisant mon axiome (appelé axiome de Hamkin)) on aura même que tout modèle de ce paradigme est dénombra :-D
J'espère donc bien ne rien avoir loupé (car je n'ai pu récupérer que des infos impressionnistes). Ça apprendra aux gens à crier trop vite victoire :-D
Il dit un peu plus que ça, mais une de ses conséquences est que isomorphe implique égal.
Si tu comprends un peu l'homotopie, il dit qu'une certaine application entre deux espaces est une équivalence d'homotopie, où un de ces espaces est l'espace dont les points sont les preuves que $A=B$, et l'autre est l'espace des isos $A\to B$ (donc l'espace des preuves que $A$ est isomorphe à $B$); cette application étant évidemment celle qui à une preuve que $A=B$ associe la preuve naturelle que $A$ est isomorphe à $B$.
Et je me répète : Shulman a prouvé que ça a un modèle dans tout $(\infty,1)$-topos, donc dans des trucs a priori pas dénombrables (sauf si tu dis que tout univers est contenu dans un univers qui le croit dénombrable, mais dans ce cas...)
Un truc du genre "il n'y a qu'un nombre dénombrable d'importants dont tous led autres sont de simples puissances par exemple enfi. Je me comprends mais de toute façon j'attends d'avoir vu les détails techniques avant de me prononcer. Je préférerais avoir tort. Sinon ça montrerait trop à quel point chaque spécialité vit dans sa bulle
Après 25 ans d'abstinence j'ai du mal à réenclencher; j'ai d'abord pensé à m'aider d'un cocktail taurine-xanax mais je vais y arriver sans.
En gros on n'a rien dans rien. Si des gens sont contents et "le désirent" (sans compter d'éventuels aigris ça c'est toujours possible) et vu la "conservation de l'énergie" en maths et ce en grande partie parce qu'on a ajouté cet axiome (et non évidemment à cause des types qui existent depuis même avant ZF) qui semblent identifier un peu magiquement les choses voulues telles alors il est fort probable qu'on soit face à une opération un peu similaire métaphoriquement parlant à l'ajout de V=L (exemple).
Il existe de nombreux arguments via grands cardinaux qui DÉMONTRENT qu'il ne peut pas exister de bonnes théories identifiant ce qui est isomorphe. Même l’extensionnalité en contexte mal fondé pose un problème de "magie itérée" et ce n'est que l'isomorphisme de graphes simples.
[À ton service :-) AD]
Comme manifestement j'imagine qu'il y a des tonnes de lecteurs qui doivent se dire "pfff, cc sucre les fraises mais dans le mauvais sens, il est trop gentil, y a pas besoin d'ensembles pour voir qu'il y a plein d'objets isomorphes et pourtant différents et dès le CE2", je me permets de préciser en non expert de catégories que deux objets (dans une catégorie) entre lesquels il existe au moins une flèche qui est un isomorphisme (googlez j'ai la flemme) sont INDISCERNABLES dans ladite catégorie, ie, aucune propriété écrite avec des forall , connecteurs et les adjectifs catégoriques ne les distingue.
C'est bien entendu dans ce contexte que le paradigme prétend s'épanouir. Sinon, evidemment il contredirait même les premiers axiomes du CE2.
Et toi tu dis : Tout est ensemble. Autrement dit, tu te places d'emblée dans un univers d'objets mathématiques (que tu ne définis pas, mais que tu caractérises vaguement par "objets égaux à leur illusion". Cet univers contient tout, aussi bien les modèles de ZFC, que les assemblages de signes et autres propositions que l'on veut bien définir, valeurs de vérité, etc. qui nous conviennent, et l'on peut appeler tous ces objets ensembles si on le désire. Et noter a $\in$ b ou b a ou encore b(a) dans le langage que l'on aura choisi (constitué aussi d'ensembles).
Avant d'aller plus loin et de m'égarer, j'attends ta confirmation que c'est à peu près ça.
Je ne parle pas de ZFC, et pour moi, ça n'a pas de sens de dire "dans ZFC, tout est ensemble". ZFC est un ensemble d'axiome, donc dans ZFC, il y a des ... axiomes.
Je parle bien en amont de ça, à savoir des fondements DE LA SCIENCE. Je rappelle que "Science = maths + hypothèses sur le monde réel". Donc il n'y a d'emblée pas à distinguer entre maths et science quand on parle de fondement.
Ensuite, il s'agit de regarder les choses comme elles sont, et de comprendre quel rôle ZFC joue là dedans, donc je précise un peu son rôle, car, une fois de plus, je rappelle que quand des militants prétendent "détrôner" ZF et le remplacer par je ne sais quelle usine à gaz absconse que presque personne ne comprend, avant de dire un truc faux, ils font bien pire, ils déclarent la guerre à des moulins à vent.
Que se passe-t-il donc, entrez ZFC et les fondements scientifiques. Bin la réponse est presque très simple:
1/ En maths il n'y a pas d'implicites (plus précisément les implicites sont des fautes, même s'il y en a)
2/ Les matheux font ce qu'ils veulent et ne se placent pas dans un système plutôt qu'un autre. Il écrivent des preuves avec des "donc" et des références "far" (métaphore: pointeur far). POINT BARRE;
3/ il est donc complètement stéril et contre-productif de prétendre avec une arrogance inouie les "dresser" pour qu'ils écrivent tout dans un système précis que Machin ou Truc aurait passé 2 ans de sa vie à programmer et dans lequel, sauf à coder de façon interminable, on ne peut à peu près rien faire sauf à recevoir une grosse formation orientante et stérilisante.
4/ Dans ce contexte, ce qui est important n'est pas la théorie dans laquelle on travaille mais le recensement des axiomes (aussi appelés admis, hypothèses, etc) de leur preuve. Par tel dans tel article de probas, tu recenses les admis (les composants non justifiés), tu regardes si ça vaut le coup d'en avoir déduit la conclusion X et c'est tout. Evidemment, si l'auteur de l'article a bien fait les choses, il a DEJA par lui-même recensé ce qu'il admet quelque part dans le texte et il n'y a pas grand chose à faire. D'autres fois, faut que ce soit les lecteur ou le referee qui dise (attention, tu as aussi admis ci, ça et ça)
5/ Quel est le rôle de ZF là dedans. Bin c'est très simple. Sans rien faire (ni codage ni traduction autre que mot à mot), les matheux (et sans s'en rendre compte) ont déjà admis uniquement des choses qui sont ou bien des hypothèses explicites ou bien des hypothèses-axiomes pointant vers des références où c'est prétendu déjà prouvé (mais localement au texte, c'est hypothésé) et enfin ... des axiomes de ZF(C). Autrement dit, il SE TROUVE SCIENTIFICO-MATHEMATIQUO-sociologiquement que les matheux "ne parviennent même pas" à écrire des preuves dont les admis NE SONT PAS DANS ZFC.
6/ Et ce n'est pas parce qu'ils ont été dressés à utiliser ZF, c'est juste qu'être matheux, c'est taffer avec des hypothèses concernant des petites collections. Mais il y a une chose qu'il faut bien comprendre: ce ne sont que des hypothèses.
7/ ZF n'est pas un fondement de la science. C'est juste un FAIT INEVITE et probablement inévitable que quand un scientifique décide de ne pas prouver un truc, c'est parce qu'il estime (sans le savoir) que c'est "évident" et IL SE TROUVE qu'il n'existe pas de matheux sur Terre, pour l'instant (et d'ailleurs pas non plus de scientifique) qui considère comme évident des énoncés qui ne sont pas dans ZFC. (Et de très loin, la plupart ne parviennent même pas à sortir de Z(C))
8/ Voilà, c'est tout. Je ne suis pas idéologue, je ne fais que le constat très simple que le fondement en amont de la science est parfaitement connu et inamovible depuis la nuit des temps (au langage près, qui lui peut évoluer) et il s'énonce ainsi:
8.1/ Tout doit apparaitre, pas "d'argument caché", pas "d'axiomes implicites".
8.2/ Quand les théorèmes sont archivés à l'académie des sciences mondiales, les axiomes écrits en blanc sur blanc doivent être facilement et AUTOMATIQUEMENT IDENTIFIABLES (recensables plutôt), aurtement dit, la preuve est archivée avec le théorème. (Bon même s'il y a par ci et parlà des fascicules de résultats)
9/ Maintenant tu veux probablement une explication de pourquoi "ensemble". En fait, comme je le dis souvent, ce n'est rien d'autre, là aussi qu'un constat. Il serait d'ailleurs plus exact de parler de fonctions plutôt que d'ensembles (et même plutôt d'applications). La raison est parfaitement simple: le langage est composé de mots (que l'on peut considérer comme "des lettres") séparés par des ESPACES. Et tout est fonction. Autrement dit:
<<Mot1 Mot2>>
se traduit juste en Mot1(Mot2). De même que :
<<Mot1 Mot2 Mot3>>
se traduit juste en (Mot1(Mot2))(Mot3)
Je ne te fais perdre de temps avec les trivialités consistant à gérer les parenthèses, c'est une autre affaire (ce sont des raccourcis)
Là aussi, ce n'est pas une opinion, c'est un constat factuel langagier bête et méchant.
Bien des gens voudraient pérenniser qu'un verbe n'est pas un sujet et que par exemple Medor mange est une phrase où on identifie bien le verbe. Hélas, il est IMMEDIAT que tu seras embêté avec la phrase Manger détruit qui a un sens parfaitement habituel dans la vie courante.
Ca se respecte, mais ce n'est pas du tout important.
Si tu te demandes pourquoi "ensemble" et non pas "fonction", c'est juste parce que PAR CONVENTION, les gens considèrent qu'un texte doit contenir des phrases. Par exemple, il n'est pas agréable de lire 3+4. On préfère lire 3+4=8.
C'est pourquoi au lieu de noter $\{x\mid x+5\}$, on préfère écrire $x\mapsto x+5$, mais que par contre, au lieu de noter $x\mapsto (x+5 = x^2)$, on préfère noter $\{x\mid x+5=x^2\}$. Mais ceci n'est qu'une différence poétique liée à ce qu'on veut que l'assemblage qui ne nécessite pas un environnement immédiat complétant est la phrase.
Ce FAIT langagier c'est lui ET LUI SEUL qui fait que tout est ensemble. Dans cette histoire, ZF n'a fait qu'obéir aux gens à la suite de la crise des fondements, mais il n'est en rien un cadre qui s'impose, il est juste un cadre que les gens MALGRE EUX ont décidé de ne pas dépasser. Mais j'insiste bien que "ne pas dépasser" ne veut pas dire "pousser au max de sa puissance". Ceux qui le poussent au max, ce sont les théoriciens des ensembles professionnels.
Il est donc complètement débile, puisqu'on taffe, qu'on le veuille ou non dans ZF (et même un petit fragment) de dire qu'on a trouvé telle et telle usine à gaz qui en sort. Ce n'est pas tout simplement honnête et c'est inventer un moulin à vent contre qui crier victoire. Et ça désinforme bêtement les néophytes.
Maintenant, comme je l'ai souvent fait, et tu peux relire ma réponse à xax, je rappelle que nous taffons dans une théorie CONTRADICTOIRE et non pas dans ZF. On a simplement tendance à l'oublier parce comme je l'ai dit ci-dessus, les gens "n'éprouvent pas le besoin" d'étudier les grosses collections, mais elles sont là point barre.
Il se trouve juste que c'est LA LOGIQUE qui est elle-même IMPACTEE. Et c'est "tant mieux". La physique nous a confronté depuis 150ans à des phrases égales à leur négation, mais les matheux font hypocritement comme s'ils n'étaient pas au courant. La science s'applique. Les preuves servent de garanties par l'entremise d'interventions humaines matérielles fragiles. Nos axiomes logiques rejettent la charge de l'affectation de valeurs se trouvant dans $\{vrai; faux\}$ sur l'être humain habillé en bleu de travail qui va soulever des cailloux et déplacer des parping, ou couper des fils de nylon avec un cutter.
Rien dans les formalismes que nous utilisons ne vient discerner cette interface d'une interface divine infaillible. Il n'est pas donc pas du tout étonnant que $0\neq1$ puisse être ébranlé par de gros cardinaux et que $e:= \{x\mid x\notin x\}$ soit tel que son poids situe la phrase $e\in e$ au milieu de l'intervalle $[vrai; faux]$
Parmi les gens qui ont décidé d'étudier les grosses collections (qui font vaciller la solidité du vide logique, car valent $1/0$ et non pas juste $\infty$) à ma connaissance le seul "honnête homme" est Quine avec NF. Lui au moins n'a rien rejeté et juste proposé une autre partie, qu'il a parié fructueuse de l'unique et inamovible théorie contraidctoire (en logique classique) fondatrice qu'est : $\forall R\exists a \forall x: ((x\in a)\iff (x\in R))$
Remarque HS: NBG n'a qu'une seule sorte d'objets, simplement les gros sont définis par
$$x\mapsto (\forall y: x\notin y)$$
Plus sérieusement, contrairement à ce qu'affirment les gens qui n'y connaissent manifestement pas grand chose en fondements, dont la TOTALITE des auteurs du livre collaboratif HoTT (dont je viens de lire l'introduction et qui n'est qu'à peine moins erronées que les introductions des profs de CPGE lambda en logique en année 1) , ZF n'est pas un "fondement".
Un théorème prouvé dans ZF, comme un théorème prouvé dans la théorie TX comme un théorème prouvé dans HoTT, etc, c'est un énoncé de la forme A=>B où A est une conjonction des axiomes utilisés par la théorie (ZF,TX,HoTT, TrucMuche).
Les matheux ne s'amusent pas à dire à chaque instant "sachez msieurs-dames qu'il existe $x$ tel que $\forall y: (y\in x\iff R(y)),$ et que je vais prendre un tel $x$ que je vais nommer $a$, et donc dorénavant blabla a blabla"
Ils écrivent tous "with $a:=\{x\mid R(x)\}$ blabla a blabla"
Et la plupart du temps d'ailleurs*** écrivent "with $b:=\{x\in c\mid R(x)\}$ blabla b blabla" ce qui les situe immédiatement dans $Z$ plutôt que $ZF$ (je rappelle $Z\subset ZF$)
MAIS: ce n'est pas ZF qui les guide (à la rigueur on pourrait "mieux tricher" en disant que c'est $Z$ qui les guide, mais bon), c'est eux tout seuls qui "pensent".
Tu n'as peut-être pas lu le début du fil où je rappelle que de toute façon, on a en amont de tout le reste l'égalité "en dur" définitionnelle dans toute la science:
$$ u\in \{x\mid expression\} = ReplaceByDans(x,u,expression)$$
où ce qui est EXACTEMENT LA MËME CHOSE/
$$ (x\mapsto expression)(u) = ReplaceByDans(x,u,expression)$$
qui se moque comme d'une guigne que les gens ne vont utiliser ça qu'avec des expressions "gentilles". Il faut bien comprendre que c'est une égalité en dur AVANT la logique. (Pour te représenter la structure, tu quotientes par la relation (elle s'appelle beta-équivalence)). Par exemple, HoTT est une triste tentative usine à gaz de mettre un système de typage bien connu et complexe pour brider violemment, ZF n'est pas vraiment "une tentative", mais plutôt un constat que les gens ne sont jamais tentés (ou pas souvent) d'utiliser de grosses collections, mais tout ça, c'est dérisoire. On fait tous la même chose et les pros taffent essentiellement, au plus haut dans $P(\R)$.
En espérant t'avoir éclairé. J'ajoute une chose. Comme il a été démontré (je retrouverai les références du théorème), la partie utilisée par HoTT est triviale, ie les maths subtiles se situent au niveau non normalisable (ce qui est en fait évident, d'ailleurs, pas tellement besoin de preuves "complexes" puisque le normalisable est la zone des programmes qui terminent, donc sont inutilisables**). Ca représente pas loin de 40ans de retard sur les développement sérieux et pertinents en CCH. Autrement dit, en allant chercher des alliés pour leur pub, et en programmant COQ, ce petit groupe a complètement oublié de taffer. Ils réussissent l'exploit de mettre ensemble deux trivialisations stérilisantes:
1/ programmes qui terminent (donc de peu d'intérêt fondateur)
2/ Non intégration de la découverte de Timothy Griffith qui intègre le RPA dans la CCH.
à quoi il faut ajouter
3/ une hyper-extensionalité (l'univalence) qui est très exactement le "mauvais sens" pour comprendre le fond des choses (là aussi des théorèmes robustes l'établissent, ce n'est pas une opinion)
4/ et un logiciel difficile d'emploi pour le tout venant.
** par essence "fondation" = "OS" = "programmes qui bouclent". Le jour où tu es en train de taper un article t'es vachetement content si unix ou windows décide de terminer :-D :-D
*** je rappelle que $\{x\in a\mid P\}$ est une abréviation de $\{x\mid x\in a$ et $P\}$ (contrairement là aussi à des usages, mal compris, cherchant des distinctiions là où il n'y en pas)
Rien ne m'empêche de me placer dans une théorie où je postule :
Soit a un élément de l'ensemble vide,
et d'en conclure que je comprends les maths.
Le problème est que j'aurai de la peine à convaincre un lecteur ..
C'est un peu ça le problème des théories contradictoires, non ?
De même si tu prouves le théorème de Brouwer comme suit:
1/ je prends $a:= (x\mapsto f(x(x)))$
2/ Je calcule $f(a(a))$ et vous remarquez que c'est $a(a)$.
3/ J'ai mon point fixe $p:=a(a)$ pour $f$.
Mais qu'est-ce que tu auras alors fait? Et bien c'est simple, tu auras utilisé un outil (EXISTANT BEL ET BIEN) qui est "trop fort"
Quand l'usine te répondra pour acheter ou pas ton produit et l'exécuter, elle ne t'enverra pas de chèque, mais "Cher, Monsieur, nous vous remercions, mais nous n'avons hélas pas les moyen de nous fournir en $x\mapsto x(x)$. aussi votre produit partiel ne nous sera d'aucune utilité, car aucun de nos sous-traitant ne dispose de la pièce dont vous déclarez qu'il faut la mettre à droite de $\circ$.
Ce qui compte ce sont les preuves. Si tu n'utilises pas un axiome dans ta preuve, personne ne te dira que sous prétexte qu'il fait partie d'une théorie dont il est membre et qu'on rejette cette théorie, on rejette ta preuve.
Sinon, la plupart des articles seraient retoqués au nom du fait qu'on ne sait pas si ZF est consistant ou pas.
Quel est l'intérêt de ce que je prouve dans une théorie contradictoire ?
Si tu écris une preuve en utilisant ces "gros" ensembles là, mais tous propres, tu fais une démonstration dans NF (le système de Quine). C'est tout.
Si tu mélanges et obtiens une contradiction avec par exemple 4 ensembles autorisés par ZF et 5 ensembles autorisés par NF et bien ça va juste dépendre de l'intérêt de ta preuve, rien n'indique a priori qu'elle sera inintéressante.
Comme le rappelait Martial récemment, en 2014 (il a mis l'article en lien) il a été prouvé que NF est consistante (moyennant la consistance de ZF + peut-être quelques modérés gds cardinaux, je n'ai pas encore lu).
De toute façon, là, on sort du sujet. Ce que je dis est juste que ce sont les preuves et non pas les théories qui comptent. Par exemple je sais prouver sans dupliquer les hypothèses que $\forall a:[(\forall x: ((x\in a) =x\ontin x)) \to (0=1)]$. Et bien la preuve est très nettement plus longue que l'habituel argument diagonal. Essaie de le faire en exercice tu verras, ce n'est pas si facile et pourtant tu es fort.
D'une manière générale, il n'est jamais bon "d'interdire", comme l'a fait par exemple 708 (mais aussi bien d'autres gens!!!) en disant "je n'ai pas le droit d'écrire que". En effet, n'importe qui prouve immédiatement, mais surtout plus gravement LUI-MEME, prouve que c'est faux, puisqu'il l'écrit en disant qu'il n'a pas le droit de l'écrire.
Je me répète: le fondement de la science ce n'est pas une théorie, c'est le logiciel de recensement de ce qui est utilisé, qui lui doit être correct et surtout chiadé.
(:P)
Il existe certes des programmes $T$ qui affichent après exécution, "le texte affiché par $T$ affirme quelque chose de faux" (**)mais leur assimilation à leur production (voire à un énoncé mathématique en bonne et due forme) est un abus de langage (un lambda terme n'est pas "égal en dur" à ses réductions).
[size=x-small](*) $\neg A$ contient au moins un symbole de plus que $A$, à savoir "$\neg$".[/size]
[size=x-small](**) @christophe c: plutôt que des phrases plus authentiquement gödéliennes ("F(100110110) =>X" où 100110110 est l'encodage de la phrase entre guillemets), c'est toujours ce type d'exemple qui apparaît dans tes textes de promotion de l'inconsistance de ZF[/size]
@Foys : il y a tout de même une grosse différence entre exécuter une preuve ou le RPA est juste mis en hypothèse et une preuve où il est réalisé. Même si la preuve elle même ne change pas c'est un peu dommage de mettre en hypo ce qu'on sait réaliser (et c'est trompeur).
@GA : en TQ je suppose que c'est évident pour toi et en TDE exemple : (edans e) où e est l'ensemble des X tels que x pas dans x.
Je ne crois pas que ma vision des fondements en soit influencée, pour la bonne et simple raison que je promeux comme tu dis les théories inconsistantes. Ce serait fort de café de m'attribuer l'idée saugrenue que je cherche à casser ZF pour mieux l'aimer au titre que j'aimerais que les contradictoires :-D
Mon problème est pourtant simple : si je me base sur ton abréviation qui me semble imprudente et que j'écris l'innocente proposition
$ \{x\mid x=x\}$ = $\{x\mid x=x\}$
je me retrouve à dire tout et son contraire !
$\forall$x (x $\in$ Toto $\Leftrightarrow$ x = x) (abréviation cc)
$\exists$x$\forall$y (y $\in$ x $\Leftrightarrow$ (y $\notin$ y et y $\in$ Toto)) (schéma compréhension)
$\forall$y (y $\in$ a $\Leftrightarrow$ (y $\notin$ y et y $\in$ Toto)) (règle introduction constante)
$\forall$y (y $\in$ a $\Leftrightarrow$ y $\notin$ y)
a $\in$ a $\Leftrightarrow$ a $\notin$ a
Je dis tout ...
... et son contraire !
Je suis intéressé par des phrases égales à leur négation en TQ et des phrases égales à leur négation en maths. Pour les maths, OK. Est-ce qu'il faut comprendre que tu veux dire les choses suivantes (j'essaie de résumer mais je ne dis pas que je suis d'accord) :
1) Il n'y a aucun problème moral à utiliser le schéma de compréhension non restreint, c'est juste qu'il est connu qu'avec ça on démontre facilement le faux.
2) En fait, notre langage, ontologiquement et intrinsèquement, nous oblige à considérer que tout est ensemble (et que tout est fonction) et le schéma de compréhension non restreint est naturel dans notre langage. C'est en ça que nous travaillons toutes et tous dans une théorie contradictoire. En mode slogan : "langage = théorie des ensembles avec schéma de compréhension non restreint" où on entend que l'égalité est au sens "non opératoirement différent" (i.e. on ne peut pas distinguer la pratique de ces deux choses).
3) $ZF(C)$ est un des seuls (ou est le meilleur ?) ensembles de règles de conduite que l'humanité a trouvé pour éviter de démontrer trop de choses fausses et ça marche... pour l'instant.
Mais, si tout cela est vrai, rien ni personne ne fonde rien, n'est-ce pas ? Pas plus $ZF$ que $NF$ ou que $HoTT$ ?
Bon et pour la TQ, ben je veux bien voir aussi. Je suis d'accord avec ce qu'a dit Foys dans un autre fil : en TQ, une phrase est un sous-espace (fermé) d'un Hilbert, sa négation est son orthogonal, et donc il ne peut y avoir égalité que si le Hilbert est nul. C'est un peu comme "le vide est égal à son complémentaire dans l'ensemble vide". Et alors ?
Je trouve que tes points 1 et 2 résument plutôt bien ma position, même si comme tu t'en doutes, il y aurait à préciser pas mal de choses surtout à l'adresse de gens "à l'ancienne" qui pourraient mal comprendre les choses TELLES QUELLES.
Je n'approuve en revanche pas du tout le point 3. Je ne crois pas que l'humanité "ait trouvé ZF" pour ensuite s'y plier. L'humanité (comme tu dis) a juste CONSTATE que personne n'a jamais ADMIS comme axiome AUTRE CHOSE qu'un tout petit fragment de ZF(C). Une chtite psychanalyse vite faite de Zermelo et Frankael a ensuite suffi à mettre de l'encre sur du papier pour dire "ok, bin msieurs-dames, ne vous fatiguez plus à écrire que vous admettez ceci et cela, on l'a fait pour vous, ce sera réputé admis dans chacun de vos articles".
La question ensuite de savoir si on y prouve des choses "vraies" n'a pas vraiment de sens, car on y prouve des choses à propos du monde des objets mathématiques où la vérité est triviale, mais ça ne garantit rien sur le monde réel qui n'est pas égal à son illusion (à ses apparences si tu préfères). De plus, je ne crois pas un instant qu'il y ait en profondeur qui que ce soit qui considère autrement un théorème $P$ de ZF, que comme un théorème absolu disant $ZF\to P$. Certes, il y a des inconditionnels, mais bon, ils sont très minoritaires.
De même pour n'importe quelle autre théorie. Comme il n'y a pas d'entiers, de mots, de phrases, etc, bref rien de mathématique en dehors des modèles de ZF (pour l'heure), de même que comme il n'y a pas d'algorithme non calculable (pour l'heure aussi : thèse de Church), en particulier, comme il n'y a pas de modèles qui habite en dehors de tout modèle de ZF, évidemment que les gens ont une certaine à penser que si $ZF\to P$ alors $P$ est vrai, mais c'est au nom d'une conviction extrêmement précise qui est que les choses dont parle $P$ sont toutes dans la réunion des $M$ quand $M$ parcourt les modèles de ZF. Je ne dirais donc pas que c'est un "faute de mieux", mais une réelle "conviction factuelle" des gens. Même s'ils n'en sont pas conscients (hélas, ce qui provoque parfois des malentendus)
Oui, j'avais vu que Foys faisait remarquer qu'un état quantique PUR est un sev d'un Hilbert. On est bien d'accord. Mais les morceaux d'objets étendus spatialement ne sont pas dans des état purs, ils sont gérés actuellement (et ontologiquement mal) avec le même formalisme que les mélanges statistiques classiques d'états purs (et souvent, à tort, considérés comme saisis par leur matrice densité (celle du groupe statistique entier). Un superposition CLASSIQUE (ie $a+non(a)$) est une phrase égale à sa négation:
$$ non(a+non(a)) = non(a) + non(non(a)) = non(a)+a=a+non(a)$$
Alors attention, c'est un peu subtil car le $+$ ici n'est ni le $ou$ classique de l'ignorance ni le $+$ quantique. Mais ce n'est pas grave, je pense que tu comprends. La cohabitation subtile entre les différents opérateurs binaires émergeant de la TQ n'est pas du tout finie d'être étudiée et pose de gros problèmes de statut (la téléportation quantique en donne un des meilleurs exemples, en montrant que le $ou$ classique lui-même est indiscernables, dans certaines contextes du "et" quantique)
@christophe :
Euh, si Foys disait ça, je ne serais pas d'accord. Pour moi (et j'espère ne pas me tromper), l'ensemble des phrases est un sous-treillis ($\sigma$-complet orthocomplémenté) du treillis des sous-espaces fermés d'un Hilbert, et on appelle état une application de $\{phrases\}$ vers $[0,1]$ qui vérifie les mêmes axiomes que "mesure de probabilité" dans la théorie de l'intégration. Maintenant, le théorème de Gleason affirme que tout état est égal à $F \mapsto Tr(AP_F)$ où, pour tout sous-espace fermé $F$, $P_F$ est le projecteur orthogonal dessus et où $A$ un opérateur positif de trace $1$. Un état est dit pur si $A$ est le projecteur orthogonal sur une droite vectorielle (un tel opérateur est positif, de trace $1$). Alors, quand tu affirmes citer Foys comme ci-dessus, ou que tu dis
ben j'ai envie de dire que soit je ne suis pas d'accord du tout (au vu de ce que j'ai écrit ci-dessus) ou alors je ne comprends pas ce que tu veux dire.
Je sais absolument pas ce que veut dire ton $+$ (qui ne serait pas le "+ quantique" - je ne sais pas ce que c'est non plus). Si je prends deux phrases (deux sous-espaces) je peux prendre le sous-espace (adhérence de la) somme ; si je prends deux projecteurs orthogonaux, je peux prendre leur somme (mais ce n'est pas souvent un projecteur, et si l'un des deux espaces est l'orthogonal de l'autre, alors la somme des projecteurs est bien un projecteur car c'est... l'identité).
En outre, je ne comprends pas grand chose à
La téléportation quantique, c'est bien le fait de savoir transmettre exactement un état à condition de savoir transmettre quelques bits classiques ? Quel rapport avec la choucroute ?