Que doivent faire les fondements ?

Merci pour le spoiling.

Bin, ça me donne l'occasion de ronchonner.

Le mot "fondement" est simple et peu problématique. Donc je suis contre sa démarche à cette dame.

Depuis des lustres, je propose que ce soit le mot "unification" beaucoup plus expert comme réceptacle de tels débats qui soit utilisé. En gros, cette dame écrit un livre que, si je l'avais écrit, on obtiendrait peut-être le même texte en tout point à ce ci près qu'avant la compilation, il aurait appliqué un "menu-edit-remplacre-fondement-by-unification"

Je rappelle que le fondement de la science théorique est invariable: prouver formellement tout ce qu'on dit, et laisser bien visibles les axiomes (ie les hypothèses faites, TOUT COMPRIS).

La suite n'est plus dans les fondements, mais dans les affaires pratiques de comment classer, répertorier, faire fructifier cette obligation. C'est d'autant plus important que nous travaillons tous dans des théories contradictoires, donc ce ne sont pas les conclusions (ce qui est prouvable) qui compte, mais les preuves elles-mêmes.

Et ça ne m'étonne pas que HoTT et le catégorisme soit déclaré comme n'ayant pas eu comme but initial d'être refondant par cette dame car effectivement on voit bien quand on papote et se dispute que c'est "revendicatif".

Or la recherche n'est pas revendicative.

Il est chaque fois d'ailleurs utile de rappeler que ZF(C) ne fonde rien du tout, puisque ZF** (enfin au choix des axiomes près, ie du bridage de la compréhension) EST le substrat dans lequel les gens s'expriment (all science et même all comprises), il n'y a donc pas de "sens" à prétendre le déloger (ce serait comme dire qu'on retire le vide d'une pièce pour y mettre quelques chose. Quand on met un truc, on remplit le vide, on ne le "déloge pas").

** j'entends par là le fait d'exécuter un $\forall x$ sur une collection et rien d'autre***.

*** ZF n'a rien fait d'autre que "forcer" les gens à assumer, ie s'ils remplacent les occurrences de $u_i\in x$ par $R(u_i)$, ils doivent le dire**** et pas le passer en catimini. Ce n'est pas un fondement, c'est une prise de conscience.

**** le choix conventionnel pour le dire est d'avoir "fait exister" $e:=\{y\mid R(y)\}$ et prétendre appliquer un truc vrai pour tout $x$ à $e$, mais ce n'est pas offensif ni profond.

Fonder veut dire "donner des règles de base explicites". Par exemple le jeu de go et le jeu d'échecs sont fondés.

Pour les maths n'importe quel système de règles de réécriture capturant toute la récursivité fournit un fondement acceptable (à défaut d'être pratique, mais ce dernier point appartient à une problématique distincte).

christophe c a écrit:

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

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

