Par contre, je recommande de ne pas appeler "fondement" les recherches de haute voltige que tu signales, il faut les appeler "tentatives d'unification", ça n'a rien à voir avec des fondements et ça ne fonde d'ailleurs rien du tout :-D
Je ne crois pas que tu m'aies compris: je ne dis pas qu'il ne faut pas exposer ZF évidemment. Je dis que dans certains contextes, cela n'est pas du tout nécessaire, puisque le taf se fait, qu'on ait exposé ZF ou non
dans l'unique règle $(u\in \{x\mid R\}) = R[u/x]$. (***)
c'est à dire, pour le dire autrement, en lambda-calcul pur.
Et ce que je dis est que ZF ne sert qu'à brider de manière institutionnelle les R qu'on s'autorise à utiliser. C'est donc un DEUXIEME aspect.
Dans ton analogie, les règles des échecs c'est (***)
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Je ne comprends pas bien la discussion, donc peut-être que je vais être hors-sujet.
Il me faut bien des axiomes à un moment ou à un autre pour démarrer quelque part.
J'ai choisi ceux de ZFC parce que ce sont ceux qui me plaisent, voilà tout.
Il se trouve que la science se fonde en n'admettant "rien du tout", donc en commençant par 1.
Or on a choisi le plus honnête, c'est à dire de ne pas coder dans des hiéroglyphes les choses, mais juste d'être sens ambiguité, c'est à dire de:
- préciser les parenthèses
- utiliser la chose qui a toujours été utilisée pour définir à la technique $a:=[x\mapsto ...]$ les pointillés figurant N'IMPORTE QUOI et où la lettre $x$ est vouée à servir de "trou".
Exemple de nouveau verbe: $perv: [x\mapsto (x$ mange les pieds de $x)]$
qui donne $perv (Toto) = ( Toto$ mange les pieds de $Toto)$
Quand une suite S de symboles est une phrase, on a remplacé $(x\mapsto S)$ par la notation $\{x\mid S\}$
En dehors de ça, rien d'autre.
Ca, c'est 1 et ça te fait toute la science (les éventuelles polarités négatives des sciences expérimentales sont en notion première et ça ne pose pas de problème spécifique)
Problème: c'est une théorie (sans axiome) contradictoire
Dans un DEUXIEME temps, on a donc convenu d'une tradition, d'une convention, la théorie ZF, qui exprime juste quand tu as le droit de ne pas préciser par un paragraphe de politesse que tu vas utiliser une des habituelles astuces pour prouver $0=1$.
Le choix a été très simple: L'usage de $\{x\mid R(x)\}$ est interdit quand iil y a au moins un petit doute qu'il y a une surjection intuitive sur l'univers de tous les objets possibles.
Ce choix a un avantage, il "platonise". C'est un choix qui évite les usines à gaz syntaxiques, les types, les trucs, les machins etc où on devrait vérifier au millimètre si on est pas entrain d'utiliser une "collection" magique comme $\{x\mid x\notin x\}$
Ah j'oubliais, on a remplacé "Medor mange" mange par $Medor\in Mange$ pour "assumer" l'espace entre les mots. Le $\in $ n'est que ça. On a platonisé avec l'axiome d'extensionalité (à savoir qu'il y a un monde qui "voit" les passages par valeur et ne se prononce pas en fonction du nom de l'objet mais de ce qu'il est)
Remarque: en dehors de l'extensionalité, il n'y a donc pas d'axiomes à strictement parler, même si on s'en est donné l'impression. L'axiome du choix se met très bien sous la forme que j'ai dite l'utilisation de $\{x\mid x$ est un ordinal et il n'y a pas de surjection de $x$ sur $E\})$ se met facilement en bijection avec eux "par définition".
$\{x\mid x=a$ ou $x=b\}$ est utilisable car on considère qu'il serait très très étonnant que l'univers n'ait que 2 éléments par exemple, ce qui se traduit dans ZF par l'axiome de la paire.
Voilà, en gros, c'était ça que je te disais. En conclusion, il n'ya pas d'axiomes à un chouya près et tu peux écrire tous tes livres de maths en disant:
définissons $Robert$ par $\{x\mid blabla\}$. Il suit que blabla.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Tout comme une tour a besoin de fondations, tout comme un jeu a besoin de règles, j'ai besoin de propositions primaires desquelles partir et desquelles je vais démontrer tout le reste.
@Foys : je n'ai rien compris à tes allusions, ou plutôt j'ai peur d'avoir un peu compris.
Selon toi il faudrait que la maîtresse du CP commence son cours de maths par la liste des axiomes de ZFC, c'est ça ?
Du coup à la fin de l'année elle définirait $1= \{\emptyset\}$, puis peut-être 2 et 3.
Au CE1 on découvrirait les entiers, et au CE2 on apprendrait à les additionner.
Plus sérieusement je suis d'accord qu'il faut être rigoureux mais je ne vois pas l'intérêt de bombarder le lecteur d'axiomes abscons avant de lui avoir expliqué pourquoi on en a besoin. Et je ne pense pas qu'on puisse faire de la théorie des ensembles sérieusement sans avoir déjà une certaine pratique mathématique. Regarde le fil de Julia qui a du mal avec le lemme de Zorn. Je me tue à lui expliquer que le plus important est de savoir l'appliquer à des situations "concrètes", et qu'elle pourra toujours revenir sur la démonstration plus tard, si ça l'intéresse.
Cordialement
Martial
P.S. : C'est qui, cet homme de paille ? C'est moi ou CC ? Ou les deux ?
Foys et moi ne sommes pas très éloignés sur ces points, mais je crois que sans le dire beaucoup de gens nous approuvent. Il y a cependant des différences que je précise, car j'ai (et j'espère re) enseigné dans le secondaire alors que je crois que Foys en est plus éloigné.
Mes motivations sont un peu différentes de celles de Foys, qui elles sont plutôt "sur le principe" alors que je les ai construites dans la "psychanalyse intime du jeune face à aux maths"
Mais avant une précision : personne ne parle de CP, on évoque plutôt l'âge ados tardif, voire adulte.
Foys et moi ne nous différencions pas sur le fait qu'il faut distribuer la règle du jeu (CAR ELLE EST SIMPLE, et non pas "pour rien") et il y a fort longtemps sur le forum (mais j'ai la flemme de tout résumer) j'ai détaillé énorméménent pourquoi et comment fonctionne "cette problématique".
Je reprends juste un point qui je pense échappe à tous quand on parle de ça (et c'est pour ça que j'iai évoqué la psychanalyse en mode opérette):
tu ne verras jamais un gamin qui m'a eu dire que j'étais "un bon pédagogue", mais comme tu sais, si on leur pose la question à froid, ils disent presque tous qu'ils n'ont jamais de meilleur prof. Cela provient d'une différence ESSENTIELLE entre le ressenti présent et le bilan. Par ailleurs, en tmeres de performance, j'apporte 3 à 4 pts de plus sur 20 en moyenne à niveau égal.
Le grand malheur du pédagogue aujourd'hui et je l'ai raconté des milliers de fois surle forum, c'est "de vouloir donner le sein" (j'ai énormément utilisé cette expression). L'apprenant, privé de sein dans un tel système a tendance à gueuler et, vu le crahs de l'EN et des premiers cycles universitaires de science les appreneurs prennent peur.
Mais en réalité derrière le "je ne fais pas ci, je fais ça" que tu pourras lire dans la bouche de foys ou de moi il y a la dimension ESSENTIELLE, si ce n'est la seul, du sevrage salvateur. La construction d'une distanciation (parodn je m'entraine à écrire comme le journaleux de Libé) entre le pédago et l'apprenant.
Dire à 17ans à quelqu'un "Voici la fiche de la règle du jeu, veuillez la traiter ce soir, demain on commence doucement les exercices" n'est pas que une recommandation pedago mais SURTOUT une recommandation anti-dépendance-attente-du-sein-à-têter.
Ca n'a l'air de rien, mais c'est totalement conséquent ensuite, puisque tu "réveilles" les personnes face à leur autonomie. Elles doivent s'apercevoir qu'elles existent en tant qu'espcrit critique, chercheurs indépendants, etc
L'erreur qui est souvent faite, vu que ce que je rappelle parait banal, c'est de parler "comme si le système ne s'était pas crashé", et donc comme si la solution que je signale ci-dessous ne serait "un gros apport", car "allant de soi".
Mais la réalité est autre et du coup cette solution agit COMME UN MIRACLE.
Les positions de Foys sont proches, mais elles se nourrissent moins à l'aspect psychologique que je viens d'évoquer je pense.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Christophe : moi aussi je te propose un exercice très facile : déduis l'hypothèse de Riemann (ou tous les axiomes de ZF , comme tu préfères de $0=1$ :-D
(Je te taquine encore - mais tu dois comprendre que ta consigne, sans plus de précisions, pire encore pour quelqu'un qui ne te connait pas, n'a pas de sens )
En fait la théorie des ensembles promue par Christophe, c'est un peu la théorie des ensembles de Fitch (cf internet): un lambda calcul avec des termes rajoutés comme $\in$, $\Rightarrow$, $\neg...$ et parmi les règles, une équivalence entre $x\in \lambda yA$ et $A[y:=x]$. Bon dans Fitch il y a aussi une petite restriction dont je pense qu'il la trouvera inacceptable :-D (seules les preuves normalisantes sont acceptées).
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
@Max: je me suis retenu de compliquer l'énoncé mais je savais que quelqu'un ferait cette blague et même je l'espérais. J'ai déjà dit 1000 fois que quand tu tombes sur une personne qui utilise la TDE comme ça pour prouver un truc, l'avantage c'est que c'est gagné pour lui de toute façon. Mon argument est purement psy.
Par contre, ce n'est pas naturel de prouver les axiomes de ZF comme ça.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
ne ressemble pas du tout à ce que je dis. Il est même annoncé sa consistance et prétendu qu'on ne peut quantifier que sur du dénombrable :-D
Comme je l'ai souvent dit, je vais me répéter, je me demande quand estce qu'on sortira de ce paradigme de la consistance, qui semble faire bugguer tout le monde en maths fondationnelles ou unificatrices. PAr définition et Godel un fondement ne peut bien évidemment qu'être contraidctoire. Sinon ça voudrait dire (Godel), que ses améliorations internes le modifieraient de manière externe et ce ne serait pas un fondement.
Je signale donc un truc très simple: si vous croisez des gens qui vous recommandent un système de fondement, et qu'il vous dit "on l'espère consistant", vous pouvez de suite lui répondre "je n'irai pas voir, ça ne peut pas être un fondement".
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
PAr définition et Godel un fondement ne peut bien évidemment qu'être contraidctoire. Sinon ça voudrait dire (Godel), que ses améliorations internes le modifieraient de manière externe et ce ne serait pas un fondement.
Voilà, c'est exactement ce genre de propos que je voulais dénoncer hier.
Fonder veut dire livrer une théorie récursive (expressive), pas livrer une théorie avec garantie qu'elle est consistante (ou complète).
Souhaiter la consistance de la théorie n'est pas non plus prétendre en livrer une garantie.
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
Et pour la théorie de Fitch, c'est bien de la même chose qu'il s'agit (un lambda calcul avec $t \in \lambda x E$ si et seulement si $E[x:=t]$ pour tous $t,x,E$). Bon avec une notion de preuve un peu spéciale aussi (de toute façon c'est ça ou bien tout énoncé est prouvable en moins de 20 étapes, mais un système qui a une telle propriété est inutilisable pour la moindre compréhension du monde).
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
Est-ce que tu aurais un document qui ne fait pas 100 pages où cette théorie est décrite? Parce que le philosophe qui a écrit l'article que j'ai mis en lien s'étale en compliment suivis de "on ne peut traiter que le dénombrable", etc, donc je t'avoue que j'ai eu du mal à résumer les 100 pages en en parcourant aléatoirement 5
Concernant les fondements, on connait nos désaccords, mais je crois que tu ne revendiques pas y avoir beaucoup rélfléchi. Ca fausse un peu l'échange.
Je prends avec des adages très simples, donc un peu caricaturé, ma position, qui elle est revendiquée fouillée et refouillée.
1/ On ne prouve pas la consistance de théories de toute façon (quand-bien même on dispose d'une preuve, elle est entachée de nullité au motif qu'elle utilise des axiomes dont on a pas prouvé la légitimité.
- Il n'y a pas besoin de Godel pour ça. Godel a juste trouvé un algorithme qui à toute théorie qui exprime quelque chose associe à chacune des preuves de sa consistance une preuve de 0=1, le tout de manière constructive.
-Autrement dit, il a prouvé ce que je viens de dire, mais qu'on savait déjà tous avant et avait oublié par manque d'instrospection
2/ L'erreur la plus courante est de confondre "fondements" et "unifications". Le deuxième terme renferme la plupart du temps, un mélange de découvertes d'uniformisations, de revendications de prophétisme (ie les spécialistes du truc veulent "rééduquer les foules avec leurs nouveaux axiomes"), etc. C'est le crash dont lequel sont tombés, le catagorisme, HoTT, et tout un tas de choses de ce genre.
2.1/ Bien entendu, il ne s'agit de jeter ou de critiquer injustement des systèmes, mais, lorsque leur gestation provient de recherches avancées, de les appeler des unifications (ou tentatives de) et de mettre en garde contre des volontés d'impérialismes ou d'universalisme émergeant des orgueils des producteurs
2.2/ Les maths ne sont pas la physique. Il n'existe strictement aucun risque non négligeable que des preuves "disparaissent". Théoriquement, l'ensemble des théorèmes de maths archivés par la recherche est croissant avec le temps.
2.3/ On peut pousser un peu plus loin. Il n'y a pas de théorie contradictoire. Il n'y a que des théories collapsant, c'est à dire considérées sans grand intérêt car elle ont trouvé "le chemin à leur bottom" (ie leur élément minimum, dont ensuite elles peuvent tout déduire avec leur réglèe)
2.4/ Et enfin le plus trivial : ce ne sont pas les axiomes qui comptent, mais les preuves. Une théorie ne reconnait pas des théorèmes, mais des preuves.
3/ Une fois tout ça rappelé et précisé, un fondement est une théorie dans laquelle toute théorie actuelle et future sera incluse. C'est donc une théorie inconsistance, dont l'inconsistance n'est pas grave. Car les gens ne travaillent pas avec elle, mais avec des sous-théories d'elle artisanales susceptibles d'évoluer au gré des découvertes.
4/ Il se trouve qu'on l'a trouvée (c'est la TDE + extensionalité) non pas de manière arbitraire mais en prenant juste conscience que les textes écrits, tous, jusqu'à probablement un futur lointain, sont des mots séparés par des espaces. On a donc, et c'est ça un fondement, juste identifié comment se font les définitions "actives" (c'est à dire les objets que le langage produit et du coup fait émerger des axiomes sans rien demander). Il n'y a rien d'étonnant à ce qu'elle soit contradictoire. On a gagné d'ailleurs beaucoup plus, puisqu'elle est même venue avec, sans nécessité d'inspiration, son kit de bridage qui est la cardinalité (seuls les gros objets sont contradictoires).
5/ Je conçois que C'EST LA SEULE chose pour laquelle on avait le choix, on aurait pu brider par "les objets contradictoires sont les trop complexes", mais je pense que tout le monde de bonne foi, reconnait que les bridage par la taille a tout de même de gros avantages:
- on connait et pratique l'art d'évaluer des tailles depuis le début de la science, qui a même émergé à ses début presque qu'exclusivement comme ça
- on sait définir la taille (le cardinal)
- une bonne théorie doit donner les entiers naturellement sans les ajouter, or les entiers qui sont les cardinaux des ensembles finis, sont échelonnés par eux-mêmes et il n'existe pas d'entiers absolus, ils dépendent de l'univers dans lequel ils vivent, plus un univers est grand, moins il y a d'entiers, etc.
En ce qui concerne des alternatives CONSISTANTES, j'en ai souvent signalé plein sur le forum, sans écrire des textes de 100 pages comme Fitch.
Par exemple,
- tu gardes la TDE originelle mais tu n'autorises que les preuve sans coupures. C'est un très bonne théorie soit dit en passant, mais elle a de gros inconvénients. (+++)
-Il a aussi été prouvé récemment que NF est consistante.
Mais NF est un bridage sur les axiomes, ce qui est dommage, alors que (+++) garde tous les axiomes et ne brident que les preuves.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
- tu gardes la TDE originelle mais tu n'autorises que les preuve sans coupures. C'est un très bonne théorie soit dit en passant, mais elle a de gros inconvénients. (+++)
3/ Une fois tout ça rappelé et précisé, un fondement est une théorie dans laquelle toute théorie actuelle et future sera incluse. C'est donc une théorie inconsistance, dont l'inconsistance n'est pas grave. Car les gens ne travaillent pas avec elle, mais avec des sous-théories d'elle artisanales susceptibles d'évoluer au gré des découvertes.
Il faudrait lire l'avenir pour décréter un truc pareil.
Par contre on peut prévoir large.
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
Il faudrait lire l'avenir pour décréter un truc pareil. Par contre on peut prévoir large.
C'est pour ça que je te dis que quand on tient un mécanisme assurant un $\forall avenir$ qui marche, il n'y a rien d'étonnant à ce qu'il soit unique et pérenne.
Par ailleurs l'idée de "WYSWYG" n'était pas si mal avec ZF (comme on l'a vu depuis pour des raisons que je détaillerai plus tard)
Merci pour le conseil Prawitz, je vais googler.
Le fait de ne pas avoir le modus ponens n'est pas gênant du tout, il ne passe pas informatiquement (vérifier que A = A' pour déduire B de A=>B et A' oblige à analyser des "boucles potentielles" d'en haut, on ne peut pas appeler seulement récursivement une vérification de construction)
Par contre, ce serait dommage qu'on n'ait pas
$$ \frac{A+(B\to C)}{(A\to \to C}$$
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Foys, j'ai essayé de googler, mais les trucs de Prawitz Fitch que j'ai lus ressemblent, sauf erreur, à des usines à gaz reposant plus ou moins sur les créativités de leurs auteurs (mais hélas je lis très mal l'anglais, donc j'ai peut-être loupé quelque chose).
A la fin d'un article j'ai lu que in fine, Fitch évite le paradoxe de Curry en typant ... les signes implique plutôt que les objets :-D :-D
Encore une fois ça n'a rien à voir avec ce que je recommande. Moi, je ne recommande AUCUNEMENT de rechercher une théorie consistante et je n'interdis AUCUNEMENT des règles de déduction au petit bonheur la chance comme semblent le faire Prawitz et Fitch: évidemment qu'à chaque contradiction si on enlève un des ingrédients qui l'a engendrée, l'exo finit par être difficile d'en trouver une avec les outils restant.
Ma démarche est celle de distinguer les axiomes émergeant de la langue de ceux émergeant sémantiquement de quelque chose de platonicien ou de physique, mais surtout de regarder LES PREUVES et non pas les théorèmes.
Je prends l'habituel exemple de $\forall x: a(x)=non(x(x))$ qui nous donne une phrase $A$ telle que $A=non(A)$. Je ne vois pas en quoi il y a quelque avantages à lui tourner pudiquement le dos comme si elle n'existait pas. C'est une très étrange attitude scientifique d'autant qu'elle réapparait sous la forme "je suis fausse" ou "j'implique tout" qui semblent aux gens tout aussi analysables que celle issue de Curry.
En bref, on a découvert la superposition quantique et on lui tournerait le dos. Je trouve ça idiot. Même remarque en ce qui concerne 0=1. On connait quelques géants qui forcent 0 à être égal à 1 et on décide de ne pas les regarder en face, c'est bizarre, non, d'autant que dans tout le reste des maths on accepte de calculer des distances, mais là, on ne le ferait pas pour "$distlogique(0,1) = $le $a$ ci-dessus.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Etant donné $A,B$ tels que $A=B^A$, on prouve que $A,B$ sont tous deux des singletons. C'est important de se rappeler que "ce n'est pas grave". Il n'y a rien "d'étonnant" à ce qu'il existe des preuves de vrai = faux dans les univers fondationnels. C'est juste que (par exemple) $\{x\mid x\notin x\}$ est la longueur d'une preuve de vrai = faux.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Réponses
Par contre, je recommande de ne pas appeler "fondement" les recherches de haute voltige que tu signales, il faut les appeler "tentatives d'unification", ça n'a rien à voir avec des fondements et ça ne fonde d'ailleurs rien du tout :-D
Je ne crois pas que tu m'aies compris: je ne dis pas qu'il ne faut pas exposer ZF évidemment. Je dis que dans certains contextes, cela n'est pas du tout nécessaire, puisque le taf se fait, qu'on ait exposé ZF ou non
dans l'unique règle $(u\in \{x\mid R\}) = R[u/x]$. (***)
c'est à dire, pour le dire autrement, en lambda-calcul pur.
Et ce que je dis est que ZF ne sert qu'à brider de manière institutionnelle les R qu'on s'autorise à utiliser. C'est donc un DEUXIEME aspect.
Dans ton analogie, les règles des échecs c'est (***)
Il me faut bien des axiomes à un moment ou à un autre pour démarrer quelque part.
J'ai choisi ceux de ZFC parce que ce sont ceux qui me plaisent, voilà tout.
1/ Un langage
2/ Une pratique de ce langage
Il se trouve que la science se fonde en n'admettant "rien du tout", donc en commençant par 1.
Or on a choisi le plus honnête, c'est à dire de ne pas coder dans des hiéroglyphes les choses, mais juste d'être sens ambiguité, c'est à dire de:
- préciser les parenthèses
- utiliser la chose qui a toujours été utilisée pour définir à la technique $a:=[x\mapsto ...]$ les pointillés figurant N'IMPORTE QUOI et où la lettre $x$ est vouée à servir de "trou".
Exemple de nouveau verbe: $perv: [x\mapsto (x$ mange les pieds de $x)]$
qui donne $perv (Toto) = ( Toto$ mange les pieds de $Toto)$
Quand une suite S de symboles est une phrase, on a remplacé $(x\mapsto S)$ par la notation $\{x\mid S\}$
En dehors de ça, rien d'autre.
Ca, c'est 1 et ça te fait toute la science (les éventuelles polarités négatives des sciences expérimentales sont en notion première et ça ne pose pas de problème spécifique)
Problème: c'est une théorie (sans axiome) contradictoire
Dans un DEUXIEME temps, on a donc convenu d'une tradition, d'une convention, la théorie ZF, qui exprime juste quand tu as le droit de ne pas préciser par un paragraphe de politesse que tu vas utiliser une des habituelles astuces pour prouver $0=1$.
Le choix a été très simple: L'usage de $\{x\mid R(x)\}$ est interdit quand iil y a au moins un petit doute qu'il y a une surjection intuitive sur l'univers de tous les objets possibles.
Ce choix a un avantage, il "platonise". C'est un choix qui évite les usines à gaz syntaxiques, les types, les trucs, les machins etc où on devrait vérifier au millimètre si on est pas entrain d'utiliser une "collection" magique comme $\{x\mid x\notin x\}$
Ah j'oubliais, on a remplacé "Medor mange" mange par $Medor\in Mange$ pour "assumer" l'espace entre les mots. Le $\in $ n'est que ça. On a platonisé avec l'axiome d'extensionalité (à savoir qu'il y a un monde qui "voit" les passages par valeur et ne se prononce pas en fonction du nom de l'objet mais de ce qu'il est)
Remarque: en dehors de l'extensionalité, il n'y a donc pas d'axiomes à strictement parler, même si on s'en est donné l'impression. L'axiome du choix se met très bien sous la forme que j'ai dite
$\{x\mid x=a$ ou $x=b\}$ est utilisable car on considère qu'il serait très très étonnant que l'univers n'ait que 2 éléments par exemple, ce qui se traduit dans ZF par l'axiome de la paire.
Voilà, en gros, c'était ça que je te disais. En conclusion, il n'ya pas d'axiomes à un chouya près et tu peux écrire tous tes livres de maths en disant:
définissons $Robert$ par $\{x\mid blabla\}$. Il suit que blabla.
Tout comme une tour a besoin de fondations, tout comme un jeu a besoin de règles, j'ai besoin de propositions primaires desquelles partir et desquelles je vais démontrer tout le reste.
T'inquiète c'est juste des recettes de cuisine japonaise.
Selon toi il faudrait que la maîtresse du CP commence son cours de maths par la liste des axiomes de ZFC, c'est ça ?
Du coup à la fin de l'année elle définirait $1= \{\emptyset\}$, puis peut-être 2 et 3.
Au CE1 on découvrirait les entiers, et au CE2 on apprendrait à les additionner.
Plus sérieusement je suis d'accord qu'il faut être rigoureux mais je ne vois pas l'intérêt de bombarder le lecteur d'axiomes abscons avant de lui avoir expliqué pourquoi on en a besoin. Et je ne pense pas qu'on puisse faire de la théorie des ensembles sérieusement sans avoir déjà une certaine pratique mathématique. Regarde le fil de Julia qui a du mal avec le lemme de Zorn. Je me tue à lui expliquer que le plus important est de savoir l'appliquer à des situations "concrètes", et qu'elle pourra toujours revenir sur la démonstration plus tard, si ça l'intéresse.
Cordialement
Martial
P.S. : C'est qui, cet homme de paille ? C'est moi ou CC ? Ou les deux ?
Foys et moi ne sommes pas très éloignés sur ces points, mais je crois que sans le dire beaucoup de gens nous approuvent. Il y a cependant des différences que je précise, car j'ai (et j'espère re) enseigné dans le secondaire alors que je crois que Foys en est plus éloigné.
Mes motivations sont un peu différentes de celles de Foys, qui elles sont plutôt "sur le principe" alors que je les ai construites dans la "psychanalyse intime du jeune face à aux maths"
Mais avant une précision : personne ne parle de CP, on évoque plutôt l'âge ados tardif, voire adulte.
Foys et moi ne nous différencions pas sur le fait qu'il faut distribuer la règle du jeu (CAR ELLE EST SIMPLE, et non pas "pour rien") et il y a fort longtemps sur le forum (mais j'ai la flemme de tout résumer) j'ai détaillé énorméménent pourquoi et comment fonctionne "cette problématique".
Je reprends juste un point qui je pense échappe à tous quand on parle de ça (et c'est pour ça que j'iai évoqué la psychanalyse en mode opérette):
tu ne verras jamais un gamin qui m'a eu dire que j'étais "un bon pédagogue", mais comme tu sais, si on leur pose la question à froid, ils disent presque tous qu'ils n'ont jamais de meilleur prof. Cela provient d'une différence ESSENTIELLE entre le ressenti présent et le bilan. Par ailleurs, en tmeres de performance, j'apporte 3 à 4 pts de plus sur 20 en moyenne à niveau égal.
Le grand malheur du pédagogue aujourd'hui et je l'ai raconté des milliers de fois surle forum, c'est "de vouloir donner le sein" (j'ai énormément utilisé cette expression). L'apprenant, privé de sein dans un tel système a tendance à gueuler et, vu le crahs de l'EN et des premiers cycles universitaires de science les appreneurs prennent peur.
Mais en réalité derrière le "je ne fais pas ci, je fais ça" que tu pourras lire dans la bouche de foys ou de moi il y a la dimension ESSENTIELLE, si ce n'est la seul, du sevrage salvateur. La construction d'une distanciation (parodn je m'entraine à écrire comme le journaleux de Libé) entre le pédago et l'apprenant.
Dire à 17ans à quelqu'un "Voici la fiche de la règle du jeu, veuillez la traiter ce soir, demain on commence doucement les exercices" n'est pas que une recommandation pedago mais SURTOUT une recommandation anti-dépendance-attente-du-sein-à-têter.
Ca n'a l'air de rien, mais c'est totalement conséquent ensuite, puisque tu "réveilles" les personnes face à leur autonomie. Elles doivent s'apercevoir qu'elles existent en tant qu'espcrit critique, chercheurs indépendants, etc
L'erreur qui est souvent faite, vu que ce que je rappelle parait banal, c'est de parler "comme si le système ne s'était pas crashé", et donc comme si la solution que je signale ci-dessous ne serait "un gros apport", car "allant de soi".
Mais la réalité est autre et du coup cette solution agit COMME UN MIRACLE.
Les positions de Foys sont proches, mais elles se nourrissent moins à l'aspect psychologique que je viens d'évoquer je pense.
ok, je résume :-D
Déduis de la manière la plus simple TOUS LES AXIOMES DE ZF (sauf l'extensionalité) du schéma :
$$ \forall R,u: [(u\in \{x\mid R(x)\})\iff (R(u))]$$
C'est un exercice très facile qui te permettra peut-être d'avoir envie de relire mes avis.
(Je te taquine encore - mais tu dois comprendre que ta consigne, sans plus de précisions, pire encore pour quelqu'un qui ne te connait pas, n'a pas de sens )
Par contre, ce n'est pas naturel de prouver les axiomes de ZF comme ça.
ne ressemble pas du tout à ce que je dis. Il est même annoncé sa consistance et prétendu qu'on ne peut quantifier que sur du dénombrable :-D
Comme je l'ai souvent dit, je vais me répéter, je me demande quand estce qu'on sortira de ce paradigme de la consistance, qui semble faire bugguer tout le monde en maths fondationnelles ou unificatrices. PAr définition et Godel un fondement ne peut bien évidemment qu'être contraidctoire. Sinon ça voudrait dire (Godel), que ses améliorations internes le modifieraient de manière externe et ce ne serait pas un fondement.
Je signale donc un truc très simple: si vous croisez des gens qui vous recommandent un système de fondement, et qu'il vous dit "on l'espère consistant", vous pouvez de suite lui répondre "je n'irai pas voir, ça ne peut pas être un fondement".
Fonder veut dire livrer une théorie récursive (expressive), pas livrer une théorie avec garantie qu'elle est consistante (ou complète).
Souhaiter la consistance de la théorie n'est pas non plus prétendre en livrer une garantie.
Concernant les fondements, on connait nos désaccords, mais je crois que tu ne revendiques pas y avoir beaucoup rélfléchi. Ca fausse un peu l'échange.
Je prends avec des adages très simples, donc un peu caricaturé, ma position, qui elle est revendiquée fouillée et refouillée.
1/ On ne prouve pas la consistance de théories de toute façon (quand-bien même on dispose d'une preuve, elle est entachée de nullité au motif qu'elle utilise des axiomes dont on a pas prouvé la légitimité.
- Il n'y a pas besoin de Godel pour ça. Godel a juste trouvé un algorithme qui à toute théorie qui exprime quelque chose associe à chacune des preuves de sa consistance une preuve de 0=1, le tout de manière constructive.
-Autrement dit, il a prouvé ce que je viens de dire, mais qu'on savait déjà tous avant et avait oublié par manque d'instrospection
2/ L'erreur la plus courante est de confondre "fondements" et "unifications". Le deuxième terme renferme la plupart du temps, un mélange de découvertes d'uniformisations, de revendications de prophétisme (ie les spécialistes du truc veulent "rééduquer les foules avec leurs nouveaux axiomes"), etc. C'est le crash dont lequel sont tombés, le catagorisme, HoTT, et tout un tas de choses de ce genre.
2.1/ Bien entendu, il ne s'agit de jeter ou de critiquer injustement des systèmes, mais, lorsque leur gestation provient de recherches avancées, de les appeler des unifications (ou tentatives de) et de mettre en garde contre des volontés d'impérialismes ou d'universalisme émergeant des orgueils des producteurs
2.2/ Les maths ne sont pas la physique. Il n'existe strictement aucun risque non négligeable que des preuves "disparaissent". Théoriquement, l'ensemble des théorèmes de maths archivés par la recherche est croissant avec le temps.
2.3/ On peut pousser un peu plus loin. Il n'y a pas de théorie contradictoire. Il n'y a que des théories collapsant, c'est à dire considérées sans grand intérêt car elle ont trouvé "le chemin à leur bottom" (ie leur élément minimum, dont ensuite elles peuvent tout déduire avec leur réglèe)
2.4/ Et enfin le plus trivial : ce ne sont pas les axiomes qui comptent, mais les preuves. Une théorie ne reconnait pas des théorèmes, mais des preuves.
3/ Une fois tout ça rappelé et précisé, un fondement est une théorie dans laquelle toute théorie actuelle et future sera incluse. C'est donc une théorie inconsistance, dont l'inconsistance n'est pas grave. Car les gens ne travaillent pas avec elle, mais avec des sous-théories d'elle artisanales susceptibles d'évoluer au gré des découvertes.
4/ Il se trouve qu'on l'a trouvée (c'est la TDE + extensionalité) non pas de manière arbitraire mais en prenant juste conscience que les textes écrits, tous, jusqu'à probablement un futur lointain, sont des mots séparés par des espaces. On a donc, et c'est ça un fondement, juste identifié comment se font les définitions "actives" (c'est à dire les objets que le langage produit et du coup fait émerger des axiomes sans rien demander). Il n'y a rien d'étonnant à ce qu'elle soit contradictoire. On a gagné d'ailleurs beaucoup plus, puisqu'elle est même venue avec, sans nécessité d'inspiration, son kit de bridage qui est la cardinalité (seuls les gros objets sont contradictoires).
5/ Je conçois que C'EST LA SEULE chose pour laquelle on avait le choix, on aurait pu brider par "les objets contradictoires sont les trop complexes", mais je pense que tout le monde de bonne foi, reconnait que les bridage par la taille a tout de même de gros avantages:
- on connait et pratique l'art d'évaluer des tailles depuis le début de la science, qui a même émergé à ses début presque qu'exclusivement comme ça
- on sait définir la taille (le cardinal)
- une bonne théorie doit donner les entiers naturellement sans les ajouter, or les entiers qui sont les cardinaux des ensembles finis, sont échelonnés par eux-mêmes et il n'existe pas d'entiers absolus, ils dépendent de l'univers dans lequel ils vivent, plus un univers est grand, moins il y a d'entiers, etc.
En ce qui concerne des alternatives CONSISTANTES, j'en ai souvent signalé plein sur le forum, sans écrire des textes de 100 pages comme Fitch.
Par exemple,
- tu gardes la TDE originelle mais tu n'autorises que les preuve sans coupures. C'est un très bonne théorie soit dit en passant, mais elle a de gros inconvénients. (+++)
-Il a aussi été prouvé récemment que NF est consistante.
Mais NF est un bridage sur les axiomes, ce qui est dommage, alors que (+++) garde tous les axiomes et ne brident que les preuves.
Il faudrait lire l'avenir pour décréter un truc pareil.
Par contre on peut prévoir large.
C'est pour ça que je te dis que quand on tient un mécanisme assurant un $\forall avenir$ qui marche, il n'y a rien d'étonnant à ce qu'il soit unique et pérenne.
Par ailleurs l'idée de "WYSWYG" n'était pas si mal avec ZF (comme on l'a vu depuis pour des raisons que je détaillerai plus tard)
Merci pour le conseil Prawitz, je vais googler.
Le fait de ne pas avoir le modus ponens n'est pas gênant du tout, il ne passe pas informatiquement (vérifier que A = A' pour déduire B de A=>B et A' oblige à analyser des "boucles potentielles" d'en haut, on ne peut pas appeler seulement récursivement une vérification de construction)
Par contre, ce serait dommage qu'on n'ait pas
$$ \frac{A+(B\to C)}{(A\to
(Récupéré légalement, comme d'hab).
A la fin d'un article j'ai lu que in fine, Fitch évite le paradoxe de Curry en typant ... les signes implique plutôt que les objets :-D :-D
Encore une fois ça n'a rien à voir avec ce que je recommande. Moi, je ne recommande AUCUNEMENT de rechercher une théorie consistante et je n'interdis AUCUNEMENT des règles de déduction au petit bonheur la chance comme semblent le faire Prawitz et Fitch: évidemment qu'à chaque contradiction si on enlève un des ingrédients qui l'a engendrée, l'exo finit par être difficile d'en trouver une avec les outils restant.
Ma démarche est celle de distinguer les axiomes émergeant de la langue de ceux émergeant sémantiquement de quelque chose de platonicien ou de physique, mais surtout de regarder LES PREUVES et non pas les théorèmes.
Je prends l'habituel exemple de $\forall x: a(x)=non(x(x))$ qui nous donne une phrase $A$ telle que $A=non(A)$. Je ne vois pas en quoi il y a quelque avantages à lui tourner pudiquement le dos comme si elle n'existait pas. C'est une très étrange attitude scientifique d'autant qu'elle réapparait sous la forme "je suis fausse" ou "j'implique tout" qui semblent aux gens tout aussi analysables que celle issue de Curry.
En bref, on a découvert la superposition quantique et on lui tournerait le dos. Je trouve ça idiot. Même remarque en ce qui concerne 0=1. On connait quelques géants qui forcent 0 à être égal à 1 et on décide de ne pas les regarder en face, c'est bizarre, non, d'autant que dans tout le reste des maths on accepte de calculer des distances, mais là, on ne le ferait pas pour "$distlogique(0,1) = $le $a$ ci-dessus.
Etant donné $A,B$ tels que $A=B^A$, on prouve que $A,B$ sont tous deux des singletons. C'est important de se rappeler que "ce n'est pas grave". Il n'y a rien "d'étonnant" à ce qu'il existe des preuves de vrai = faux dans les univers fondationnels. C'est juste que (par exemple) $\{x\mid x\notin x\}$ est la longueur d'une preuve de vrai = faux.