Catégories et types

De mon téléphone. Concernant la recherche sur les théories faibles (ie qui courent le moins de risque d'être contradictoires ) je crois que la question de la consistance de NF à été résolue récemment ou alors j'ai rêvé???

C'edt un très jolie et sobre théorie que l'on peut voir comme mettant en valeur la notion de type. Elle a tous led avantages de HoTT mais n'en a pas les inconvénients ni le côté usine à gaz artificielle et "voulue à la force du poignet". De plus elle a le mérite de pré exister à son intention ce qui la rend moins suspecte.

Et cerise sur le gâteau: elle est programmable facilement. À vérifier donc...

Salut ignatus,

Pas de souci. Si tu veux je peux te donner (un peu) plus d'infos sur la sémantique catégorique de la théorie des types mais comme je l'ai dit.plus haut ça ne répond pas forcément à ta question, qui est en soi assez compliquée.

Ok, je te ferai un mini topo (sans mauvais jeu de mots) quand j'aurai le temps (peut-être demain, mais je ne garantis rien)

Bon, très brièvement, l'idée est la suivante :

En théorie des types tu as des types $A,B,C,...$ et des opérations dessus. C'est de la syntaxe : si j'ai un type $A$ et un type $B$, je peux par exemple former $A\to B$, mais ce $\to $ ne représente rien, ce n'est qu'un symbole. Ce serait plus qu'un symbole uniquement si on avait une sémantique.

Dans une catégorie $C$, on a des objets $A,B,C,...$, et si la catégorie est suffisamment gentille on peut faire des constructions dessus : par exemple s'ils existent, on peut former le produit cartésien $A\times B$.

Bon où est le lien à part une certaine similarité formelle ? Beh en théorie des types on a des règles de constructions, de dérivations de jugements etc. (je ne rentre pas dans les détails et je ne peux pas : il y a plein de théories des types avec des nuances et des variations, donc à part dans mes exemples je dois rester très vague).
Un exemple typique (sans mauvais jeu de mots) est le type produit : (dans certaines théories des types) si on a deux types $A,B$, on peut former le type $A\times B$. Associé à ça, on a deux flèches de type $\pi_A: A\times B\to A, A\times B \to B$ et des règles qui ressemblent essentiellement à $\Gamma, x:A, y:B \vdash (x,y):A\times B$;
$\Gamma, x:A, y:B \vdash \pi_A(x,y) = x : A$;
$\Gamma,x:A, y:B \vdash \pi_B(x,y) = y : B$ ;
$\Gamma, s : A\times B \vdash s= (\pi_A(s), \pi_B(s)) : A\times B; $

On voit directement la similarité avec le produit cartésien dans une catégorie : que nous disent ces règles ? Elles nous disent essentiellement qu'un terme de type $A\times B$ c'est pareil qu'un terme de type $A$, et un de type $B$.
En catégories, un morphisme $C\to A\times B$ c'est pareil qu'un morphisme $C\to A$ et un morphisme $C\to B$.

ça suggère que plus généralement les règles syntaxiques de théorie des types (en logique plus généralement, d'ailleurs) correspondent à des propriétés/constructions universelles en théorie des catégories. Eh bah en suivant ce principe jusqu'à son aboutissement, on obtient une sémantique de notre théorie des types dans une catégorie avec suffisamment de structure.

Pour te donner une idée générale d'à quoi ça ressemble (c'est pas du tout important de comprendre les détails à ce stade !), je prends une théorie des types très basique, qui a disons un type distingué $\mathbf 1$ avec un constructeur $\Gamma \vdash * : \mathbf 1$, et un constructeur $\times$ qui a les propriétés décrites plus haut, et finalement un constructeur $\to $ avec certaines propriétés syntaxiques (que tu peux t'amuser à chercher un peu, ne t'inquiète pas si tu n'as pas la liste complète ou quoi que ce soit) qui disent essentiellement que $A\to B$ est le type "des fonctions de $A$ vers $B$". Alors pour toute catégorie cartésienne close (CCC) $\mathscr C$, et fonction $[|-|] : $ types élémentaires $\to$ objets de $\mathscr C$, on obtient une sémantique (interprétation) de notre théorie des types dans $\mathscr C$; où on étend notre fonction à tous nos types via $[|A\times B|] := [|A|] \times [|B|]$, $[|\mathbf 1|] = $ objet terminal, $[|A\to B|] = B^A$ (hom interne, puisqu'on est dans une CCC);

et ensuite à tout terme $t:A$ dans un contexte $\Gamma = (x_1 : A_1, ..., x_n : A_n)$ on va associer une flèche dans $\mathscr C$ qui s'appellera $[|t|] : [|\Gamma |] \to [|A|]$ où $[|\Gamma|] = [|A_1|]\times ... \times [|A_n|]$. Cette définition se fait par induction sur la complexité des termes, en utilisant à chaque fois la similitude entre les notions syntaxiques de notre théorie des types et les constructions/propriétés universelles dans $\mathscr C$.
Il faut ensuite vérifier (en général ce n'est que mécanique, et souvent long et ennuyeux) que notre interprétation préserve ce qu'il y a à préserver : si deux termes se réduisent à quelque chose d'égal, alors leurs interprétations sont égales, etc. etc.

Après il y a plein de trucs drôles : comme de manière générale, la sémantique permet de démontrer des résultats de consistance relative,on peut définir des morphismes entre interprétations; on peut s'amuser à prouver des résultats de complétude (dans le cas simple que j'ai décrit on aura une "catégorie syntaxique" qui sera l'interprétation initiale, et dans celle-là "vérité" sera équivalent à "prouvabilité") etc. etc.

Comme je n'ai pas été spécifique ce schéma peut s'étendre un peu : si on prend une logique intuitionniste un peu bornée, le même genre de chose permet de l'interpréter dans un topos, et à nouveau on aura des résultats de consistance relative, on aura de la complétude (et pour les "théories géométriques", on aura un "topos classifiant" qui sera le "modèle libre" de ladite théorie) etc. etc.

Après il y a des trucs plus compliqués qu' on commence à peine à savoir faire : par exemple HoTT on vient de lui trouver des modèles, mais c'est plus subtil (c'est une théorie des types où pour $x:A, y: A$ on a un type $x=_A y$ qui n'est pas qu'un simple jugement, il faut un moyen de gérer ça).

Pour plus de détails il faut un peu plus se fixer sur ce qu'on veut étudier, et plus de temps :-D

Comme je l'ai dit, ça ne répond pas vraiment à ta question, puisqu'on ne se "libère" pas du tout de la théorie des ensembles (nos catégories sont toujours définies via les ensembles), et la question de définir les catégories dans une théorie des types est très complexe : pour HoTT, les expert.e.s ne sont pas (me semble-t-il) d'accord sur quelle est la bonne définition de catégorie interne à HoTT

708 : surtout ça perdrait l'intérêt de tout faire dans HoTT :-D

Bon comme je ne suis pas prêt d'être sur un ordinateur et que je ne me lasse pas de voir mon téléphone écrire ce que je lui dicte sans pour autant que j'ai besoin de parler doucement je donne quelques détails

Premièrement les types au début du siècle ont été inventé pour tenter d'avoir des théories consistantes mais comme modèle l'a découvert plus tard ça se paye dès qu'on fait un effort dans le sens de la consistance en a automatiquement une très forte pauvreté de la théorie

Deuxièmement les types tel qu'on l'entend aujourd'hui en langue de calcul en catégorie ça n'a presque rien à voir en fait un terme du lambda calculer quand il est type Absa garantie qui va s'arrêter on dit qu'il est normal isable c'est une garantie de consistance mais c'est pas tout à fait la même

3e man on peut toujours inventer des types bizarroïde pour clan auto références qui fait que de toute façon n'importe quelle théorie sera type able ou plus précisément n'importe quel nom se sera type able avec ses nouveaux types a inventé et ça m'a pas très loin

Bon à ce que je vois il a encore des efforts à faire mon téléphone pour écrire ce que je lui dicte donc j'aime arrêter la globalement si tu veux il y a beaucoup de publicité en faveur des Duty page mais en fait maintenant ce qu'on met derrière le mot typage est devenue une espèce de spécialité non mathématiques pas c'est-à-dire que c'est devenu une espèce de but et que ce weekend en mathématiques mais que les gens en vente chaque jour des moyens mathématiques pour le satisfaire partiellement

Ah là là c'est vraiment trop marrant de voir les phrases s'écrire à toute vitesse je fais aucun effort pour parler doucement c'est ça le pire

Christophe
Quand tu utilises cette prise de notes par ton téléphone, [large]relis-toi avant d'envoyer[/large]. Cela te permettra de corriger les interprétations du logiciel, qui font que ce que tu écris est partiellement incompréhensible et sûrement non conforme à ce que tu voulais dire.
Merci.
AD

Je suis sur wifi et un pc. Ignatus, je te donne des précisions.

1/ Désintoxique-toi de l'hypnose qui a envahi une partie de la communauté consistant à croire qu'on parle de fondements. Les catégories, les topos, HoTT, etc n'ont jamais, au grand jamais touché à un gramme de débat sur les fondements.

2/ Cette erreur de mot provient (probablement) qu'ils auraient peut-être estimé "encore plus vantard" de se revendiquer "chercheurs d'unification, de la grande théorie du tout". Alors ils ont opté (mensongèrement) pour remplacer le mot "unification" par le mot "fondement", faisant ainsi un certain mal à la vérité et à la compréhension. Peut-être ne voulaient-ils pas ressembler aux physiciens qui gonflent le torse avec leurs théorie des cordes and co, et qui ont durablement donné une image stupide à leur psyché collective.

3/ Début du 19e, il y a eu une crise, mal diagnostiquée, qui a encore laissé des traces aujourd'hui sur les débutants. Ces traces s'expriment sous la forme de "recherches de théories consistantes", donc faibles, MAIS qui "en même temps", donneraient du jus.

4/ Autrement dit, une sorte de réhabilitation de "Hilbert versus Godel"

5/ Et c'est dû à de l'amateurisme dans le domaine.

6/ Maintenant, ça n'empêche en rien, le fait d'avoir une approche de bisounours pathétiquement vantard, de produire de bonnes maths, ou des maths compliquées. Ca n'a rien à voir.

7/ Il faut simplement, pour comprendre ce qui se fait, parvenir à tenir éloignés les discours tarte à la crème sur les intentions. Par exemple, HoTT réinvente l'eau chaude et ça lui fait plaisir ("il" = ses précurseurs), pour des raisons psychanalytiquement un peu inavouables (une éternelle volonté d'empêcher le coming-out du slogan "maths = logique appliquée" *** ) bon et bien c'est pas grave, l'important est "d'avoir du plaisir".

8/ Sur le fond, indépendamment des hommes, toute tentative, je le répète, d'acheter de la consistance à Dame Nature se paie cash par un renoncement à l'accès à l'échelle des consistency-strength qui PAR DEFINITION s'incarne en transgressant les types.

9/ On a donc un "versus" clair.

10/ On a même un théorème très simple et élémentaire qui résume toutes ces agitations intra-verre d'eau qui est le suivant: (mon dictaphone l'a mal traduit :-D ) : un terme est typable (dans un système de typage très simple) si et seulement si il est fortement normalisable.

11/ C'est un théorème basique et constructif qui vouera systématiquement à l'échec non pas ces travaux, mais les intentions dont leurs producteurs prétendent animés

12/ Et le plus amusant N'EST PAS le sens "typable => normalisable" (qui hélas occupe stérilement les esprits à plus de 90% contre moins de 10% pour l'autre sens) mais le sens "normalisable => typable"