@Max: je vais lire, je l'ai d'ailleurs téléchargé (on dirait qu'il a été tapé à la machine à écrire)...

@Foys, je parle de la "vraie" théorie*** dans laquelle on travaille. ZF est une sorte de version polie, rien d eplus (dont on ne sait pas si elle est ou n'est pas consistante d'ailleurs)

***

$$ \forall R\exists a\forall x: [(x\in a) \iff (R(x))] $$

comme avec les dollars, je ne pouvais pas faire de smiley $<<$ :-D $>>$, je réécris sans :

Personnellement en tout cas, j'inverserais les mots: l'unification doit "se préoccuper" des fondements, en particulier les grumeaux restés trop en aval, pour bien unifier.

Mais j'en reste à fonder c'est expliquer à un enfant de 8ans la règle du jeu. Et donc poser la théorie originelle et attendre maturité pour différencier.

J'ai traficoté avec chrome pour en faire une traduction en français par google, que j'attache et vais maintenant lire (j'ai essayé de casser les paragraphes avec des sauts de lignes)

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

Je pense que dire "c'est l'ensemble des théorèmes qu'on peut déduire de ZFC" serait une réponse évidente mais trop simpliste. On ne peut pas rendre trop simpliste dans l'autre sens non plus, et dire que c'est toutes les déductions de la logique classique. Est-ce que "j'ai un chromosome Y, donc je suis presque sûrement un homme" c'est des maths ? Il y a des maths en dehors de la logique classique, il y a des maths en dehors de ZFC... mais du coup les maths c'est quoi ? Un ensemble de déductions faites à partir d'axiomes formels dans un langage logique formel ? Je suis sûr que vous trouverez encore quelque chose à critiquer à cette définition, c'est là tout l'intérêt de la chose. Mais si on prend ça comme définition, les fondements dont on a besoin sont clairs : il faut un langage logique, des règles de déduction, des axiomes logiques, des axiomes "pour démarrer les maths" et ainsi ne plus faire de la logique pure. Auquel cas n'importe quel théorème exprimé dans un certain langage formel, en utilisant les règles d'un système de logique donné, serait des mathématiques. Est-ce que c'est ça qu'on veut ? Moi, je ne sais pas. Je sais que ce que je fais, je veux que ce soit "des maths", mais décrire toutes les maths ? Au secours.

Personnellement, de toute façon, et je pense qu'on n'est pas encore sorti de cette époque archaïque, il est probable que les gens habitués à me lire sur le forum seront sous-pessimistes, qui consiste à rechercher la consistance en même temps que la contradiction. C'est de la shcizophrénie pure et simple!

1/ On veut des contradictions, ie des théorèmes, c'est à dire des garanties que tel et tel truc mène au paradis

2/ On veut le faire dans des théories qui ne sont pas contradictoires, autrement dit on veut "ne pas obtenir de contradictions"

Tant qu'on n'aura pas atteint l'époque où les scientifiques auront dépassé cette idiotie, on aura des débats stérils de ce genre.

3/ Je prends quelques exemples:

3.1/ l'auteure du texte déclare que ZF apporte beaucoup, que les recherches ont été approfondies et qu'on a fourni une mesure du risque à travers la consistency-strength des axiomes et théories.

3.2/ Très bien, mais si ZF est contradictoire, ça nous fait une belle jambe...

3.3/ Les obsédés du typage le considèrent comme "un gros truc" en termes de contraintes garantissant la consistance. A ça, deux commentaires:

3.3.1/ "Le gros truc" en question étant prouvé dans ZF (à la rigueur pour certains alinéas dans Peano :=ZF-) idem. C'est du vent. Par ailleurs, que se dépêche de faire quelqu'un qui type? Se placer en pensée "au dessus du truc" (autrement dit "détyper" :-D ) pour faire mieux que ses petits copains qui, s'lis ont le malheur de la jouer loyale et rester "dans le type" ne seront paa inspirés. On a à nouveau cette dualité "beurre et argent du beurre".

3.3.2/ La contrainte garantit bien évidemment un système beaucoup trop faible. Ca ne veut pas dire que c'est inintéressant, mais, c'est une spécialité très très spécifique (en gros, conscient que Brouwer et cie sont des équations diophantiennes expriment des trucs à pixels assez fins, MAIS EN NOMBRE FINI, le développement d'outils adaptés est une ambition tout à fait légitime, comme l'est le développement de programmes s'exécutant en temps polynomial et effectuant des trucs fins.

3.4/ Mais attention à ne pas faire comme en physique, un genre de "prise de pouvoir" sociologique qui stériliserait les choses et ralentirait énorménet la recherche, un peu comme En France la géométrie algébrique a occupé trop de place dans les Etats-majors recrutant.

4/ Un rappel me semble aussi profitable: en maths il y a réellement deux applications: l'optimisé pratique et le "par principe".

4.1/ PGCD(a,b), ce n'est pas PGCD(b,r :=reste ..), c'est PGCD(a-b,b).

4.2/ Si l'on veut OPTIMISER on remarquera qu'on peut DEVINER la suite de l'exécution et donc modifier le programme etça c'est une science difficile et appliquée qui ne mérite en aucun cas parfois le mépris qu'on lui inflige, MAIS C EST AUSSI SPECIFIQUE, c'est à dire qu'on ne peut pas faire que ça, et maintenir des définitions hybrides désorientantes au motif de s'embrasser à distance avec les appliquaurs.

4.3/ Pour ces même raisons, $p$ est premier quand for i:=2 to p-1 do if i | p then ExitWith "CRASH" else NeRienFaire done ne renvoie pas d'exception "crash" et non pas quand begin i:=2; while $i\times i\leq p$ do if i | p then ExitWith "CRASH" else i:=i+1 done n'en renvoie pas

5/ On peut multiplier à perte de vue les exemples où chaque boutique, avec ses préoccupations tente de préempter des choses et ça ne sert personne, car bien souvent complique à la fois la recherche mais aussi la transmission des acquis.

6/ De mon point de vue fonder n'est pas recherche la consistance d'une théorie, mais positionner un protocole EXTREMEMENT simple d'arbitrage des preuves qui puisse être très vite acquis par l'enfant.

7/ On oublie trop que c'est ce qu'a fait ZF (d'où toutes les maths exprimées dedans sans même que les gens s'en rendent compte), mais là encore, il faut être très clair, pas "ZF qui est vrai" (ça ne veut rien dire), mais "ZF qui est supposé" (c'est à dire en polarité négative) et en fait assez variable.

8/ A mon sens le reste est du blabla. De toute façon ce qui compte ce sont les preuves et non leurs conclusions et les chercheurs sérieux ont plutôt intérêt à connaitre les preuves des lemmes qu'ils manipulent je pense (sinon, on est devant de l'amateurisme Syracusien à la petite semaine, à s'amuser à tirer à la Kalachnikov pour voir la taille des trous dans le mur). Ce n'est pas parce qu'on va remplacer

$$a=b=c=d=\dots =w$$

par un chemin homotopique continu allant d'une entité bellement dessinée "a" vers l'entité idem "w" qu'on va faire avancer "les fondements", ce sont là des considérations relevant de la recherche aguerrie et des experts, tout comme les histoires de consitency-strength.

Merci, je n'y avais pas pensé, et pourtant je fais couramment du tex->txt pour poster ici.
Inutile donc de perdre du temps, j'ai récupéré ce texte mais j'ignore si je vais y comprendre quelque chose.
Bon courage.

Je vais essayer de compléter ce que j'ai dit au dessus avec quelques exemples "typiques" qui invalident les slogans usuels qu'on prononce pour affirmer des oppositions entre bords.

1.1/ L'axiome du choix serait un anti-constructif objet.

1.2/ Non, dans bien des cas, il permet au contraire des raccourcis qui ne seraient pas permis sans, et donne des existences effectives là on il faudrait taffer pour en trouver. Les groupes de tresses de Dehornoy (certes utilisant AUSSi d'autres ingréients mais pas plus consrtuctifs), le théorème des zéros de Hilbert où Zorn etc, donne directement une solution, etc.

2.1/ Les théories contradictoires sont non constructives.

2.2/ C'est tout l'opposé, elles permettent parfois des constructions auxquels les gens n'auraient pas pensé spontanément. L'énoncé $\forall f\exists x: f(x)=x$ peut donner l'impression qu'on aura du mal à trouver un point fixe, alors qu'avec $e: x\mapsto f(x(x))$, vous avez immédiatement un point fixe parfaitement effectif avec $e(e)$. Ne pas confondre son caractère DEPLAISANT avec son caractère non constructif: certes on en voudrait un autre, mais on a celui-là

3.1/ Un preuve prouvant l'existence d'un objet est généralement capable de produire une preuve constructive qui va l'exhiber.

3.2/ Non!! Ce n'est pas vrai que pour les théories extrêmement faibles et "triviales" (non pas pour l'humain, mais à supposer qu'on dispose d'autant de temps qu'on veut). Evidemment qu'un théorème d'arithmétique se dépliera (en temps long tout de même) en exhibition de l'objet du fait qu'on "essentiellement" identifié $\epsilon_0$ comme la sup de la puissance arithmétique. En pratique, cependant, l'algorithme est hyperexponentiel.

Mais surtout, ça procède d'un très mauvaise vision des maths, et d'ailleurs c'est rigolo, souvent perçue trop platoniquement par ceux-là même qui critique le platonisme. Par exemple, il n'y a pas d'entiers, mais pour ceux-là, qui ont tendance à croire qu'il y en a, ils n'ont pas conscience que les preuves d'existence peuvent être obtenues de façon telles qu'on attestera seulement l'existence de l'objet dans tout univers vérifiant les axiomes. Or les entiers n'existent pas, seuls existent les entiers de l'univers truc, et ça dépend irrémédiablement de Truc.

3.3/ Un exemple simple: soit $(P>Q) :=$ il existe une preuve $r$ dans ZFC que $P\to (\exists Inaccessible(E): E\models Q)$. Soit $T$ l'ensemble des $P$ tels qu'il n'existe pas de suite $P_0:=P>P_1>P_2>..$ infinie descendante.

Intuitivement on pourrait croire que si l'univers est "bien fait" et assez gros, il existe un inaccessible $E$ tel que $\forall P\in T: E\models P$. C'est un exercice basique de 2 lignes de prouver que non. Il existe donc $P\in T$ tel qu'aucun inaccessiible (donc a priori aucun univers aussi gros soit-il) ne $\models P$.

Quel est ce $P$ dont on vient d'otenir l'existence en 2 lignes?

4.1/ C'est la frontière classique / intuitionniste qui joue un grand rôle.

4.2/ Absolument pas. Le raisonnement par l'absurde n'ajoute strictement rien de plus que ce qu'on appelle en informatique une procédure d'interruption des fins de boucles inutiles.

Exemple:
begin a:= true ; for i := 2 to p-1 do if i divise p then a:= false else Nop done return a end
est améliorée par

f(p):= begin a:= true ; for i := 2 to p-1 do if i divise p then begin a:= false; Stop(i) end else Nop done return a end
g(p) := try f(p) EnCasDeStop(x): renvoyer x

4.3/ Il en va très exactement de même de l'axiome ((A=>faux)=>faux)=>A: en effet partant d'une preuve qui supposant (A=>faux) conclut faux, vous la parsez pour trouver où vous utilisez l'hypothèse A=>faux.

4.3.1/ Si vous ne l'utilisez pas, c'est que vos autres hypothèses sont contradictoires.

4.3.2/ Si vous l'utilisez,

4.3.2.1/ ou bien vous fournissez à l'hypothèse (A=>faux) une garantie construite précédemment de A. Il vous suffit alors de récupérer cette garantie

4.3.2.2/ (délégation) ou bien vous utilisez quelque part que (A=>faux)=>B dont vous retrouvez en conclusion de quel hypothèse explicite il est de façon à le rendre redondant.

4.4/ De manière générale, c'est juste la possibilité d'interrompre (et heureusement qu'on peut) AVANT un calcul de $f(x)$ l'exécution d'une garantie afin de prendre connaissance de $x$. Tout bêtement, ça répare l'oubli de la non commutativité de $(f,a)\mapsto f(a)$ qui a donné lieu, dans un premier temps "un peu naif" à l'idée qu'on ne pouvait pas "piquer" son argument à $f$.

4.2/ Le VRAI PROBLEME est la capacité de dupliquer des ressources, choses qui n'a strictement pas de parenté avec la vraie vie.

4.2.1/ Dans un exemple où Anatole m'a prouvé en 5mn que tout anneau tel que $\forall x\exists n>1: x^n=x$ est commutatif, il a réutilisé au moins 2 ou 3 fois l'hypothèse PRINCIPALE

4.2.2/ Quand vous prouvez qu'il n'y a pas de surjection de $E$ sur $P(E)$, vous réutilisez DEUX FOIS de manière absolument irréductible l'hypothèse, ie de $f(a)=\{x\mid x\in f(x) \to Paradis\}$, vous déduisez:

$a\in f(a)\to ( a\in f(a) \to Paradis)$ donc

$[a\in f(a) $ ET $a\in f(a)] \to Paradis$

donc EN ADMETTANT que $a\in f(a) $ implique $[a\in f(a) $ ET $a\in f(a)]$

$a\in a \to Paradis$

Et c'est pas fini. De là, vous avez seulement obtenu $a\in f(a)$. Qu'il va falloir recloner pour gagner le paradis.

4.2.3/ Quand vous prouvez que $9$ est un nombre entier fini, vous devez CLONER 9 fois vos axiomes.

5/ Je compléterai, voilà, je pense avoir évoqué quelques points peu , enfin trop peu engagés dans les débats "politiques", mais qui sont techniquement les plus importants.

christophe c a écrit:

2.2/ C'est tout l'opposé, elles permettent parfois des constructions auxquels les gens n'auraient pas pensé spontanément. L'énoncé $\forall f \exists x:f(x)=x$ peut donner l'impression qu'on aura du mal à trouver un point fixe, alors qu'avec $e: x \mapsto f(x(x))$, vous avez immédiatement un point fixe parfaitement effectif avec e(e)$e(e)$. Ne pas confondre son caractère DEPLAISANT avec son caractère non constructif: certes on en voudrait un autre, mais on a celui-là

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

christophe c a écrit:

Ne pas confondre son caractère DEPLAISANT avec son caractère non constructif

Ce qui est déplaisant est cette manie de forcer la main des gens sans preuve, en les accusant d'avoir peur ou d'être faibles.
Et faut arrêter de prétendre que les gens sont en désaccord par faiblesse psychologique. Le vrai monde N'EST PAS CONTRADICTOIRE (y a pas d'éléphant rose qui apparaît devant moi en une fraction de seconde). Donc on a besoin d'outils FIABLES c'est-à-dire NON CONTRADICTOIRES pour l'explorer (les résultats qui établissent la très grande difficulté à s'assurer de ça sinon son impossibilité et a maintenir un système décemment expressif ne modifient pas ce besoin; les développeurs de la NASA envoient dans l'espace des objets à plusieurs centaines de millions de dollars: ils ont des restrictions draconniennes sur le contenu de leus programmes interdisant la Turing-complétude notamment: est-ce de la puérilité? ).

3.1/ J'ai lu que Coquand dit que ce qui est emmerdant, c'est la démo par l'absurde.
Je soupçonne d'ailleurs que la correspondance démo-programme c'est un truc satellitaire de l'absurde.

xax a écrit:

3.1/ J'ai lu que Coquand dit que ce qui est emmerdant, c'est la démo par l'absurde.
Je soupçonne d'ailleurs que la correspondance démo-programme c'est un truc satellitaire de l'absurde.

Il y a des solutions ad-hoc (Diaconescu, mais on suppose donnés des mécanismes encore moins constructifs comme l'axiome du choix) ou des nnouveaux paradigmes comme la réalisabilité classique.

Oui, en gros dans ZFC par exemple, on part du fait que pour tous $x,y \in \{0,1\}$, il est intuitionnistiquement prouvable que $x=y$ ou $x\neq y$ (*)(car un objet $u$ appartient par définition à $\{0,1\}$ si et seulement si $u=0$ ou $u=1$ puis on distingue les cas $x=y=0$, $x=1$ et $y=0$, $x=0$ et $y=1$ et $x=y=1$).
Noter aussi que "$a\neq b$" abrège $\neg (a=b)$ qui lui-même abrège $(a=b)\Rightarrow\perp$ (**)

Ensuite on prend $F$ un énoncé quelconque (dans lequel la lettre $x$ n'est pas libre) et $\varphi$ une fonction de choix de $\{0,1\}$, i.e. une fonction telle que pour toute partie non vide $X$ de $\{0,1\}$, $X\in dom(\varphi)$ et $\varphi(X)\in X$. Posons $A:=\left \{x \in \{0,1\} \mid x=0 \Rightarrow F \right \}$ et $B:=\left \{x \in \{0,1\} \mid x=1 \Rightarrow F \right \}$. On a $1\in A$ et $0\in B$ donc $A$ et $B$ sont non vides, posons $a:=\varphi(A) \in A$ et $b:=\varphi(B) \in B$.
On exploite (*).
Si $a=b$ alors comme $a\in \{0,1\}$, $a=0$ ou $a=1$. Si $a=0$, on a $F$ car $a\in A$ (cf définition de $A$) et si $a=1$, $a=b\in B$ donc on a a nouveau $F$.
Si $a\neq b$ (a.k.a. $a=b \Rightarrow \perp$ d'après (**) ): supposons $F$. Alors pour tous $x\in \{0,1\}$, $F$ et donc aussi $x=0\Rightarrow F$ et $x=1\Rightarrow F$ sont satisfaites. Donc par extensionnalité, $A=B=\{0,1\}$. Donc $a=b$. Donc
$\perp$. Donc au final, $a\neq b$ entraîne $F\Rightarrow \perp$.

Finalement on a montré $F \vee (F\Rightarrow \perp)$ ce qui est le tiers exclu..

foys a écrit:

Donc [large]on a besoin d'outils FIABLES c'est-à-dire NON CONTRADICTOIRES[/large] pour l'explorer (les résultats qui établissent la très grande difficulté à s'assurer de ça sinon son impossibilité et a maintenir un système décemment expressif ne modifient pas ce besoin; les développeurs de la NASA envoient dans l'espace des objets à plusieurs centaines de millions de dollars: ils ont des restrictions draconniennes sur le contenu de leus programmes interdisant la Turing-complétude notamment: est-ce de la puérilité?

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

Je suis sérieux. Je ne conteste ps ce que tu dis, en rien. Mais je ne vois pas où est le problème. Et après avoir parlé de la vocation non opératoire de la science pour justifier qu'on ait rejeté le LC (ie opposition platonisme / opératoire), tu le ré-évoques pour justifier qu'on a besoin de fiabilité: j'ai du mal à te suivre.

C'est bien pour ça que j'insiste sur le sérieux et la compétence de fond sur ces problèmes et condamne (sans vouloir traiter de faible ou de peureux, comme tu le dis, pardon si la forme stytlistique que j'utilise en donne l'impression) les modes de s'évanouir face à $A:=non(A)$.

J'ai l'impression que tu es entre les deux. Si tu me dis qu'on se restreint au polynomial (ou légèrement plus) pour éviter les non tes terminaisons non voulues d'algorithme, ce n'est vraiment pas moi qui vais te contredire puisqu'au contraire, je n'ai fait que l'expliciter et ranger ça sous le statut de spécialité. J'ai l'impression que sous le prétexte que je dis que les spécialistes du sécurisable (ie du taf dans les théories faibles) forment UNE PARTIE seulement de la science, tu m'accuses de vouloir les rabaisser. Pas du tout!!! Ce que je dis est qu'il ne sont pas spécialisés dans les autres domaines, plus platoniciens, voire, pour certains domaines, à la limite de l'ambition de frôler la folie via tentative de "toucher" à Dieu (enfin l'espèce de Dieu de l'infini si tu préfères), où là, disons-le, et tu sais que je les respecte puisque ce sont mes pairs, la prétention de sécurité est tout sauf élevée.

J'avoue même être un peu étonné de ton gout pour le sécurisé, le typage et COQ, je t'aurais vu plus platonicien, pluss à flirter avec les gens qui veulent aller papoter avec woodin ou Solovay, mais in fine, je m'aperçois que j'avais un préjugé gratuit, car il est tout à fait vrai que tu ne montrais pas de signes spécialement "platoniste", et que c'est vers la CCH que tu t'es formé récemment (moi, la voyant comme une opportunité de purisme expressif, et adapté à étudier les théories contradictoires, j'ai involontairement projeté ça sur l'idée que j'avais de tes gouts, mais maintenant il me revient qu'effectivement tu interviens souvent en "contre-magie" si j'ose dire.

T'inquiète, j'y pense, j'ai commencé rédiger un article, où j'intègre:

1/ Preuve de la conservativité de l'ajout d'un symbole opérant le choix non extensionnel au dessus de ZF+CD (je veux rester discret, car ça fait 10 lignes et la première partie des longues recherche d'un ami (JLKrivine) qui s'est "trompé" en préjugeant que ça devait peut-être un peu difficile te donc a "grillé" de la réalisabilité dessus

2/ plusieurs pages pour traduire ce que m'a pporté alesha

3/ Probablement plusieurs pages de discussions philo-technique pour tenter d'établir un peu un résumé de mes "validations définitives de position" d'avant (j'ai un peu avancé récemment avec le confinement, mais ça reste encore instable, je ne viens seulement que de découvrir que $)a=b) = -(b=a)$, je ne vais pas l'y inclure.

Ca devrait être prêt et sur HAL avant fin juin vu que c'est récréatif chez moi, pas une obligation corvéeuse que je me fais. J'y réintègrerai ta correction sur les anneaux d'alileurs

@foys et xax, comme je viens de le dire à Max, là encore c'est "une erreur" de percevoir l'axiome du choix comme le héros de la réalisation du RPA. Mais bien plus fréquentes et graves sont les erreurs de Coquand et de toute la communauté qui fait de la CCH sans avoir de connaissance en TDE (on a LC = TDE, et bien des erreurs sont commises par déportation destinée à créer des oppositions artificielles d'ailleurs)

Le génis de la lampe d'Aladin dans cette affaire, c'est l'axiome d'extensionalité. L'axiome du choix n'y joue un rôle qu'à peu près nul et "notationnel".

Foys aurait donc dû écrire:

[small]supposons F. Alors pour tous blabla et donc aussi blabla sont satisfaites.[/small] [size=x-large]Donc par extensionnalité[/size][small] blabla. Donc a=b. Donc blabla. Donc au final, blabla entraîne blabla[/small]

et non pas

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

En fait, l'axiome d'extensionalité est "essentiellement" faux, et presque prouvablement, c'est de cet ADN qu'on a tiré sa puissance. LE RPA,lui, par contre, n'est rien, je l'ai un peu détaillé au post de ce matin. Quand à la TDE, déjà, c'est un peu "étrange" et artificiel d'y prouver le RPA, car il est en fait impliqué (ce sera la partie de mon article from Alesha) (ie DEDUCTIBLE) de la TDE, même intuitionniste.

L'intuitionnisme trouve sa fondation dans une assymétrie infligée aux phrases. Elle étudie le positionnement d'un joueur opposé à un n=unique adversaire, mais qui a le droit de dupliquer autant qu'il veut ses copies de lui-même. Ce n'est pas "une logique" au sens où en fait, on voudrait l'entendre, c'est plutôt un protocole asymétrisant certains contextes pour les adapter à ce qu'on veut.

Le RPA n'y est pas faux, il est caché sous l’asymétrie. Pas plus que tu ne peux inverser une application BILINEAIRE allant de $(E^*) \times (E^*)$ dans $\R$, tu ne peux récupérer $A$ à partir d'une preuve de $(A\to Tout)\to ((A\to Tout) \to Tout)$, car tu as "au moins" deux endroits où tu as utilisé l'hypothèse $A\to Tout$. La seule chose que tu peux récupérer mais la logique intuitionniste ne l'implémente pas c'est une sorte de "superposition quantique" entre deux objets différents (et possiblement très différents) qui, dans le passé, ont habité $A$, et ça n'avance pas beaucoup.

Dans l'argument que t'a signalé foys, la fonction choix (a priori pas méchante :-D ) $f$ est interdite de choisir $f(A)\neq f(B)$ quand $A\subset B$ et $B\subset A$ et c'est l'axiome d'extensionalité qui l'exige, ce n'est pas du tout un problème de difficulté de choisir un élément dans $A$ ainsi qu'un élément dans $B$, c'est un problème de "faire semblant de pas savoir que ces deux ensembles sont réclamés égaux par l'extensionalité, alors qu'à l'évidence ils sont différents (ils se comportent juste de la même manière au regard de qui ils acceptent d'être appelés leurs éléments).

Il n'y a pas d'opposition technique entre nous, je crois surtout que je n'avais "pas vu" (du fait de sa maitrise de l'infinitisme et des autoréférences, plus affichée que d'autres experts du forum) juste qu'il "préfère" l'encadrement par des règles de garanties de consistance assez basse, et le fait qu'il ait acquis le lambda-calcul ici même (enfin pendant la période où il venait AUSSI ici en parler) m'a induit en erreur sur son intention de s'envoyer des gros kiffs à coups de points fixes itérés. Peronnellement, tu me proposes un terme fortement normalisable***, je pars en disant "non merci", et j'ai un peu trop appliqué ça à mon camarade en face qui lui les aime, je pense, c'est tout.

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

Foys a écrit:

Pour ta remarque sur le fait que c'est "faux", je pense que l'extensionnalité fait partie de l'identité des théories des ensembles

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

$$[(A\subset \ et\ (B\subset A)\ et\ (A\in X)] \to (B\in X)$$

(il n'y a pas de égal en TDE)

C'est extrêmement fort, car ça dit qu'un X pour décider si A lui appartient ou pas, non pas connait A (ça l'induirait en erreur), mais uniquement les éléments de $A$. (Un peu comme si un appel informatique $f(g)$ ne pouvait s'exécuter qu'après que $f$ ait visité tous les $g(h)$, afin non pas de connaitre $g$, mais de connaitre son comportement).

Ca n'a pas loupé :-D dans des recherches comme celles de Krivine par exemple, ça s'est avéré un appel au père Noel tellement exorbitant qu'il a fini par mener à des "contradictions intra-paradigmatiques")

Il est à noter aussi que le tiers exclus et l'axiome du choix sont EQUIVALENTS** (sur le fond) VIA l'axiome d'extensionnalité, ce qui ne le rend pas inintéressant puisqu'il "met le doigt là où ça fait mal". Mais il est trop fort, il a tendance à envoyer sur $0=1$ toute hypothèse un peu fine.

** tu n'as signalé qu'un des deux sens, le médiatique à cause du boucan années 2000 des catégoriciens, mais l'autre est en fait le plus significatif car s'exécute avec $J$ (ie le combinateur tel que $\forall x: Jx:=x$, pardon pour mes notations), via :

$$A(E):=\{x\mid x\in Ordinaux\ et\ NoSurjectionDeSur(x,E)\}$$

On peut faire de la CCH dans les catégories cartésiennes fermées, ça permet de retirer l'aspect "machine" qui n'est pas une nécessité. On peut faire ça dans des catégories plus générales (ex: monoïdales symétriques) pour récupérer la logique linéaire (un fragment en tout cas).

Pour les lecteurs qui ne viendraient pas ici par le fil auquel j'ai réagi je mets ce lien vers l'explication très concise de GBZM: http://www.les-mathematiques.net/phorum/read.php?9,2017604,2018360#msg-2018360

C'est lui qui m'avait fait remarquer que la topologie servait parfaitement de sémantique pour la logique intuitionniste. Je ne le savais pas avant.

Un lancé de fleurs en ce vendredi ensoleillé :

Maxtimax a écrit:

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

CC a écrit:

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

B-)-

CC a écrit:

et le confinement m'a fait prendre des kilos

mais tu n'avais pas déjà un problème de "foie gras" cc ?