Introduction claire au fondements des maths
Bonjour,
Je souhaiterais étudier les fondements des mathématiques mais j’ai du mal à trouver des sources qui me conviennent. En cherchant sur le forum j’ai pu voir quelques suggestions et en regardant ces livres il y avait toujours le même problème : il y a des notions qui ne sont pas clairement définies.
Par exemple, le livre de Jean-Louis Krivine rien qu’au début on parle d’univers en disant que ce ne sont pas des ensembles sans même définir ce qu’est un univers (on dit juste que c’est une collection), pour les autres ouvrages j’ai rencontré le même type de problème (par exemple dans le premier tome de René Cori on parle directement d’ensembles et on définit à partir d’eux les formules etc ...)
C’est assez perturbant, pour l’instant le seul ouvrage qui m’ai satisfait du point de vue fondement c’est celui de Bourbaki théorie des ensembles, là j’avais vraiment senti que les choses démarraient de zéro et c’était assez agréable à lire, mais en voyant que beaucoup de personnes disaient que la construction de Bourbaki est très mauvaise d’un point de vue logique (le tau serait problématique) alors je n’ai pas voulu finir de l’étudier.
Du coup voilà, j’ai vraiment envie de reprendre les mathématiques des fondements mais vraiment vraiment les fondements, tout absolument de zéro, et surtout avec des définitions rigoureuses au maximum, du coup j’aimerais beaucoup que vous me conseillez des sources s’il vous plaît.
Merci par avance
Je souhaiterais étudier les fondements des mathématiques mais j’ai du mal à trouver des sources qui me conviennent. En cherchant sur le forum j’ai pu voir quelques suggestions et en regardant ces livres il y avait toujours le même problème : il y a des notions qui ne sont pas clairement définies.
Par exemple, le livre de Jean-Louis Krivine rien qu’au début on parle d’univers en disant que ce ne sont pas des ensembles sans même définir ce qu’est un univers (on dit juste que c’est une collection), pour les autres ouvrages j’ai rencontré le même type de problème (par exemple dans le premier tome de René Cori on parle directement d’ensembles et on définit à partir d’eux les formules etc ...)
C’est assez perturbant, pour l’instant le seul ouvrage qui m’ai satisfait du point de vue fondement c’est celui de Bourbaki théorie des ensembles, là j’avais vraiment senti que les choses démarraient de zéro et c’était assez agréable à lire, mais en voyant que beaucoup de personnes disaient que la construction de Bourbaki est très mauvaise d’un point de vue logique (le tau serait problématique) alors je n’ai pas voulu finir de l’étudier.
Du coup voilà, j’ai vraiment envie de reprendre les mathématiques des fondements mais vraiment vraiment les fondements, tout absolument de zéro, et surtout avec des définitions rigoureuses au maximum, du coup j’aimerais beaucoup que vous me conseillez des sources s’il vous plaît.
Merci par avance
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Sans ça, tu ne peux même pas poser ton stylo sur le papier pour écrire : ça devient compliqué de faire des maths :-D
Ainsi le mieux que tu peux espérer c'est partir de quelque chose qui ressemble à une syntaxe avec une "méta-récurrence" que tu dois admettre. Il me semble que le Cori et Lascar commence un peu ainsi (dans les rappels de début ils parlent de ce qu'ils admettent sur la syntaxe si je me souviens bien). Une fois cela acquis, tu peux voir tout le reste comme se passant "à l'intérieur" de la syntaxe, et donc il n'y a pas de problème puisque tu n'as pas à définir "ensemble" : n'est-ce pas merveilleux ?
Dans tous les cas tu ne trouveras pas de référence qui te définit ce qu'est un ensemble, puisque c'est une sorte de notion première. Sous les axiomes de ZF(C) il s'agit juste des objets que l'on manipule. En un sens, "tout est ensemble". J'insiste sur le fait qu'il s'agit du point de vue ZF, et que ce n'est pas la seule manière de fournir des fondements aux maths, même si c'est historiquement celle qui a remporté une sorte de consensus chez les mathématiciens.
Quand on définit une opération syntaxique par récurrence on parle de ce qui est faisable à la main étapes par étapes.
G.Dowek: Les démonstrations et les algorithmes.
Pour un point de vue non français: les livres de R.Smullyan (First order logic; Logical labyrinths; Mocking a mockingbird -pour un sujet moins minimaliste qu'il n'y paraît: la logique combinatoire).
-Il se sert d'indices de Bruijn sans le dire (au lieu d'avoir des nombres indiquant l'adresse du lieur à la place des variables liées, il a recours à des traits physiques. C'est moche mais ça marche). Ainsi il se débarrasse complètement de la corvée consistant à traiter l'alpha-équivalence
-Le symbole tau (à l'origine epsilon, introduit par Hilbert) a fait couler beaucoup d'encre. Une remarque au passage. Les systèmes d'axiomes des maths assumés comme tels (Peano,ZF(C)) sont limités en constantes et symboles de fonction, plus précisément:
-dans PA il y a $1,0$, $+$ et $\times$.
-dans ZF et ses variantes il n'y en a aucun.
Ainsi, un énoncé comme "Pour toutes fonctions continues $f,g$ de $[0,1]$ dans $[0,1]$ qui commutent, il existe $x\in [0,1]$ tel que $f(x)=g(x)$" n'est pas un énoncé de ZFC.
L'introduction de nouveaux noms $1,2,3, \R, ...$ est pris en charge par la règle d'élimination du quantificateur $\exists$, certes, mais pour des fonctions, il y a seulement des résultats de théorie des modèles assez lourdingues (on peut montrer via le théorème de complétude que si $P$ est un énoncé clos du premier ordre sans occurence du symbole de fonction $f$ et $R(x,y)$ un énoncé à deux variables libres $x,y$ que si $\left (\forall xR\left (x,f(x) \right) \right ) \Rightarrow P$ est démontrable, alors $\left (\forall x \exists yR(x,y) \right ) \Rightarrow P$ est également démontrable).
Dans les présentations usuelles on vous laisse vous faire vous même à l'idée que vous pouvez manipuler librement tous les symboles de fonctions (et il faut bien reconnaître que sans pouvoir parler de fonctions, on ne risque pas de faire beaucoup de maths...) que vous voulez mais on ne vous dit jamais pourquoi.
Las! l'auteur génial du "Théorie des ensembles" bourbakiste a court-circuité le problème en décidant que "f(x)" serait une abréviation d'un truc complexe écrit avec tau, mais défini explictement.
Ainsi le traité bourbakiste tient vraiment ses promesses: construire from scratch et tout dire.
Il y a bien des critiques légitimes à lui adresser:
-il est inutilisable pour traiter les catégories (déjà pourtant bien établies quand l'édition la plus récente du livre est parue: en 1970).
-les fondements exposés sont différents de ceux plus habtuels comme ZF(C) (présence d'un axiome du choix global notamment).
-la lecture est franchement pénible -en fait le livre de fondements accessible que ModuleLibre semble appeler de ses voeux n'existe pas (pas encore?).
-impossibilité physique d'implémenter la construction bourbakiste (les termes mathématiques les plus simples dépassent allègrement les $10^{50}$ caractères: la faute revient au symbole $\tau$: il y a des articles qui traînent sur le web qui parlent de ça).
En tout cas les problèmes ne viennent certainement pas d'une prétendue "impossibilité" à formaliser complètement les mathématiques. Ca c'est un vieux cliché répété par habitude.
(NB: il ne faut pas confondre "tout formaliser" avec "ne rien admettre", ou "prouver ou réfuter toutes les affirmations": formaliser consiste à expliciter tous les admis et règles du jeu).
(Je ne dis pas qu'il y faudrait une définition de "succession", attention ! j'ai abandonné mes rêves fondateurs il y a un moment. Simplement ne prétendons pas pouvoir tout formaliser)
Je suis peut-être à côté de la plaque, il est possible que ModuleLibre me soit déjà largement supérieur. J'étais à zéro dans le domaine il y a quelques mois (et je reste à peu près au niveau débutant, mais je n'ai pas besoin d'être bon), et je ne partage donc qu'une expérience "d'apprenant". J'ai emprunté ce livre-là dans une bibliothèque en ai potassé quelques chapitres (surtout le premier, sur les règles de logique), mais je ne suis pas certain que ce soit un très bon bouquin, j'ai notamment été assez choqué par le fait qu'on parle d'arité des fonctions et formules avant qu'on soit capable de dire ce qu'est un nombre, mais je suppose que c'est normal, le pire était l'usage d'induction dans la démonstration du théorème de complétude, ça me donne plutôt l'impression que ZFC prouve le théorème de complétude plutôt que ça se tienne en soi, mais bon, perso, je n'approfondirai pas...).
Et plus tard, ai pioché à droite et à gauche (surtout sur le net) pour approfondir ZFC (pas allé loin, surtout ce qui concerne les machins de graphes et de structures, parce que ça me donne l'impression d'avoir des outils plus généraux, les théorèmes de bases sur les cardinaux, puis des trucs sur les raisonnement par induction suite à un tour sur ce forum), je crois que le fait d'avoir déjà une notion formelle de langage et de démonstration m'a aidé à aller assez vite dans ce domaine (sachant que je ne suis pas une flèche, mais que j'apprécie assez une certaine rigueur).
C'est bizarre cette remarque! Ne voulais-tu pas dire que Bourbaki NE TRAITE PAS le chapitre "catégories" plutôt? Il n'y a pas que les catégories, je crois que Bourbaki omet un certain nombre de chapitre des maths, ce n'est quand-même pas "étonnant".
J'explique vite fait pourquoi aux amateurs. Pour dire par exemple $\exists xR(x)$, on dit $R(\lambda xR(x))$, ce qui double d'un coup (répétition deux fois de R de quelque chose)
Bourbaki est très bien, comme le signale foys (j'en suis la preuve vivante, puisque les seules maths que j'ai apprise avant 30ans, en gros c'est dedans), mais beaucoup trop compliqué. Ce n'est pas un reproche, vue l'époque lointaine d'écriture.
Il n'y a pas d'alternative (JLKrivine pourrait l'être, mais il ne s'est volontairement pas adressé aux mêmes lecteurs, donc passe sous silence pas mal de choses), car ça ne se vendrait pas "assez vite".
Cependant je peux te former (1000 fois mieux que n'importe quel livre, avec un texte 10 fois plus court, mais interactif) par le forum, ModuleLibre, mais j'ai besoin de savoir plus de choses sur tes motivations, où tu veux aller avec ça et quel est le NIVEAU de tes motivations (au sens: quel investissement en efforts et tortures es-tu prêt à miser?)
@christophe c je vous remercie infiniment ! Je suis actuellement en première année en école d’ingénieur (après deux années de classes préparatoires), j’ai le niveau d’un étudiant en L3 mathématique (j’ai étudié le programme en autodidacte avec des pdf et des livres que j’ai trouvés).
Mes connaissances en logique se limitent aux bases de la construction de Bourbaki (j’ai étudié les Bourbaki jusqu’aux théories égalitaires) ainsi qu’à quelques notions que j’ai vues par-ci par-là pendant mes études de maths (par exemple quand Roger Godement parle de relations indécidables etc ...)
Quant à ma motivation, j’ai l’impression que la logique est l’étude du squelette des mathématiques, quelque chose qui permet de voir la structure même de la mathématique, et cela m’intéresse beaucoup !
Pour les efforts que je suis prêt à déployer, j’ai décidé de vouer ma vie à la science (bien sûr je ne peux pas savoir comment ma vision de la science va évoluer, mais pour l’instant c’est ce que je veux). Pas qu’aux mathématiques, mais vraiment à toutes les sciences, je veux apprendre tout ce qui m’intéresse, et la logique est une discipline qui m’intéresse énormément (principalement parce que pour une fois, j’avais l’impression que tout était très clair, des notions limpides, des choses qui démarrent vraiment de zéro, contrairement à d’autres disciplines comme la physique où rien n’est clair et défini --du moins de ce que j’ai vu jusque là--, mais ça ne veut pas dire que je n’aime pas physique au contraire, c’est juste ce point là qui me dérange).
Pour être plus précis pour les efforts, puisque j’ai mes cours d’ingénieur aussi et les révisions alors je ne fais que 3h de mathématiques par jour en moyenne. En ce moment je n’ai pas cours donc j’en profite pour faire des mathématiques toute la journée.
Par contre, oublie Bourbaki afin de ne pas être tenté de faire des rapprochements dans un premier temps.
Il faudrait aussi que tu me précises si tu préfères que l'objet primitif soit "les ensembles" ou que ce soit "les fonctions". Ca ne change rien, ce sont les mêmes fondements, mais ça change comment je vais manipuler latex pour t'initier.
Je te signale juste 2 avantages:
1/ Pour les ensembles, l'avantage est que ça permet de poser une fois pour toute comme convention que l'objet textuel primordial est la phrase (autrement dit, l'auteur est considéré comme affirmant des phrases). L'inconvénient est que lieur** abrégeant est un peu exotique, puisqu'on ouvre une accolade, on utilise une barre verticale et on ferme l'accolade
2/ Pour les fonctions, l'avantage est que le lieur ** universel abrégeant est "bien connu" et unique. L'inconvénient est qu'on n'a pas de convention spécifique pour les expressions, ie, ce ne sont pas forcément des phrases, donc il y a une "petite galère" de disposition.
Il serait bien que tu choisisses (mais de toute façon tout en amont, aux fondements des fondements si tu préfères, je vais prendre (2), avant, si tu le demandes de bifurquer vers (1) assez vite.
[size=x-large]**[/size]
[small]Ensemblistement:
$$\{x\mid x^2 = 37\}$$
Fonctionnellement:
$$(x\mapsto (x^2=37))$$[/small]
Et encore merci infiniment
Je commence.
Exercice1: soit $Z$ un ensemble (appelé ensemble de tout ce qui existe :-D de manière purement arbitraire). On suppose qu'il est doté d'une relation transitive, notée $<$ et d'une application de $Z^2$ dans $Z$, que je vais noter au début $*$, mais ensuite par un simple espace. En outre, $a*b*c$ signifiera $(a*b)*c$. On fixe définitivement dans $Z$ les éléments suivants: $C,K,W,J$ et on suppose les choses suivantes:
$\forall x,y,z$ dans $Z: $
1/ $((C*x)*y)*z < y*(x*z)$
2/ $(K*x)*y < x$
3/ $(W*x)*y < (x*y)*y$
4/ $J*x < x$
5/ si $x<y$ alors $[x*z<y*z$ et $z*x<z*y]$
Prouver qu'il existe dans $Z$ un élément $B$ tel que : $\forall x,y: (B*x)*y < y*x$
Edit: merci à Pierre Cap!! J'avais oublié le point 5 avec la canicule
1°) Quelles sont les règles relatives à $J$?.
2°) On se place sur le magma libre sur $\{C,W,J,K\} \cup L$ où $L$ est un ensemble de lettres. On garde les règles de réduction ci-dessus. On définit pour tout terme $t$ la lettre la plus à droite de $t$ par $\delta(x):=x$ si $t$ est la lettre $x$ et $\delta(ab):=\delta(b)$ si $t=ab$.
Alors $\delta$ est constante au cours des réductions qui utilisent uniquement les règles relatives à $C,W$ (et $J$ si $J*x<x$ pour tout $x$ mais est-ce ça?).
Ca veut dire que la construction de $B$ utilise au moins un $K$, je ne sais pas si c'est voulu mais bon.
J'ai édité mon post bleu et ajouté, et évidemment qu'il y a compatibilité, à l'edit j'ai ajouté le point5
Bien entendu, il y a des boucles, mais on obtient une fluidité substantielle. Elle est d'ailleurs parfaitement traductible dans $ZF$, via $a:=\{x\mid (R(u)\to x\in v)$ et $(R(u)$ ou $x\in u)\}$ qui lui aussi vaut:
$$if \ R(u)\ then \ v\ else\ u $$
Je pense cerner ton objection (tu me corrigeras si je me trompe): les diverses formes de récurrence/construction par induction qui sont utilisées en maths ne pourraient être justifiées que par un raisonnement circulaire (les propriétés des objets syntaxiques eux-mêmes n'étant prises en charge que via une "méta induction" mystérieuse elle-même injustifiable voire carrément indéfinissable).
J'avais vu "in order to understand recursion, you must first understand recursion" sur le web.
Au cours de leurs études les gens apprennent d'abord au lycée qu'il y a un phénomène de récurrence sur les entiers qui est ouvertement présenté comme un miracle qui tombe du ciel: la main de Dieu établit magiquement l'existence de la fonction
"définie par récurrence" ou la certitude de l'énoncé paramétré par $\N$ visés, après énonciation claire des psaumes incantatoires exigés par le maître (intitialisation/étape de récurrence). Après ça, s'il n'est pas dégoûté, l'étudiant poursuit son exploration des maths et découvre (sous réserve de la consistance de ZFC) des modèles ZFC où un entier (dit parfois "non standard") est l'index d'une preuve de 1=0, et aussi la possibilité, pour tout ensemble totalement ordonné I, de construire un modèle de PA où I se plonge injectivement. Ces bizarreries, avec les résultats d'indécidabilité usuels, amènent à bon droit à faire douter les gens des nombres "standards" voire des
nombres tout court.
Ce message se propose de répondre à ce genre de préoccupation (et de construire le concept de récurrence sans référence a priori au moindre nombre).
La récurrence est en fait un phénomène de point fixe (le système CWKJ introduit par christophe c admet des combinateurs de points fixes).
Je vais me servir du langage de la théorie des ensembles pour la clarté (ça reste le meilleur véhicule d'idées à mon avis) mais je n'utilise pas tout l'arsenal de ZF (ce qui suit peut être entièrement fait en logique du second ordre avec prérequis minimalistes).
En particulier il n'y a pas besoin de toute la force du schéma de compréhension, seulement du fait que les ensembles particuliers évoqués ci-dessous existent.
J'ai seulement besoin du théorème de point fixe suivant:
0°) Soit $A$ un ensemble et $f:\mathcal P(A) \to \mathcal P(A)$ une fonction croissante pour l'inclusion. Alors $f$ possède un (plus petit) point fixe; c'est-à-dire qu'il existe une partie $Z$ de $A$ telle que $f(Z)=Z$.(Tarski)
Ce point fixe est simplement l'intersection des $Y\in \mathcal P(A)$ tels que $f(Y)\subseteq Y$.
1°) Récurrence sur des nombres.
En fait l'idée de récurrence est l'exploitation indirecte du fait que les nombres sont écrits/construits avec des chiffres ( NB(*): les adjectifs "écrit"; "construit" souffrent du même problème que "standard": les maths ne les définissent vraiment que via des succédanés comme "le plus petit ensemble tel que ..."; cela dit lire le point 1.4°) ci-dessous).
1.1°) Soit $E$ un ensemble, $u\in E$, $f_0,f_1,\sigma$ des fonctions de $E$ dans $E$ telles que
(i) $f_0(u)=\sigma(u)$
(ii) $\sigma \circ f_0 = f_1$
(iii) $\sigma \circ f_1 = f_0 \circ \sigma$
Une partie $X$ de $E$ sera dite "P-stable" (resp. "B-stable") si elle contient $u$ et si pour tout $x\in X$, $\sigma(x)\in X$ (resp. $f_0(x)\in X$ et $f_1 (x) \in X$).
L'intersection d'un ensemble de parties P-stables (resp B-stables) est encore évidemment une partie P-stable (resp B-stable) et on note dan la suite $N_P$ (resp $N_B$) l'intersection de toutes les parties P-stables (resp B-stables).
Théorème: $N_B=N_P$.
Il suffit de vérifier que $N_B$ est P-stable et $N_P$ est B-stable. Pour cela il suffit d'établir que $\{x \in N_B \mid \sigma(x) \in N_B\}$ est B-stable et que $\{x \in N_P \mid f_0(x)\in N_P \text{ et } f_1(x) \in N_P\}$ est P-stable. A chaque fois c'est l'affaire d'une ligne.
Si on note $1:=u$, et pour tout $x$, $x.0:=f_0(x)$ et $x.1:=f_1(x)$ alors on a $\sigma(1)=1.0$, $\sigma(1.0)=1.1$, $\sigma(1.1)=1.0.0$, $\sigma(1.0.0)=1.0.1$ etc; ce qui suggère que (modulo les réserves évoquées en (*)) les éléments de $N:=N_P=N_B$ peuvent s'appeler les "nombres de $E$ non nuls écrits en base $2$" (ce sont aussi des nombres écrits en base 1!! C'est le point de vue de Peano en fait). Un analogue au théorème ci-dessus est démontré en COQ dans le lien ci-après, pour la base 10: https://pastebin.com/TGq4ettC.
1.2°) (définition de suites par récurrence) on garde les hypothèses de 1.1 et on suppose de plus que $u$ n'appartient pas à l'image de $\sigma$ et que $\sigma$ est injective.
Soit $E'$ un ensemble.
Soit $i$ un élément de $E'$. Soit $\varphi:E'\to E'$ une application.
Pour toute partie $G$ de $E\times E'$ on appelle $R(G)$ l'ensemble des couples $(p,q)$ de $E\times E'$ tels que $p=u$ et $q=i$, ou bien il existe $(a,b)$ dans $E\times E'$ tels que $\sigma(a)=p$, $(a,b)\in G$ et $q=\varphi(b)$.
Alors:
1.2.1°) L'application $G\mapsto R(G)$ de $\mathcal P(E\times E')$ dans lui-même est croissante. (évident)
1.2.2°) Si $F$ est un point fixe de $R$, l'ensemble $D(F)$ des $y$ de $E$ tels qu'il existe exactement un seul $z\in E'$ tel que $(y,z)\in F$ est une partie P-stable de $E$.
En effet, si $x$ est dans $D(F)$ et si $(\sigma(x),q)\in F$ et $(\sigma(x),q')\in F$, il existe $(a,a',b,b) \in E \times E \times E' \times E'$ tels que $\sigma(a)=\sigma(a')=\sigma(x)$, $(a,b)\in F$, $(a',b')\in F$, $\varphi(b)=q$ et $\varphi(b')=q'$. Comme $\sigma$ est injective, $a=a'=x\in D(F)$. Ceci entraîne que $b=b'$ et donc que $q=\varphi(b)=\varphi(b')=q'$, ainsi $\sigma(x)\in D(F)$.
Si $(u,v)\in F$ alors $(u,v)\in R(F)$ (puisque $F=R(F)$...) donc $u=u$ et $v=i$ ou bien $u=\sigma(x)$ et blabla. mais $u\notin \sigma(E)$ par hypothèse d'où l'égalité $i=v$. Ainsi $u\in D(F)$. Donc $D(F)$ est P-stable.
La restriction de $F$ ci-dessus à $D(F)$ est donc une fonction.
1.2.3°) Si $F'$ est un point fixe de $R$ alors $F(u)=i$ et pour tout $x$ dans $D(F)$, $F(\sigma(x))=\varphi(F(x))$; de plus si $G$ est une application de $E$ dans $E'$ telle que $G(u)=i$ et pour tout $x\in E$, $G(\sigma(x))=\varphi(G(x))$, alors l'ensemble $X$ des $x\in D(F)$ tels que $G(x)=F(x)$ est P-stable..
On a déjà vu que $u\in D(F')$ et donc que $F'(u)=i$.
Si $x\in D(F')$, et si $q$ est l'unique élément de $E'$ tel que $(\sigma(x),q) \in F'$, alors il existe $b$ tel que $(x,b)\in F'$ et $\varphi(b)=q$. Mais $b=F'(x)$ et $F(\sigma(x))=q$, autrement dit $F'(\sigma(x))=\varphi(F'(x))$.
Si $G$ et $X$ sont comme dans l'énoncé, il est clair que $u\in X$. De plus si $x\in X$, $F(\sigma(x))=\varphi(F(x))=\varphi(G(x))=G(\sigma(x))$ d'où le résultat.
Les théorèmes 1.2.1°; 1.2.2° et 1.2.3°; avec le théorème de Tarski cité en 0°, entraînent l'existence et l'unicité d'une fonction $h$ définie sur $N_P=N_B=N$, dite "définie par récurrence", telle que $h(u)=i$ et $h(\sigma(x))=\varphi(h(x))$ pour tout $x\in N$.
1.3°) on peut définir des opérations, par exemple (NB: dans ce 1.3°, on considèrera que $u=0$ et non pas 1): on prend $k\in N_P$ et pour un $k\in E$ on définit $\ell \mapsto k+\ell $ par récurrence en posant $k+0=k$ et $k+\sigma(x):=\sigma(k+x)$.
On peut aussi définir $\times$ par (en fixant $y\in E$) $y\times 0:=0$, $y \times \sigma(z):= (y \times z)+y$.
On peut prouver que pour tous $x,y$ dans $N_P$, $x+y=y+x$(montrer que $\{x\in E \mid x+0 =x = 0+x\}$ est P-stable puis que pour tout $y\in N_P$, $\{x\in E \mid x+y = y+x\}$ est P-stable), l'associativité, etc.
1.4°) Introduction d'un prédicat "standard" (pour les gens qui ne considèrent pas que $N_P=N_B$ est vraiment l'ensemble des nombres vraiment "construits" à l'aide de $u$ et $\sigma$ ).
On garde les hypothèses de 1.2) ci-dessus. On considère maintenant qu'on rajoute un symbole de prédicat à un argument"$St$" au langage de la théorie; $St(x)$ pourra se lire "$x$ est standard"; "$x$ est un nombre véritable"; "$x$ est un nombre construit" etc etc.
Les seules hypothèses qu'on rajoute ici sont:
(S1) $St(u)$
(S2) Pour tout $x\in E$, $St(x) \Rightarrow St(\sigma (x))$
(S3) Pour toute partie P-stable $A$ et tout $x\in E$, $St(x) \Rightarrow x \in A$ (à mon avis cette hypothèse signifie que les éléments satisfaisant St sont vraiment ceux qui sont "constructibles" en un sens raisonnable).
Je signale que l'analyse non standarde (façon IST d'Edward Nelson) est capable de manipuler un tel $St$ avec au moins un $y\in N_P$ tel que $non(St(x))$. En fait $St$ désigne une "collection" (et non pas un ensemble en bonne et due forme): la "collection des objets qui existent vraiment sur le papier" ou quelque chose comme ça.
On va maintenant malmener un peu les objections contre la formalisation de la récurrence: réponse: on n'a pas besoin de savoir ce que $St$ veut dire, on définit par récurrence la fonction comme en 1.2°) et sa restriction à $St$ sera de toute façon unique.
C'est en ce sens que les définitions bourbakistes sur des assemblages sont parfaitement définies par exemple (même si on ne sait pas ce qu'est un assemblage "vraiment physique" !!!) Ce sont des recettes algorithmiques parfaitement claires.
***********************************
2°) Récurrence sur des arbres (autrement dit: étude d'un magma libre).
Soit à nouveau $E$ un ensemble. Dans cette partie on considère une partie $B$ de $E$ et une application $p$ injective de $E\times E$ dans $E$, telle que l'image de $p$ est disjointe de $B$. Une partie $Y$ de $E$ sera dite A-stable si $B\subseteq Y$ et si pour tous $x,y\in Y$, $p(x,y)\in Y$. On désignera par $M$ l'intersection de toutes les parties A-stables: il est clair que $M$ est encore A-stable (c'est la plus petite telle partie).
Les éléments de $M$ sont des arbres binaires dont les feuilles sont dans $E$ et avec cette structure, on peut implémenter plein de choses, des formules logiques, des nombres etc.
On considère dans toute la suite un ensemble $E'$ et deux applications $\psi: E'\times E' \to E'$ et $j: B \to E'$ .
Si $G$ est une partie de $E\times E'$, on note $R'(G)$ l'ensemble des couples $(u,v)\in E\times E'$ tels que $u\in B$ et $v = j(u)$, ou tels qu'il existe $(a_1,a_2,b_1,b_2)\in E\times E \times E' \times E'$ tels que $u=p(a_1,a_2)$, $(a_1,b_1)\in G$, $(a_2,b_2)\in G$ et $v=\psi(b_1,b_2)$.
Si $G\subseteq E\times E'$, on note $D(G):= \{x\in G\mid \exists ! y \in E', (x,y)\in G \}$ exactement comme au 1.2°.
On a alors les analogues des théorèmes 1.2.1, 1.2.2 et 1.2.3 (les preuves sont les mêmes et sont laissées au lecteurs) ainsi que la conclusion:
2.1°) $R'$ est croissante.
2.2°) Si $F$ est un point fixe de $R'$, $D(F)$ est A-stable
2.3°) Si $F'$ est un point fixe de $R'$, $F'(u)=j(u)$ pour tout $u\in B$, et $F'(p(x,y))=\psi (F'(x),F'(y))$ pour tous $x,y\in D(F')$; de plus si $G$ est une autre application telle que $G(u)=j(u)$ pour tout $u\in B$, et $G(p(x,y))=\psi (G(x),G(y))$ pour tous $x,y\in D(G)$, alors l'ensemble des $x$ tels que $F'(x)=G(x)$ est A-stable.
Via le théorème 0°) on conclut à l'existence d'une unique fonction définie sur $M$ par induction à l'aide de $\psi$ et $j$.
Après on peut faire plein de choses: désigner un élément $\nu\in B$ privilégié et définir des listes (plus petite partie $L$ de $E$ contenant $\nu$ et telle que pour tout $t\in L$ et tout $h\in E$, $p(h,t)\in L$), des nombres en base un (on fixe $\mu,\nu\in B$ et on constate que comme $\sigma:x\mapsto p(\mu,x)$ est injective, les résultats de la partie 1.2°) et 1.3°) du présent message s'appliquent - noter que ceux-ci n'utilisent pas $f_0$ ni $f_1$).
On peut aussi refaire le coup du prédicat $St$ et parler des arbres "vraiment écrivables" (français?).
Etc etc ...
tu réponds auquel de mes messages et que désigne $R$ ?
Ainsi même sans entrer dans les questions d'entiers standards ou non (je ne pensais même pas à ça, parce qu'un.e sceptique n'a a priori pas de raison de "croire" en les entiers non standards; disons un.e sceptique ultrafinitiste), la définition "une succession d'assemblages" n'est pas claire : qu'est-ce qui constitue ou ne constitue pas une succession ? Est-ce que si, comme tu le dis, je fais des abbréviations de sorte que la "vraie succession" (celle que j'aurais dû écrire pour un ordi) dépasse en nombre de caractères le nombre de particules de l'univers, c'est toujours une succession ? Dès lors que cette question se pose, il faut prendre une position philosophique ("platonisme" ou pas, par exemple) et donc on quitte le royaume de la formalisation parfaite.
Entendons-nous, je le répète : moi je ne suis pas dérangé, et le niveau de formalisme qu'on peut donner me suffit largement (qui refuserait l'utilisation de "succession", franchement ?) - mais je me joue l'avocat du diable, plus précisément, de la sceptique ultrafinitiste (de conviction): face à une telle personne, je me vois mal justifier que les maths sont bien fondées, c'est tout.
C'est un peu comme si après avoir expliqué à une personne les règles du jeu d'échec, tu disais qu'il faut encore la convaincre que ces règles sont des bonnes règles pour le jeu d'échec...
Pour ton objection avec les abréviations il suffit de bien assumer ce qu'on fait et de passer toutes les abréviations en axiomes rajoutés, et ne pas prétendre que on a démontré sans ajouter d'axiomes la conclusion avec les abréviations dépliées. Mais ces axiomes sont tellement acceptés que on les passe sous silence.
Pour l'histoire de succession je ne vois pas ce que tu veux dire sur une nécessité de la fonder : c'est une notion qui n'est évidemment pas utilisée ici dans un sens mathématique (puisque il s'agit de fonder les mathématiques) mais dans le sens de la langue parlée. Et ça n'est pas un problème! De mémoire Bourbaki dit dans son introduction quelque chose comme "on ne discutera pas de la possibilité d'expliquer les mathématiques à quelqu'un qui ne saurait pas parler", et pareil pour l'identification de deux caractères identiques à des places différentes ou encore l'identification de deux assemblages identiques : ce sont clairement des admis dans la présentation de Bourbaki mais ça n'est en rien une objection à sa tentative de formalisation.
Ou plutôt : personne ne s'intéresse à ce genre de sceptique, qui considère aussi que le jeu d'échec est mal fondé parce que on a pas définit une "succession de tours" -une succession alternée en plus !- et que il faut pouvoir identifier les pièces sur l’échiquier. D'ailleurs ce sceptique aura du mal à s'exprimer puisque il devra utiliser une succession de mots :-D
@Oka : j'aime bien ta réponse pour les abbréviations, j'accepte ça. Cependant tu dis " il suffit d'ajouter que ce n'est pas un fondement mais précisément ce que sont les mathématiques. " alors que depuis le début on parle précisément de fondement :-D
Et je ne suis pas d'accord avec ton analogie avec les échecs (pour d'autres raisons que GG) : je ne dis pas qu'il faut convaincre le.a sceptique que ce sont des bons fondements pour les mathématiques, mais que "succession" a un sens.
Et tu as raison que c'est un mot utilisé dans le langage usuel, et c'est précisément mon point : le langage usuel est fondamentalement imprécis et non formel, mais on en a besoin pour parler et donc pour fonder les maths, qui reposeront donc nécessairement sur une imprécision.
Je suis d'accord qu'elle est minime, à nouveau : moi je suis convaincu. Mais elle existe, et c'est un peu illusoire de prétendre que non
La seule chose "première" qu'elles s'auto-infligent est l'EXPLICITATION.
Qu'est-ce que ça veut dire?
Ca veut dire [large]"mettre en rouge gras gros caractères** tout ce qui n'a pas été justifié"[/large], rien de plus.
[small]Certaines personnes ne l'ont pas bien compris, une fois je bouffais au resto avec une pédago et elle était "choquée" (dixit elle-même) quand, me demandant un exemple d'indécidable qui le restera éternellement, je lui ai répondu "X=>X". Elle n'avait pas conscience que cet énoncé est l'énoncé le plus indécidable de tous les temps.[/small]
Cet impératif conduit ENSUITE, naturellement, à la formalisation. Pour évoquer les "règles de déduction", arbitraires ou pas, l'important n'est pas là, mais dans le fait qu'elles sont ELLES AUSSI considérées comme SUPPOSEES.
Pour reprendre le mot "sceptique", la règle d'avancée du dialogue est le RECENSEMENT, c'est tout: $<<$ sceptique tu me demandes pourquoi, je ne te réponds pas, je continue, prends bien note que je ne t'ai pas répondu, et enregistrons ça avec l'étiquette: "non accepté par sceptique"$>>$. Pour abréger, on a appelé cette étiquette "hypothèse", comme on aurait pu l'appeler "statut:dsg9nlijulg"
** pour faire simple.
@Maxtimax : oui ma phrase est mal tournée je voulais dire "un fondement" comme : "une manière de faire parmi d'autres pour accéder enfin aux mathématiques (qui seraient autre chose)".
Tu dis que déjà je le trouve bien formel et très précis dans sa forme la plus simple (les imprécisions viennent surtout de l'opacité référentielle), mais surtout ce n'est pas la question ! Ou alors c'est moi qui comprends mal le désir de ModuleLibre et plus généralement de ceux qui demandent une introduction aux mathématiques.
Pour moi il y a certains sous entendus comme : "j'ai bien compris les règles des échecs / de l'allemand / du football et j'en fais le dimanche après midi, mais pour les maths il n'y a rien à faire je n'y comprends rien : c'est comme si on me parlait en allemand pour m'apprendre l'allemand !!".
Là tu deviens plus sceptique que le sceptique, qui pourrait se tourner vers toi et te dire qu'il a bien compris les règles des échecs même si on lui a expliqué en bon français.
Je ne vais pas parler pour ModuleLibre, je ne connais pas son véritable désir; mais je sais que dans mes débuts d'initiation à la logique c'est ça qui me posait problème - j'ai d'ailleurs dû poster quelques trucs sur ce forum à ce sujet. Par exemple quand j'ai ouvert le Cori et Lascar (ce que ModuleLibre a visiblement fait) et que j'ai lu au tout début "blabla on sait ça et ça sur les formules à $n$ symboles" j'étais déçu (#choquédéçu pour reprendre l'expression) et quand je me suis rendu compte que je ne trouvais rien de rien qui repartait de zéro (zéro zéro) j'ai commencé à me poser des questions à ce sujet, et ce n'est qu'un moment après que je me suis rendu compte que c'était illusoire et me suis satisfait d'accepter "une formule blabla" sans avoir dit ce qu'était une formule (chez Bourbaki, une "succession d'assemblages", mais c'est kif-kif). Bien sûr, à nouveau, je ne prétends pas détenir la sagesse infinie, ni même que ModuleLibre a le même souci que moi à l'époque, mais son premier message m'a fait penser à mes interrogations de l'époque, et donc j'essaie de lui fournir des réponses qui m'auraient aidé, c'est tout.
Si toi, tu n'as jamais même osé imaginer qu'on puisse tout fonder sans imprécision, tant mieux pour toi - mais si quelqu'un.e ne le sait pas il faut lui dire et ne pas prétendre que "si si, tout est 100% précis".
Autrement dit, il y a un admis au tout début (dans la philosophie de christophe: il faut donc expliciter l'admis) qui est qu'on se comprend quand on dit "succession d'assemblages" (si on suit Bourbaki, ou "formule" si on suit Cori et Lascar en faisant semblant qu'ils fondent, ou "séquent et contexte" si on suit HoTT, etc.) - et prétendre que ce n'est pas un admis, bah ou bien je veux en voir la preuve ou bien c'est mentir.
Il y a par exemple des choses intéressantes dans Wittgenstein et les mathématiques (T.E.R. 2004), notamment en lien avec Gödel.
On peut définir par induction sans redondance (sans quoi des interpréteurs de langages fonctionnels basés sur ce procédé ne pourraient même pas exister physiquement).
Soit par exemple l'application a priori partielle qui à $\phi:formule \to formule$ associe $\Theta(\phi):formule \to formule$ telle que $\Theta(\phi)(U):=\neg U$ si $U$ est atomique, $\exists x \phi (F)$ si $U=\forall x F$, $\forall x \phi(F)$ si $U=\exists x F$, $\phi(G) \vee \phi(H)$ si $U = G \wedge H$, $\phi(G) \wedge \phi(H)$ si $U = G \vee H$ et $\neg \phi(V)$ si $U = \neg V$.
Alors on définit sans ambiguïté le contraire d'une formule comme étant un point fixe de $\Theta$ (i.e. "$\nu:=\Theta(\nu)$").
A défaut d'avoir un méta théorème qui dit "pour toute formule $X$, $\nu(X)$ donne une formule qui est ...", j'ai pour chaque formule que je peux écrire $G$, une suite d'égalités $\nu(G) = ... = H$ où $H$ est ce à quoi on pense. Et je peux mettre au défi mon détracteur de fournir un exemple de formule qui fera échouer ma procédure.
L'auteur de la très consternante phrase "in order to understand recursion, you must first understand recursion" était soit malhonnête, soit pas vraiment au courant, soit complètement ivre au point d'oublier jusqu'à l'existence des combinateurs de points fixes (bon il pouvait aussi faire uune blague à la "gnu", mais malheureusement les gens ont fini par le prendre au sérieux).
EDIT : j'avais mal lu : tu dis que tu peux le faire pour chaque formule à la main : ok, et alors ? ça me définit "succession" du coup ? :-D
(les lettres que j'emploie sont "officielles" pour autant que je sache et "$B,C$" ne désignent pas la même chose que dans le post de cc).
Pour tous termes $a,b,c$, $ab$ abrège $a*b$ et que $abc$ abrège $(ab)c$. On a encore une relation binaire (dite "de réduction").
On considère $B,W,C,K\in \mathcal Z$
On suppose que pour tous $x,y,z\in \mathcal Z$
$Bxyz <x(yz)$
$Cxyz < xzy$
$Wxy < xyy$
$Kxy < x$
et que
R1°) $<$ est réflexive et transitive
R2°) pour tous $p,q,r$, si $p<q$ alors $pr <qr$ et $rp < rq$.
On pose $I:=WK$.
1°) On a $Ix < x$ pour tout $x$
(en effet $Ix = WK x < Kxx < x$)
On pose $M:= WI$.
2°) On a $Mx < xx$ pour tout $x$.
Car $Mx = WIx < Ixx < xx$
3°) Pour tout $f\in \mathcal Z$, $CBMf(CBMf) < f [CBMf(CBMf)]$
Car $CBMf(CBMf) < BfM(CBMf) < f[M(CBMf)] < f[CBMf(CBMf)]$
On pose $Y:= BM(CBM)$.
4°) $Yf < CBMf(CBMf)$ pour tout $f$.
Car $BM(CBM)f < M(CBMf) < CBMf(CBMf)$.
Ainsi à l'aide de 3° et 4°, on voit que pour tout $f$, il existe $e$ tel que $Yf < e$ et $e < fe$. C'est ce qu'on appelle un combinateur de point fixe. Donc parler de "$e$ tel que $e$ se réduit en $fe$" se fait sans pétition de principe.
5°) Soit $T:=CI$. Alors $Txy < yx$ pour tous $x,y$
On a $Txy = CIxy < Iyx < yx$.
6°) Soit $V:=BCT$. Alors pour tous $x,y,z$, $Vxyz < zxy$
Car $BCTxyz < C(Tx)yz < Txzy < zxy$
On va voir que $V$ permet de représenter des couples. Ci-dessous, on définit des opérateurs de projection:
Soient $\pi_1:=TK$ et $\pi_2:=T(KI)$
7°) Pour tout $x$, $KIxy<y$.
$KIxy<Iy<y$.
8°) Pour tous $x,y$, $\pi_1(Vxy) < x$ et $\pi_2(Vxy) < y$
$\pi_1(Vxy) =TK(Vxy) < VxyK < Kxy <x$ et
$\pi_2(Vxy) =T(KI)(Vxy) < Vxy(KI) < (KI)xy <y$.
Après on peut construire par induction des opérations sur des arbres. Les détails sont traités dans ce document bordélique (qui devra être amélioré): https://pastebin.com/p1jDw9cM
** Je l'ai déjà raconté je l'avais inventé pour prouver le Th de Godel (sans savoir qu'il existait) vers 17-18and et qu'elle n'a pas été ma surprise quand bien plus tard j'ai découvert l'existence de la spécialité logique MAIS SURTOUT qu'elle avait eu "la simplicité" contrairement à moi d'inclure LES VARIABLES dans son champ (de sorte que le besoin de combinateurs apparaissait superfétatoire)
Aujoud'hui, 35ans plus tard, j'avoue que j'en reviendrais bien à dire que je n'avais pas tort mais le contexte a totalement changé, today, ce serait pour les raisons que tu dis que je défends la disparition des variables (liées).
Par ailleurs, je t'ai ouvert un fil pour faire la fête entre érudits dans ce domaine, pour pas que Module ne soit trop noyé dans les divers discussions techniques. J'ai essayé de bien détailler, mais bon il ya tant à dire.
ESSAIE CK(CCW)
L'inspiration vient de ce qu'on part à l'envers:
y x > y (Kx y) >...
Pense à $C$ comme à l'opération $\circ$ inversée, ie $Cfg = g\circ f$, du coup $[y\circ (Kx) ] (y)$ va s'écrire :
$$ C(Kx)yy$$
Et tu as ton $y$ qui est passé à droite en argument, mais "hélas" dupliqué. Mais tu as $W$.
$$ W(C(Kx)) y < C(Kx)yy$$
Et une fois là, tu n'as plus qu'à t'occuper de $W(C(Kx))$, qui en termes usuels n'est que $[W\circ C\circ K] (x)$
donc qui provient de $W\circ (C\circ K)$, que tu obtiens au choix (car tu as aussi $(W\circ C)\circ K$) en faisant :
$$ C(CCK)W$$
ou en faisant
$$CK(CCW)$$
qui agissent de la même façon.
Dommage que je ne l’ai pas trouvée tout seul.
Je suis prêt pour la suite ! Et cette fois j’essayerai d’avoir une vision plus globale du problème.
Encore merci.