13/ En résumé, même si non dit cash, le typage est essentiellement une recherche de consistance et un fermage d'yeux sur le prix payé évoqué en (8)

14/ Les catégories avec leurs flèches ** donnent l'impression d'offrir un paradigme typant à bon compte et EN PLUS à un compte sémantique, mais là encore, ce n'est qu'une dérive politique proche de ce qui précède.

15/ Pär contre, il est ABSOLUMENT FASCINANT de s'amuser à faire des maths avec tout ça. Plus les intentions sont délirantes, pauvres et rhétoriques, plus les terrains explorés risquent d'être vierges et accidentés. L'intérêt, entre autre, est que presque toute question donne un exercice difficile

16/ Exemples (exercices paramétrés par la catégorie non précisée):

16.1/ mono et épi => iso?
16.2/ catégorie CCC et extensionnelle + all limites raisonnables => topos?
16.3/ Classer les 1001 versions de l'hypothèse du continu (toutes équivalentes à HC dans un univers ensembliste classique) par classes d'équivalence prouvables
16.4/ Un topos de Grothendieck (ou de préfaisceaux) construit sur un univers ayant tout ce qu'il faut comme grand cardinaux contient-il un "ensemble" inaccessible?

etc, etc

17/ Le seul conseil que je te donne (et en fait te redonne en radotant) c'est de faire une certaine partie toi-même. Par exemple, tu peux remarquer que tous les énoncés platoniciens profonds et célèbres SE TRADUISENT FACILEMENT DANS LES TOPOS (existence d'un ensemble infini, hypothèse du continu, équations diophantiennes ayant ou pas de solutions, hypothèse de Riemann, problèmes ouverts médiatiques, etc)

