Définition exacte d'un prédicat en maths
Depuis un moment déjà, je me distancie des axiomes ZFC comme fondement des mathématiques. Pour un certain nombre de raisons, je trouve les axiomes NBG plus efficaces, plus élégants. En comparant les deux axiomatiques, j'en suis venu à me demander comment exactement il faut "voir" les prédicats quand on fait des mathématiques.
L'exemple le plus flagrant selon moi est le cas de l'axiome de compréhension.
Schéma d'axiomes de compréhension dans ZFC :
$\forall a_1, ... \forall a_p, \forall A, \exists B, \forall x; [x \in B \Longleftrightarrow (x \in A \wedge P(x,a_1 ,... a_p) )]$
Dans cette version, non seulement on se retrouve avec des pointillés (je pense qu'on peut trouver une formulation biscornue qui permet de s'en passer, mais bon), mais en plus il faut "sous-entendre" que $P$ est un prédicat dont les seules variables libres sont $x$ et les $a_k$. Je trouve ça assez laid, parce que je n'ai vu encore nulle part comment "bien poser" quels sont les formules (prédicats) qui sont censés être effectivement valides dans ZFC.
Axiome de compréhension dans NBG :
$\forall C, \forall x^V, \exists a^V, \forall z, [z \in a \Longleftrightarrow (a \in x \wedge z \in C)]$
Je précise juste : le V en exposant est une notation empruntée à Wikipédia et qui est un raccourci pour désigner les ensembles (donc quand il y a le V, la variable est un ensemble, sinon c'est une classe) dont on peut se passer sans aucune difficulté.
En tout cas, dans la version NBG, on n'a pas besoin de s'embêter avec un prédicat et ses variables libres, tout s'exprime parfaitement bien avec le langage des classes, ce qui est nettement plus élégant selon moi.
J'ai donc une question en plusieurs parties :
1) Comment fait-on, que ce soit dans le langage des ensembles avec ZFC ou le langage des classes avec NBG, pour définir ce qu'est un prédicat valable ? Je veux dire, sans français, uniquement de manière formelle, définir quels sont les prédicats que la théorie est "capable de contenir". Visiblement NBG contourne le problème en se ramenant systématiquement à un prédicat $x \in C$ ou $x$ et $C$ sont des classes (donc des objets de base de la théorie) et $\in$ est le prédicat d'appartenance qui m'amène à poser ma deuxième question.
2) Je sais que quand on écrit des maths, les symboles primitifs sont $\in$ et =. Il me semble qu'on peut donner une définition de l'égalité uniquement à partir de l'appartenance (et ça finir toujours par m'embrouiller avec l'axiome d'extensionnalité, mais passons) mais l'appartenance elle-même ne peut pas avoir de définition propre dans le langage du calcul des prédicats, si ? Je veux dire, sans utiliser de français pour expliquer ce que "x \in A" veut dire. Donc ça serait en quelque sorte un symbole primitif (dont on a besoin pour définir tout le langage) qu'on doit "accepter" sans qu'il puisse être défini dans le langage même de la logique du premier ordre, et ça serait le seul ?
En vrai, j'essaie de comprendre comment faire des mathématiques "comme une machine", de manière purement formelle. J'aurais du mal à expliquer pourquoi ça m'intéresse.
L'exemple le plus flagrant selon moi est le cas de l'axiome de compréhension.
Schéma d'axiomes de compréhension dans ZFC :
$\forall a_1, ... \forall a_p, \forall A, \exists B, \forall x; [x \in B \Longleftrightarrow (x \in A \wedge P(x,a_1 ,... a_p) )]$
Dans cette version, non seulement on se retrouve avec des pointillés (je pense qu'on peut trouver une formulation biscornue qui permet de s'en passer, mais bon), mais en plus il faut "sous-entendre" que $P$ est un prédicat dont les seules variables libres sont $x$ et les $a_k$. Je trouve ça assez laid, parce que je n'ai vu encore nulle part comment "bien poser" quels sont les formules (prédicats) qui sont censés être effectivement valides dans ZFC.
Axiome de compréhension dans NBG :
$\forall C, \forall x^V, \exists a^V, \forall z, [z \in a \Longleftrightarrow (a \in x \wedge z \in C)]$
Je précise juste : le V en exposant est une notation empruntée à Wikipédia et qui est un raccourci pour désigner les ensembles (donc quand il y a le V, la variable est un ensemble, sinon c'est une classe) dont on peut se passer sans aucune difficulté.
En tout cas, dans la version NBG, on n'a pas besoin de s'embêter avec un prédicat et ses variables libres, tout s'exprime parfaitement bien avec le langage des classes, ce qui est nettement plus élégant selon moi.
J'ai donc une question en plusieurs parties :
1) Comment fait-on, que ce soit dans le langage des ensembles avec ZFC ou le langage des classes avec NBG, pour définir ce qu'est un prédicat valable ? Je veux dire, sans français, uniquement de manière formelle, définir quels sont les prédicats que la théorie est "capable de contenir". Visiblement NBG contourne le problème en se ramenant systématiquement à un prédicat $x \in C$ ou $x$ et $C$ sont des classes (donc des objets de base de la théorie) et $\in$ est le prédicat d'appartenance qui m'amène à poser ma deuxième question.
2) Je sais que quand on écrit des maths, les symboles primitifs sont $\in$ et =. Il me semble qu'on peut donner une définition de l'égalité uniquement à partir de l'appartenance (et ça finir toujours par m'embrouiller avec l'axiome d'extensionnalité, mais passons) mais l'appartenance elle-même ne peut pas avoir de définition propre dans le langage du calcul des prédicats, si ? Je veux dire, sans utiliser de français pour expliquer ce que "x \in A" veut dire. Donc ça serait en quelque sorte un symbole primitif (dont on a besoin pour définir tout le langage) qu'on doit "accepter" sans qu'il puisse être défini dans le langage même de la logique du premier ordre, et ça serait le seul ?
En vrai, j'essaie de comprendre comment faire des mathématiques "comme une machine", de manière purement formelle. J'aurais du mal à expliquer pourquoi ça m'intéresse.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Les axiomes de compréhension servent à définir les sous-ensembles du type $A = \{x \in E \mid P(x) \}$ ou $P$ est "un certain prédicat".
Avec l'axiome dans sa version NBG, on a :
Pour toute classe $C$, pour tout ensemble $e$, il existe un ensemble $a$ dont les éléments sont exactement les ensembles qui sont à la fois dans $e$ et dans $C$.
J'ai pris ces notations exprès parce que si on applique cet axiome à $e=E$ et $a=A$, on a : pour toute classe $C$, le sous-ensemble $A$ de $E$ dont les éléments sont dans la classe $C$ existe.
J'en suis donc amené à écrire que la classe $C$ que je dois utiliser pour définir $\{x \in E \mid P(x) \}$ est la suivante :
$z \in C \Longleftrightarrow P(x)$. Donc à condition d'être sûr que cette classe existe bel et bien (donc il faut en prouver l'existence, en fonction du prédicat $P$), je peux me passer de la notation $P(x)$ dans la définition du sous-ensemble $A$.
Etant donné un certain prédicat donc, comment sait-on s'il existe bien une classe dont les éléments sont les classes (enfin, les ensembles, puisque ce sont les éléments d'une classe) qui vérifient ce prédicat ? Et quels sont les prédicats pour lesquels cette construction est valable ? Je n'arrive pas à me convaincre que tout ce qu'on fait est bien défini...
Comme tu le sais déjà, j'essaie de VRAIMENT comprendre sans aucune lacune comment construire rigoureusement les nombres entiers uniquement à partir des axiomes NBG. Les entiers naturels, c'est bon, les opérations dessus, je suis en train de le faire, les entiers relatifs a priori ça ne devrait pas poser trop de problèmes (et tout ce qui vient après, normalement, c'est bon). Donc quand on a construit $\{x \in N \mid \text{Ent}(x)\}$ dans mon autre topic, j'essaie de comprendre comment on fait ça proprement avec NBG. D'où mon deuxième post, comment fait-on pour ramener un prédicat à une variable libre $P(x)$ à un prédicat $x \in C$ ou $C$ est une classe dont on peut démontrer l'existence.
(Bon en fait dans NBG le schéma d'axiomes de compréhension pour les classes est un schéma de théorèmes; donc on a l'impression de s'en tirer, mais pour l'exprimer il faut bien dire "Pour toute formule $P$")
Je pense qu'il va falloir que je me jette un peu plus dans les formules à variables libres/liées etc parce qu'il y a encore des choses que je ne comprends pas exactement. Dans le sens de "quelles formules sont valables" je veux dire.
Par exemple, le prédicat "de base", je dirais que c'est un probablement celui de la forme $(x \in A)$. Mais celui-là n'est pas quantifié, je ne sais pas trop quelle variable est quoi (libre, liée) en fonction des quantificateurs qu'on met devant etc. C'est compliqué tout ça. En tout cas j'aurai appris que même dans NBG, on ne peut pas TOUT réduite à des prédicats $(x \in A)$.
De toute façon on va pas se mentir: une fois dans la machine on n'a pas gagné grand chose à cause des obstructions liées à la NP complétude omni présente. Le moindre mission prend bien que des milliards d'années à la machine.
Je suis justement en train de construire un système formel où on remplace heuristiquement "il existe au moins un succès" par "le nombre de succès est impair" pour substituer l'algèbre linéaire (decidzble en temps polynômiale) au calcul logique dans la machine mais l'inconvénient est que les réponses sont juste indicatives (ça donne disons une astrologie inspirante mais rien de plus)
** On utilise les combinateurs de la LC.
[Inutile de recopier un message présent sur le forum. Un lien suffit. AD]
Comment écris-tu formellement cet axiome ? Je veux surtout savoir comment on peut écrire formellement "P est un prédicat de la théorie des classes", en gros. Pour l'instant, je crois qu'on ne peut pas, qu'il faut le sous-entendre.
Au même titre qu'au premier ordre, la récurrence c'est un schéma d'axiomes, pas un axiome
Concernant la migration de ZF vers NBG (ou autre axiome unique, il ya 1001 possibilités), il te faut faire le ptite effort de t'interroger sur comment sont construites les formules. Ce ne sont que des et, des ou et des quantifications (qui deviennent sémantiquement des projections).
Mais si tu veux tout en un seul axiome (enfin nombre fini d'axiomes), il est important que tu conduises une réflexion sur des bases du collège: pourquoi les profs écrivent-ils que associatif blabla $a*(b*c)=(a*b)*c$, puis après ils changent les parenthèses de place à la hache?
Et bin ils en ont le droit pour une raison qui n'est jamais enseignée. Tu devrais faire l'exercice.
Au final, tu auras juste besoin de mettre dans les axiomes les choses suivantes:
1/ je peux passer de $(x,(y,z))\mapsto A$ à $((x,y),z)\mapsto A$
2/ je peux passer de $(x,y)\mapsto A$ à $(y,x)\mapsto A$
3/ je peux passer de $(x,y)\mapsto A(x,y)$ à $x\mapsto A(x,x)$
etc, etc
En gros commutativité, associativité, projection, constances. Le mieux serait vraiment que tu fabriques ton système tout seul. Tu serais fier.
Il y a encore mieux, que NBG ne risquait pas trop de connaitre à l'époque car ce n'était pas en vogue, c'est d'adopter le point de vue fonctionnel: Juste avec les 3 fonctions universelles suivantes:
$Kxy:=x$
$Wxy:=xyy$
$Cxyz:=y(xz)$
abc abrège (ab)c
Par exemple $WKx=Kxx=x$
On peut faire toutes les autres: en te rappelant que $(\forall xRx)$ peut se définir par $ER(KV)$, où $V$ abrège "vrai" et $Exy:=(x=y)$, etc, tu auras un système bien plus léger et maniable et tout autant "équivalent" opérationnellement à ZF que l'est NBG.
Les points de vue fonctionnel ou ensemblistes sont strictement équivalents par:
$a(b)=\{x\mid (b,x)\in a\}$ et $f=\{(x,y) \mid y\in f(x)\}$
Si tu veux une bijection entre couples et objets (c'est mieux pour l’extensionnalité), tu appliques d'abord Cantor Bernstein.
D'accord, le schéma de compréhension pour les classes dans NBG est un schéma de théorèmes, et pas un schéma d'axiomes. Ce que je veux savoir, c'est comment écrire uniquement en symboles le théorème "Pour toute classe $C$, pour tout prédicat $P$ (à une variable, éventuellement à paramètres), il existe une classe $V$ dont les éléments sont les éléments $x$ de $C$ tels que $P(x)$."
ça vous paraît peut-être stupide mais j'ai besoin d'écrire les choses qui sont à un niveau aussi fondamental que ça en symboles pour m'assurer que c'est "juste". Et le souci que j'ai, c'est que dans NBG, les lettres majuscules/minuscules (précédées d'un $\forall$ ou d'un $\exists$) désignent systématiquement des classes ! Je ne sais pas comment écrire en symboles une formule dans laquelle la lettre $P$ désignerait un prédicat et non pas une classe. Et c'est ça que je ne comprends pas. ça n'a aucun sens pour moi d'écrire un truc du style $\forall P$ parce que $P$ n'est pas une classe donc je ne sais pas comment écrire ce truc uniquement en symboles, et j'aimerais savoir si oui ou non c'est possible d'écrire uniquement en symboles la phrase entre guillemets de mon premier paragraphe.
EDIT : même la phase "étant donné un prédicat $P$, pour toute classe $C$, il existe une classe $V$ dont les éléments sont les éléments $x$ de $C$ tels que $P(x)$." me conviendrait. Je veux juste une formule entièrement en symboles dans laquelle il est clair que $P$ désigne un prédicat et non une classe. Je ne comprends pas comment faire ça.
Dans NBG, il n'y a pas de classe, (enfin à ma connaissance, je ne l'ai jamais lu, mais ces trucs évidents de logiciens se devinent sans les lire), il n'y a que des ensembles: simplement il y a les gros et les petits :-D
Un ensemble est dit gros quand $\forall y: x\notin y$. Sinon, il est dit petit. Ce que d'autres, dans ZF, vont nommer classes ou relations, dans NBG ça pourra s'appeler "gros ensembles". Rien de plus profond que ça.
J'ai l'impression que ce que tu demandes c'est tout bêtement qu'on te fasse l'exo de montrer que pour toute relation $R$ écrite avec des signes et des paramètres, NBG démontre que $\exists x\forall y,z: [y\in z \to (R(y)\iff y\in x)]$ :-D :-D
Mais justement, c'est un très bon exercice, à la fois "évident" quand on a eu le déclic et pas du tout facile quand on ne l'a pas. Il ne demande pas de l'inspiration, mais juste une compréhension "de fond" de ce que font les symboles en maths. Ca me parait difficile que de te le faire à ta place. En gros, NBG a fait exprès de mettre ce qu'il fallait comme ingrédients dans ses axiomes pour que cet exercice soit "naturellement faisable"
Et la réponse, Homo Topi, est celle que j'ai écrite plus haut : "Pour toute formule $P$ à une variable libre $x$ et à paramètres $w_1,...,w_n$, on a le théorème : $\forall C, \forall w_1...\forall w_n \exists K, \forall x, x\in K\iff (x\in C\land P(x,w_1,...,w_n))$".
Si cette réponse n'est pas claire, il faudra plus de précisions sur ta question :-S
maxtimax : donc tu ne peux effectivement pas écrire "machin est une formule" avec uniquement des symboles. ça me rend un peu triste, mais bon, tant pis. si on peut pas, on peut pas, je m'y ferai :-D
Je crois que les logiciens les plus déterminés font tout ça en partant d'un fragment de l'arithmétique: à partir de ce fragment on peut définir théorie etc. en particulier parler de ZFC et de ses théorèmes; mais il faut définir ce fragment, et pour définir ce fragment il faut dire "telle et telle formule".
Et non on ne fait pas des catégories avec des classes mais avec des ensembles. Sinon noyage dans verre d'eau inévitable. D'ailleurs il se peut que tu aies commencé à voir le verre comme un océan. Tes classes sont juste ce que je t'ai signalé être les "gros ensembles". Et tu l'échappée ABSOLUMENT pas au diagonal argument simplement tu "boudes pudiquement" sa survenue.
Si tu veux VRAIMENT un édifice qui essaie d'y "échapper partiellement" tu as NF de Quine. Mais la c'est vraiment un autre esprit.
@max merci pour la précision.
(En vrai, je serais hyper étonné que personne n'ait déjà pensé à faire ça avant)
Des fois je trouve ce bazar de logicien tellement intéressant que j'en oublie de faire des maths...
EDIT : j'ai l'impression que l'introduction d'un quantificateur de prédicats serait d'un intérêt assez limité... en dehors des axiomes fondamentaux des maths où on pourrait avoir une version purement formelle de "pour toutes variables machin, pour tout prédicat truc portant sur les variables machin, il existe une classe dont les éléments sont les classes qui vérifient truc(machin)". mais bon, ça serait déjà ça pour me donner l'impression que je me casse la tête pour un truc qui sert pas littéralement à rien :-D :-D :-D
Mais tu le cherches au mauvais endroit car tu le cherches à l'extérieur du modèle. Ca, tu ne trouveras jamais rien "à l'extérieur", car ça n'a tout simplement pas de sens.
Il faut d'abord "donné un tour de clé". Par exemple, tu peux considérer une théorie qui ne parle que des suites finies de lettres de l'alphabet, mais il faudra penser que les lettres de l'alphabet que tu écris physiquement sur des feuilles de papier issue du bois ne sont pas celles désignées par ta théorie. Ce que fait ta théorie c'est qu'elle te parle de tous les mondes où il y a ces lettres, et toi, après tu en déduis que c'est vrai "dans ton monde matériel" si ça te chante et moyennant un acte de foi irréductible.
Ce qu'on attend à minima (mais dès Peano, c'est fait) d'une théorie c'est bien entendu qu'elle reproduise "en interne" ce que tu fais "en externe". Pour ce qui est de la logique, toutes le sthéories dont l'ensemble des théorèmes n'est pas récursif le font, mais attention, en dehors des théories, il y a des tas d'ensembles non récursifs qui ne sont pas "universels". Le cas des théories logiques est très particulier, puisque, (ça n'a jamais été prouvé) on "constate" qu'elles sont toutes universelles ou récursives.
Ensuite, il y a la manière de le faire. Les "fondements" (bien grand mot), consiste à le faire "sans coder" ni interpréter**. A l'heure actuelle seule la théorie des ensembles fait ça (et de toute façon seule la TDE englobe toutes les maths actuellement, c'est une convention d'échanges d'articles)
** au sens "en dehors du résidu matériel --> platonic-monde minimum obligatoire". En TDE tu écris les choses comme tu les ressens, sans aucun codage, alors que pour coder un théorème dans Peano sur de l'analyse réelle, c'est assez illisible.
Après je me trompe peut-être, mais dans ce cas, pourquoi les auteurs qui la présentaient n'ont-ils pas pris soin de bien mettre en exergue ce que l'homotopie apporte vraiment (en dehors des truismes qu'ils ont accolé au mot homotopique)???
Ce que je crains c'est un truc tout bête: comme ça n'est pas fait par des logiciens (essentiellement même si quelques uns prêteront leur nom) ça apparait comme tout beau tout nouveau à des matheux spécialisés dans autre chose et qui découvrent l'eau chaude. Evidemment, je peux me tromper (mais tout ce que j'ai vu plaide en faveur de ce que je dis présentement et je ne suis pas le seul à le penser, je connais des experts patentés bien plus sévères encore et peu suspects de partisanité (des TDistes "tranquilles" H24 sur leurs maths, ne faisant pas de politique))
ZF(C) : axiomes de Zermelo, Fraenkel avec ou sans l'axiome du Choix (nom usuel : théorie des ensembles)
NBG : axiomes de von Neumann, Bernays et Gödel (nom usuel : théorie des classes)
TDE : théorie des ensembles
THT : théorie homotopique des types
LC : lambda-calcul, je présume
Je vais essayer de documenter en quelques lignes ce que sont vraiment les maths (enfin les preuves de maths).
1/ Tout d'abord, c'est une erreur morale* de considérer ZF comme un système d'axiomes. Il n'y a à proprement parler qu'un seul axiome dans ZF et pour le reste en fait, c'est la structure grammaticale qui est mise en place en amont, bien avant tout raisonnement.
2/ En conséquence de quoi s'interroger sur les axiome de ZF est bien souvent une perte de temps. Ce qu'il faut c'est s'interroger sur les preuves une fois qu'elles sont écrites et non pas avant même de les écrire. En effet, une fois qu'on a compris que ZF ne contient pas d'autres axiomes que l'extensionnalité, c'est la façon dont les preuves s'articulent qui va donner l'information réelle.
* je l'utilise dans le sens utilisé quand on dit "moralement" IR est l'ensemble des points d'une droite, ou des choses comme ça, mais bien évidemment pas dans le sens du bien et du mal.
3.1/ Je détaille un peu: la présentation habituelle est qu'on affirme axiomatiquement qu'il existe $a$ tel que $\forall x: [x\in A\iff R(x)]$
3.2/ C'est gravement erroné d'étudier la pensée humaine sous cette exigence de perfection scientifique. Entendons-nous bien, il est utile pour garantir les certitudes démontrées de savoir tout ce qu'on a supposé, et donc y compris d'avoir enregistré qu'on a utilisé cet axiome. Mais ça ne correspond pas du tout à la pensée humaine.
3.3/ La pensée humaine commence bien en amont par DEFINIR (elle croit que c'est une définition) :
$$ \{x\mid R(x)\} $$
autrement dit, elle abrège ce que j'ai appelé "R" ci-dessous. Et on voit bien que pour écrire ce post, je n'ai pas pris un exemple de R, mais utilisé la lettre R majuscule. Il est donc complètement idiot a priori de prétendre que mon "a" arrive après que j'ai prétendu qu'il existe $a$ tel que $\forall x: [x\in A\iff R(x)]$ et ait nommé par la lettre minuscule $a$, un des témoins de cette existence.
3.4/ Je raconte, du coup comment ça se passe vraiment dans nos têtes, les maths et l'éthique scientifique ayant requis PLUS TARD (et entre nous soit dit, grâce à la crise des fondements) qu'on assume tout
[small](elle ajuste oublié en passant de gérer les multi-occurrences qui, au même titre que les abréviations ci-dessus, NECESSITAIENT d'être placées en statut d'assumage: on a vu sur le forum les dégâts que ça faisait sur certains littéraires de croire que dans $blabla(u,w,u)$, ce n'est pas l'auteur ET LUI SEUL qui porte la charge d'avoir écrit $x=y=a\to blabla(x,w,y)$)[/small]
3.5/ On a toutes les suites de signes au sein desquelles on a appris à gérer les capture de variables liées, les connecteurs, etc. Et on a des groupes de la forme $\{x\mid M\}$. Et bien c'est tout bête, il faut d'abord EN AMONT quotienter cette structure par l'équivalence compatible $a\in \{x\mid M(x)\} == M(a)$, et c'est tout. Tu obtiens alors une structure verbale très simple, mais où tu es sûr de ne pas te tromper et n'as jamais à écrire $ceci\in \{trucs\mid blabla\}$, puisque l'objet syntaxique l'a déjà fait.
3.6/ Et c'est seulement après que tu étudies quelles phrases entrainent quelles autres, etc. Et c'est d'ailleurs très sain de procéder ainsi, car à la différence de l'approche axiomatique sur le système libre des suites de caractères, tu ne peux plus ignorer que le système est "faiblement contradictoire" dans le sens que de toute façon, tu seras obligé d'attribuer seulement à un sous-ensemble strict de l'ensemble des phrases des valeurs de vérité familières (à cause du cèlèbre $a:=\{x\mid x\in x\to P\}$ qui vérifie que $a\in a$ est EGAL EN DUR [small](c'est une égalité physique (qui doit être vue comme telle))[/small] à $(a\in a \to P)$
3.7/ Et les distinctions entre NBG, ZF, etc ne changeront rien à l'affaire. Et encore moins bien évidemment les usines à gaz d'anciens grands matheux qui redécouvrent l'eau chaude à la retraite avec du snobisme catégorique ou de prétendus re-fondements.
3.8/ Parfois on entend certaines personnes parler de typage, mais il faut bien comprendre un truc. Ils affectent la valeur "nosense" à certaines suites de caractères et au contraire focalisent sur d'autres. Ce faisant ils croient esquiver des difficultés.
Ca me fait exactement penser à un reproche écrit collectif que j'ai envoyé à mes 3 chefs le lendemain du bac où je rappelais que quand ils laissent passer des quidams en 1S en ayant l'impression de s'abstenir devant de l'insistance des familles (genre discours bateau, "ok, je signe, mais je vus aurai prévenus") , ils se mentent à eux-mêmes et prennent une décision.
Pour les fanatiques de typages, c'est exactement la même chose, ils croient ne pas attribuer de valeur à certaines signes de caractères, alors qu'ils ne font qu'envoyer une grosse partie des mots sur "nosense", ce qui peut tout à fait être fait de manière assumée et consciente (et qui est généralement mieux fait quand c'est conscient). Je précise que je ne vise personne en particulier, mais juste des slogans trop répandus aujourd'hui
4/ Je rappelle qu'une fois ça dit, et la structure de phrases HONNETES enfin précisée, TOUT théorème de maths $P$ a la propriété suivante:
il existe $H_1,..,H_n$ tel que chaque $H_i$ est d'une (**) des formes logiques qualifiées d'évidences formelles et
$$ H_1=[H_2\to (H_3\to (......\to (H_n\to P)...)]$$
Autrement dit, l'ensemble des théorèmes de maths est facteur droit d'un ensemble très simple. (ce n'est pas un langage algébrique, mais il s'en faut d'un epsilon***)
(**) dans le désordre:
1/ $A\to (B\to A)$
2/ $(A\to \to ((B\to C)\to (A\to C))$
3/ $(A\to (A\to )\to (A\to $
4/ $((A\to \to \to ((B\to A)\to A)$
5/ $(\forall x[A\to B])\to ([\forall xA]\to [\forall xB])$
*** cela est dû au fait que l'ensemble des suites de caractères telles de la forme $uQv$ telles que $u=v$ n'est pas algébrique. Mais on peut très bien contourner le problème: l'ensemble des mots de la forme $uQv$ tel que $v$ s'obtient en retournant $u$ lui est algébrique. (Exemple $94731Q13749$). Et si on veut (je ne le fais pas), en s'autorisant de prendre des langages algébriques et leur intersection, on atteint très vite tout ce qui est récursivement énumérable, donc en particulier l'ensemble des théorèmes de maths.
Il suffit de faire un langage qui reconnait les suite $u_1Qu_2'Qu_3Qu_4'...$ telle que $u_1Qu'_2$ convient et $u_3Qu_4'$ convient, etc ET telles que (deuxième langage algébrique) $u_2'Qu_3$ convient et $u_4'Qu_5$ convient, etc.
Evidemment, c'est peu intéressant dans le présent contexte, donc je m'arrête là.
Je n'arrive pas à comprendre pourquoi pour toi, l'axiome d'extensionnalité est "le seul vrai axiome". Les autres, c'est quoi alors ? Pourquoi l'axiome d'extensionnalité ne serait-il pas lui aussi juste de la "structure grammaticale" ?
J'essaie de me conceptualiser les maths d'une autre manière que toi, et je ne pense pas que ma façon de penser est pire que la tienne ou mauvaise tout court.
Je n'exprimais pas une opinion mais plutôt des faits bruts c'est pourquoi j'avais pris soin de m'attarder sur le fait que quand on prétend introduire a on se ment puisqu'on en parle déjà en l'appelant R. Le reste est descriptif.
Quand j'ai écrit $\exists a\forall x(x\in a \iff R(x))$, il ne faut pas se leurrer, j'aurais pu tout aussi bien écrire
$$ \exists a\forall x: [a(x)\iff R(x)]$$
Et tout le monde comprend car tout le monde a déjà intégré depuis longtemps qu'n maths on utilise des abréviations. Nous devons à la crise des fondements survenues entre 1850 et 1950 d'avoir forcé tout le monde à assumer qu'un définition c'est un axiome. Même s'il est rare de croiser quelqu'un qui te répond:
$<<$ nous j'objecte, tu l'as prouvé en supposant que $a = \sqrt{98+1/\pi}$, et pour moi, tu viens seulement de prouver que $a \neq \sqrt{98+1/\pi}$
au quotidien quand l'abrégeur n'avait pas utilisé la lettre $a$ avant, il est nécessaire de l'assumer depuis la crise.
Si tu parvenais à faire de l'axiome d'extensionnalité une simple "définition" par contre, je pense que tu pourrais direct postuler pour le prix Nobel.