18/ L'intérêt de villégiaturer tout seul est AUSSI de réaliser qu'il y a plein de manière de parler NON EQUIVALENTES et que les spécialistes catégoriciens EN ONT CHOISI UNE PAR IDEOLOGIE (idéologie que je ne critique pas, mais que je signale telle, car bcp de gens pensent que les chemin a été déductif)

19/ Par exemple, dans n"importe quelle catégorie, comme tu vas le constater, tu peux te demander si elle réalise "ZF" via un ensemble inaccessible. Pour ça, il te suffit de prendre des relations binaires génériques (au sens populaire) comme suit:

19.1/ tu pars d'objets $G,A, X$ de ta catégorie et de deux flèches $g,f : G\to A$ . Tu décrètes qu'une flèche $u: X\to A$ "est dans" la flèche $v: X\to A$ quand il existe une flèche $z: X\to G$ telles que :

$$ u = f\circ z\ et\ v = g\circ z$$

19.2/ tu te retrouves avec un ensemble (l'ensemble des flèches allant de $X$ dans $A$) et une relation binaire "est dans" dessus.

19.3/ Of course, tu peux particulariser psychologiquement en renommant $X$ en $1$ (voire en dotant $1$ de l'hypothèse qu'il est terminal), mais en bref, entre langue et raisonnements, tu auras des classifications importantes à faire "à part toi" en quelque sorte.

20/ Le toposisme n'est qu'une élaboration "écologique" du point (19), en suivant un autre itinéraire et où on n'a plus la dichotomie bien nette "x est dans y" ou "x n'est pas dans y"


*** sur le fil news que partagent les matheux-chercheurs de Paris, j'ai assité à une passe d'amres amusantes et d'âge mental 6.5ans, entre 2 chercheurs: l'un semblait prétendre que les courbes elliptiques étaient le truc de maths le plus profond (il a provoqué des éclats de rire, mais un seul a répondu) et l'autre s'en désolait. Je rappelle que 99% de matheux font des choses très applicables et très concrètes (l'abstraction réelle ne reçoit pas bcp de crédits, car est souvent confondue avec de la philosophie d'une part, et nécessite l'infini: MQ étudiée en profondeur, grands cardinaux,
et + généralement th des ensembles, etc) ce qui n'a rien de dévalorisant. Par ailleurs trouver la consistance ne veut pas dire trouver les garanties: une théorie consistante peut très bien attribuer une solution à une équation diophantienne qui n'en a pas and SO ON. La consistance et les typages élaborés ne garantissent pas tant qu'on croit les choses et pas comme on le croit.

** la présentation avec objets et flèches, très rhétorique, même si rhétorique non voulue, des catégories est trompeuse. Une catégorie est juste un magma associatif parmi d'autres et se définit très bien comme ça. Quand on retire le $0$, ie l'élément "undefined" tel que $a\circ b = $ cet élément quand $a,b$ ne sont pas composable, on obtient une catégorie dès lors qu'on a impose au magma quelques propriétés calculatoire simples.



Je rappelle que j'avais ouvert un fil il y a longtemps pour dire quel est le véritable enjeu. C'est l'associativité!!!! Rien de plus, rien de moins mais si un jour on arrive vraiment à faire des maths avec comme opération unique (actuellement c'est $\in$, ou encore $Ap$ (rappel $\in = Ap$)) fondatrice une opération associative, on aura fait un bond.

Pour l'heure tricher en faisant "comme si" via le développement du paradigme catégoricien me semble stéril (actuellement, on a deux opérations si on en veut une qui soit associative****: $\circ$ et l'opération $\sigma$ qui à une fonction constante associe l'unique image qu'elle donne (ou, de manière équivalente en paradigme ensembliste, $\{x\} \mapsto x$)

**** $$f(a) = \sigma (f\circ (Constante(a)))$$

Je pense que tu te trompes christophe, sur quelques points.
Sur 1/ : HoTT, même si elle n'est pas pratiquée comme ça, et même si ce n'est pas sa vocation principale, a quelques mots à dire sur les fondements.
Alors je sais que tu as un point de vue très "rigide" sur les fondements ("la tde est inévitable puisqu'on veut que 'a b' ait toujours un sens et qu'on appelle juste l'espace entre a et b l'appartenance et qu'on le note $\in$", ou quelque chose de cet ordre là si je me souviens bien), mais tu dois savoir/te rendre compte que ce n'est pas le cas de tout le monde. En particulier fournir un paradigme différent où la distinction "ensemble vs proposition" disparait etc. peut se prévaloir (si c'est assez bien fait, etc.) de fournir des fondements (en un certain sens, qui ne correspond sûrement pas au tien)

Même chose pour les catégories, même si pour celles-ci la vocation fondatrice est bien plus ténue et n'a été menée essentiellement (il me semble) que par Lawvere, et qu'on n'est pas dans un "refondement" autant chamboulant que HoTT.

Sur 7/ : "HoTT réinvente l'eau chaude" - c'est quelque chose que tu as plusieurs fois affirmé sans l'argumenter. Alors en un certain sens c'est vrai : HoTT est en grande partie tout bêtement une théorie des types intensionnelle (Martin Löf Type Theory, MLTT) et donc pas grand chose de nouveau.
Cependant il y a 2 points importants à repérer ici : HoTT c'est notamment le parti pris de refaire les maths avec cette théorie des types (bon ça, tu me diras...); mais surtout l'essentielle différence entre HoTT et les autres théories des types (on parle souvent su type $x=y$ mais je crois que ça existait avant) c'est l'axiome d'univalence, qui a pour vocation de permettre aux matheux.ses de faire comme toujoirs, mais rigoureusement : identifier des choses isomorphes (bon moi ce n'est pas cet aspect là qui m'intéresse le plus mais c'est une différence fondamentale !)

15/ "pauvre [...] vierges et accidentés" : alors du point de vue logique et fondements je ne m'avancerai pas trop puisque je n'ai pas un point de vue global sur ce sujet; mais nombre d'applications de HoTT ne se concentrent pas là dessus , comme je l'ai dit plus haut ce n'est pas forcément la vocation principale de HoTT d'être fondatrice : il y a un intérêt certain pour la théorie de l'homotopie.
Quant à la difficulté de peouver quoi que ce soit, elle a un rôle : permettre que ça se fasse facilement à l'ordi.


Dans 16/ et 17/ il y a des imprécisions techniques catégoriques et toposiques, mais bon tu ne cherchais pas à être précis :-D

D'un PC, je complète.

max a écrit:

c'est quelque chose que tu as plusieurs fois affirmé sans l'argumenter.

Si si j'avais argumenté. En fait, il y avait eu un post où quelqu'un avait posté le manuel HoTT. Je l'avais parcouru, et je n'étais pas le seul à m'être étonné de l'abus du terme "homotopique".

max a écrit:

Alors je sais que tu as un point de vue très "rigide" sur les fondements ("la tde est inévitable puisqu'on veut que 'a b' ait toujours un sens et qu'on appelle juste l'espace entre a et b l'appartenance et qu'on le note $\in $", ou quelque chose de cet ordre là si je me souviens bien), mais tu dois savoir/te rendre compte que ce n'est pas le cas de tout le monde

Je suis même + ou - au courant que ce point de vue est très peu partagé, au même titre que quand je dis "math (resp science):= recherche de certitudes formelles absolues (resp bonnes)", etc. Les gens mettent du temps à comprendre que j'ai raison, car en fait, je procède souvent par "psychanalyse extravertie de la société", dis des évidences, ou plutôt "rappelle" des évidences qui hélas sont "peu médiatisées", donc dans un premier temps paraissent douteuses. Après un peu de réflexion, les gens finissent pas réaliser que j'ai raison, mais, ensuite, on a le problème "vaniteux" de le reconnaitre (qui est somme toute accessoire). Truc marrant (pour science et non pas math), on a eu l'illustration incontestée récemment avec le faux Dupont de Ligonnès, où une fois l'ADN bien regardée plus personne ... n'a douté).

En ce qui concerne l'espace entre les mots, il est lui aussi factuellement incontestable, mais, tu vois, tu me "sanctionnes" de rigidité. Alors que ce que tu voulais probablement dire est que tu loges "fonder" un peu après le premier stade que j'exprime, c'est à dire une fois constaté qu'on sépare les mots par un espace, "qu'est-ce qu'on fait?".


Le point le plus important de ton post est le suivant (qui contient une information exportable pour les lecteurs de passage (à la différence de notre échange un peu private joke sur le reste):

max a écrit:

mais surtout l'essentielle différence entre HoTT et les autres théories des types ....... de permettre aux matheux.ses de faire comme toujoirs, mais rigoureusement : identifier des choses isomorphes

Alors là, on est entièrement d'accord sur les faits (enfin potentiellement, je ne connais ni précisément les auteurs, ni précisément leurs intentions déclarées) et c'est bien là que se concentre ma critique :

je suis TOTALEMENT OPPOSE à ce genre de méthodologie d'une part, et surtout quand elle affiche une ambition complètement démesurée. C'est comme si tu disais (sans t'en rendre compte) que le but de HoTT c'est de faire que les maths deviennent entièrement résolues et automatiques toutes entières.

Mon désaccord, (en dehors de l'ambition bisounours publicitaire) avec la méthodologie est que fonder (et même unifier) ne doit pas passer par la création d'un système généré par un but subjectif. Or tel que tu le dis, on est en plein dedans.

A l'évidence, 2 objets isomorphes sont la plupart du temps différents, point barre. Rien que RECHERCHER, je ne parle même pas de trouver, à les identifier est UNE FAUTE SCIENTIFIQUE MAJEURE et non pas un but légitime. (Et c'est un peu long, mais je peux le prouver de plusieurs manières différentes et godéliennement).

On a déjà mis platoniquement un AXIOME dont la recherche RECENTE a prouvé le caractère magique (au sens péjoratif, à savoir qu'il est tellement puissant qu'il écrase pas mal de compréhension), qui "fait tout le travail" et dispense l'humain du temps d'exécution de la vie: l'axiome d'extensionalité. Il conduit à traiter comme égaux*** deux graphes connexes orientés et pointés isomorphes et à appeler les classes des ensembles.

Quelle étrange attitude que celle qui se revendique parfois de vouloir se libérer d'un prétendu joug ensembliste qui n'existe pas pour ensuite aller bien plus loin en voulant "trouver égaux" des "n'importe quoi" isomorphes?
Je termine en précisant à propos de mon post d'avant ce que j'ai prétendu appeler fondement en disant que la seule égalité fondatrice la plus en amont, y compris devant la logique est :

$$ (x\mapsto Machin) (u) = Machin[u\ remplace \ x] $$

qui se dit ensemblistement (mais ça revient strictement au même):

$$ u\in \{x \mid P\} = P[u\ remplace \ x]$$

pour justifier un peu cette remarque:

1/ Bien que le Lambda calcul étudie syntaxiquement au niveau zéro cette identification, je ne l'en tire pas.

2/ Je l'appelle "niveau le plus en amont" car en fait, même quand les gens prétendent ne pas le faire, il le font. C'est tout simplement le fait, en science de donner des noms, de créer des abréviations. On DEFINIT (ou prétend définir) que par exemple

$$ a:= (x\mapsto x\times x) $$

puis ensuite, on utilise $a$ et parle de $a(Toto)$ pour dire $Toto\times Toto$, même s'il est vrai que présentement, les gens ont opté pour l'exposant, ie $Toto^2$.

Un voile pudique s'est abattu sur cet aspect plus que fondateur du fait que la possibilité de paramétrer entraine.... que $0=1$. Ca s'est appelé la "crise des fondement". Cependant, la pudeur ne doit pas aller jusqu'à "voiler le beauté" de cette découverte. Ca ne sert strictement à rien de prétendre "non défini", par exemple $1/0$, plutôt que prétendre :

$$ 1/0 = UNDEFINED $$

De même que $x\mapsto f(x(x))$, fonction que j'appelle $G$, est telle que $G(G)$ est un point fixe de $f$, et que pour LA fonction par excellence qui n'a pas de point fixe "bien tolérée", à savoir la fonction $non$, ça a généré de la gène en rendant contradictoires les maths.

Et bien ces choses doivent AVANT TOUT ETRE ACCEPTEES, ce sont des DECOUVERTES et non des "erreurs". Cela fait 150ans (environ) qu'elles soont gérées par la paradigme du tabou, et ça pose des soucis.

Jusqu'à maintenant, (convention** ZF), on essaie de déduire des choses (peut-être pas $0=1$, mais d'autres, intéressantes) à partir de seulement les "petites collections" (appelées "ensembles"). Autrement dit, on a fait un choix CARDINAL. ON ne sait pas (et la th des ensembles a bien progressé) où se situe exactement la barrière (ie le moment où le cardinal est trop gros pour que $0\neq 1$ subsiste), menfin, on a tout de même pas mal balisé la route vers cette borne.

Comme remarqué (dans ce fil ou un autre, je ne sais plus), Quine avait aussi essayé** de déduire des joyaux en n'utilisant que des collections propres (en marge de l'immense majorité qui avait choisi "petite") à l'aide de NF. Il devait avoir ses adeptes, je ne sais pas, en tout cas, j'avais pas mal profité de certaines vacances en essayant aussi.

Je ne sais même pas si en relachant un peu le critère de propreté de Quine, ça reste consistant (ie en demandant numéro (x) < numéro(y) à la place de numéro(x) = numéro(y)-1 quand figure $x\in y$ dans la définition de la collection)

Les topos (par exemple) donnent à ce paradigme "tout sur le cardinal" à nouveau une expression des préférences.

Bref. Tout ceci pour dire que le seul axiome qui a été réellement découvert comme ayant réellement une autre nature (en apparence, j'ai souvent donné une définition de cet axiome comme cas particulier de compréhension) est l'axiome du choix. Et rien d'autre (en termes catégoriques, histoire de rigoler, il dit que tout épimorphisme a un inverse à droite).

** et je parle bien d'une CONVENTION!


*** je rappelle aux lecteurs pas au courant que la théorie des ensembles (ie la science) est l'étude du monde de tous les graphes orientés possibles, même en rêve, mais en quotientant itéremment pour avoir l'extensionalité.

@ignatus : je ne connais rien à la théorie des types (et encore moins à HoTT), mais je peux répondre à la place de Christophe sur le point 8 (il me contredira si je trahis sa pensée).
Admettons que, pour des raisons qui n'appartiennent qu'à toi (par exemple parce que tu ne t'intéresses qu'à l'arithmétique), tu décides que Peano te suffit amplement pour faite tes maths. Tu es quand même dans la merde parce que Gödel t'interdit de prouver la consistance de Peano.
Pas grave, parce que Z (la théorie ZF privée du remplacement et du choix) prouve Cons(Peano).
Mais à nouveau Gödel t'interdit de prouver Cons(Z).
Pas grave, parce que ZFC prouve Cons(Z).
Et zut, pas possible de prouver Cons(ZFC).
Pas grave, ZFC + "Il existe un cardinal inaccessible" prouve Cons(ZFC).
And so on.
Tu vois donc poindre le tout début d'une (longue) hiérarchie de consistency strength dont il serait quand même fort dommage de se passer si on restait dans les jupons de Dame Nature Peano.
Comme le dit Christophe un peu plus loin, on ne sait pas très bien où s'arrête cette belle hiérarchie, c'est-à-dire à partir de quand la hiérarchie coïncide avec $0=1$, mais la recherche moderne a quand même pas mal fait avancer les choses en ce sens (très optimistiquement je dirais : quelque part entre I0 et l'inconsistance de Kunen).
Je suis parfaitement conscient de n'avoir répondu que de de façon très parcellaire à ta question.

@ignatus: pour ton Doc tu peux voir tout seul je pense qu'il est malhonnête. C'est du TC da s le texte et ça se voit (80% de coms publicitaires vs 20% d'infos pour le lecteur qui voudrait de l'information brute qu'il traiterait lui même).

Pour "X espace Y" je ne suis toujours pas d'accord, mais ça c'est une autre affaire du coup je ne reviendrai pas dessus.

Le doc de 500 pages que tu avais vu est sûrement celui qu'on trouve ici (cliquer sur "download PDF for on-screen viewing"). Tu vas alors dans le sommaire, tu regardes II- Mathematics, 8-Homotopy Theory et tu observeras que toute une tripotée de résultats de base d'homotopie y sont reprouvés dans ce contexte de théorie des types : $\pi_1(S^1)$, théorème de suspension, Van Kampen, des analogues de Whitehead, etc. en bref, de l'homotopie.
Des progrès ont d'ailleurs été fait plus récemment : on a recalculé $\pi_4(S^3)$ etc.
Et comme je le disais, Shulman a montré que c'est "pas du vent", puisque HoTT (avec univalence stricte) a un modèle dans tout $(\infty,1)$-topos, comme par exemple celui des espaces - ce qui permet de montrer que tous les résultats "homotopiques" qu'on prouve dans ce cadre ce transportent dans le cadre usuel - sauf que là on les prouve synthétiquement, càd sans avoir à se préoccuper de qu'est-ce qui est continu ou une bonne topologie etc.
C'est un objectif "indépendant" de l'objectif ordinateur par contre :-S qui existe aussi, et comme la MLTT a permis des avancées comme Coq etc. on peut raisonnablement penser que HoTT est plus adaptée que ZF pour la vérification ordi (qui est actuellement extrêmement compliquée pour ZF si j'ai compris ce qu'on m'a dit)

"ie enseignable en 1H à un enfant de 11ans de bonne volonté et sain comme l'est la réécriture fondatrice actuelle" : :-D tu es très optimiste, à la fois sur la réécriture fondatrice actuelle et sur les enfants de 11 ans (enfin après, je ne t'ai jamais vu la décrire, cette réécriture fondatrice actuelle, peut-être que c'est ça qui me manque ? si tu as 1H à perdre un jour ...)

"Et non pour moi la science prouve et non pas cherche à imposer une théorie revendiquée comme fondatrice afin d'obtenir "les redultats qu'un groupe de gens veulent"." : c'est naïf d'imaginer ça. Si les maths ne faisaient que prouver, une fois qu'on a obtenu nos fondations, on pourrait mettre en marche un algo qui énumère tous les théorèmes de ladite fondation (disons ZFC pour simplifier). Au-delà de la complexité purement informatique de ce truc-là, personne n'en voudrait de ça !
Les maths avancent parce que les gens comprennent (pensent comprendre) de quoi iels parlent, et parce que les énoncés qu'iels prouvent les intéressent. Au contraire j'ai envie de dire, les théories qu'on étudient en maths sont précisément celles que les gens veulent étudier (c'est quasi tautologique en fait). Sinon pourquoi ne pas étudier les monoïdes dénombrables vérifiant $xyxz = xxzy$ ?
Ensuite, le pas naturel suivant est de "vouloir un résultat" : c'est comme ça que se fait une bonne partie des maths : par exemple (c'est faux historiquement -pas totalement mais quand même - mais tu comprendras mon idée j'espère) je veux obtenir une récurrence sur autre chose que $\mathbb N$, c'est mon désir. Bah je travaille, je travaille : hop, je tombe un jour sur les ordinaux, et je vois que j'ai obtenu mon désir donc je suis content. Autre exemple : je veux pouvoir faire de l'analyse comme j'ai l'habitude mais sur des espaces vectoriels de dimension infinie. Je bosse, je bosse : hop , je remarque que la notion d'espace de Banach est sympa et permet d'obtenir mes désirs : je suis content.
Bref, les maths avancent précisément parce que les gens qui en font ont des désirs, veulent des résultats et ont des intérêts.
Sinon je te dis on ferait juste l'énumération des théorèmes de ZFC : on aurait beaucoup plus d'énoncés :-D

De mon téléphone @max. Je ne parlais pas du désir de prouver mais du désir d'obtenir sans preuve. Je n'ai jamais contesté que ce qui se développe est dépendant de la motivation des gens à prouver.

Encore une fois si on met l'homotopie dans un système on l'y retrouve. Ça n'a rien à voir avec prouver son inévitabilite.

En outre l'homotopie est forall exists arithmétique VOIRE forall il y a donc pas de "nouveauté" à automatiser. J'insiste sur je ne critique pas la qualité de ces travaux mais la pub mensongère que les gens tentent de lui associer.

@max: de mon téléphone. Si si j'ai donné les fondements "moins de 1H".

1/ admettre = supposer

2/ (u est dans {t/ R(t)} ) = R(u) ou ce qui revient strictement au même :

2bis/ ( t mapsto R(t) ) (u) = R(u)

Autrement dit "abréger et tout expliciter.

Ça n'a terdit pas enduite de se brider pour éviter le cardinal 1 du monde total des possible, mais le bridage (par exemple NF ou encore ZF) n'est pas un fondement en amont, mais une convention des axiomes (hypothèses) réputés présents même quand pas écrits (exactement au même titre que les parenthèses invisibles MAIS PRÉSENTES en classe de cinquième)

PS : si je suis un peu virulent, c'est parce que je connais pas mal de victimes qui n'ont pas pu accéder vraiment aux mahs parce qu'elles ont cru qu'elles pourraient y accéder par cette voie attirees par les publicités

http://www.les-mathematiques.net/phorum/read.php?3,1880072,1880116#msg-1880116

C'est assez vexant de profiter de mon droit d'écriture uniquement dans LF :-D Mais de bonne guerre. Par contre j'espère que ce n'est pas un manière détournée de contredire le fond car c'est pour toi que j'ai cherché des liens moi je m'en fiche un peu je connais tout ça.

Par contre je parlerais plutôt d'enjeux de CREDITS plutôt que de carrière. Les jeunes (Coquand, JBJ , etc, et la bande à cheval sur info théorique philo et th de la dem qui s'est faite financer à été repêchée par des mandarins qui n'avaient pas du tout d'enjeu. Pour le coup je peux t'assure de leur sincérité. Ils voulaient une armée et ont recruté, mais pas pour leur carrière. Ils ont pris les jeunes disponibles. Tant mieux. Mais le risque était effectivement la com, devenue élément fort chez la jeunesse.

Je suis encore sur mon téléphone donc il me sera difficile de rentrer dans les détails mais je pensais plus avoir répondu à tes questions qu' avoir été idéologue.

Après le côté plusieurs posts d'affilée provient du fait que je poste a des moments et éloignes et de mon téléphone j'aurais pu ne faire qu'un seul poste voir j'aurais pu te mettre un fichier texte joint.

De plus je mets c'est à l'art de la dictée sur mon téléphone avec correction des petites coquilles à la fin. je reconnais du coup que ça doit donner une impression un peu étrange bien que autant que possible j'essaie de ne laisser aucune faute.

Je me relirai pour appréhender la mauvaise impression que tu me signales que j'ai donnée. Mais pas tout de suite.