@Cyrano: par exemple, imaginons que Bob affronte Alice au jeu suivant: Alice choisit une chaîne de caractères x; Bob gagne s'il prouve P(x).
Alors "pouvoir prouver, séparément,pour tout n, P(n)" voudrait dire que tous les choix possibles d'Alice donnent des parties gagnables pour Bob. Mais cela ne veut pas dire qu'il a une démonstration formelle de $\forall x P(x)$.
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$.
Un autre exemple est le suivant: On considère $D(x):=x$ est une preuve de $0=1$ dans ZFC ($x$ chaîne de caractères).
Supposons $ZFC$ consistante. Alors pour toute chaîne de caractères $x$, $\neg D(x)$ est prouvable (en fait directement constatable).
Cependant une démonstration dans ZFC de $\forall x \neg D(x)$ pourrait immédiatement donner en quelques lignes supplementaires, une démonstration de $0=1$ dans ZFC par le second théorème de Gödel.
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$.
Qu'est-ce qu'un modèle de ZFC ? C'est un univers, une collection, ou quel que soit le nom qu'on lui donne, d'objets appelés ensembles (muni d'une relation binaire). Cet univers est un ensemble intuitif, et les énoncés de ZFC sont des assemblages intuitifs de signes. Maintenant, on peut dire : "Pas du tout". Cet univers est un ensemble M d'un univers M', modèle d'une théorie des ensembles T' (ZFC ou une autre, peu importe) et les énoncés de ZFC sont des suites finies d'ensembles de M' pris comme symboles. Mais alors, qu'est-ce que ce modèle M' de la théorie T' ? C'est un ensemble intuitif, et les énoncés de T' sont des assemblages intuitifs de signes. Maintenant, on peut dire : "Pas du tout". Cet univers M' est un ensemble d'un univers M'' d'une théorie T'', etc. On voit qu'on s'engage dans une absurde régression à l'infini. À un certain stade, la considération d'ensembles intuitifs, d'assemblages intuitifs, etc, est INÉVITABLE. Prétendre qu'ils n'existent pas parce qu'on les cache sous le tapis, c'est le sort des échafaudages et l'attitude du nouveau riche.
Oui, mon point de vue (en réalité celui de Mr René Cori, il me semble) c'est que d'abord, on a la théorie naïve (non formelle) des ensembles qui sert de point de départ ensuite avec cette théorie naïve des ensembles, on construit la théorie des modèles, et avec la théorie des modèles on construit la théorie formelle des ensembles qui n'est alors qu'une application de la théorie des modèles. Donc oui, dans la théorie formelle des ensembles, l'univers est un ensemble intuitif comme pour toute structure du premier ordre.
@Cyrano : En fait non; la règle de généralisation est une procédure particulière avec emploi d'une nouvelle lettre. Alors que "montrer P(n) pour chaque n explicite" voudrait dire plutôt: "on peut montrer P(0), on peut montrer P(1), on peut montrer P(2), ..., on peut montrer P(33676) ..."
On peut faire un parallèle avec l'axiome du choix: une preuve de $\forall x\in T, \ P(x)$ est un programme informatique qui à tout $t\in T$ fait correspondre une preuve de $P(t)$. Notons pour tout énoncé $E$; $\overline E$ l'ensemble des preuves de $E$ (whatever that means). Il ne va pas de soi que $\overline {\forall x \in T, P(x)} = \prod_{t\in T}\overline {P(t)}$ est non vide même si $\overline {P(s)}$ est non vide pour tout $s$, surtout dans des paradigmes (Curry-Howard) où toutes les fonctions envisagées sont des programmes informatiques (une preuve de $A\Rightarrow B$ étant un programme informatique qui transforme infailliblement une preuve de $A$ en une preuve de $B$ par exemple).
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 est clair que montrer $P(n)$ non pas indépendamment de $n$, mais en fonction de $n$, pour chaque $n$ ne couvre pas les éléments non-standard (alors que $\forall x P(x)$, si.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
@Cyrano L'intérêt de la théorie formelle des ensembles c'est que : 1) elle permet de limiter au strict minimum l'utilisation de la théorie naïve (on se repose sur aussi peu de théorèmes naïfs que possible) ; 2) la manipulation de la théorie formelle est très élégante et ne conduit pas à des erreurs (en supposant qu'il n'y a pas d'erreurs de démonstration du minimum de théorèmes naïfs dont on s'est servi) ; 3) les démonstrations en théorie formelle sont ultra-précises sans possibilité d'erreurs (encore une fois, en supposant qu'il n'y a pas d'erreurs dans les démonstrations du minimum de théorèmes naïfs). P.S. Moi ce à quoi la théorie formelle des ensembles me fait penser c'est la matrice du film Matrix.
Ah oui, j'oubliais : j'ai un jour déjeuné avec Paul Rozière (qui était dans ma classe en Terminale et en spé), Jean-Louis Krivine et un MCF dont je ne me souviens plus du nom. Au milieu d'une discussion sur la pertinence des radars fixes, Krivine nous a expliqué en 3 mots pourquoi le truc des suites de Goodstein n'est pas démontrable dans Peano.
J'ai été un des étudiants de Mr Paul Rozière en M2 LMFI. Le monde est petit.
@cohomologies et @Médiat : J'ai raté les deux à un an près (pas
dans le même sens). J'ai fait le M2 en 2003/2004. L'année d'avant
c'était Krivine qui faisait le cours de théorie des modèles / théorie
des ensembles, mon année c'était Gabriel Sabbagh. (Un grand Monsieur).
Pour le cours de récursivité / calculabilité, mon année c'était Ramez
Labib-Sami, et l'année suivante c'était... Paul Rozière.
@Médiat : je commence à comprendre pourquoi tu "touches ta bille" en théorie des modèles.
@nicolas.patrois : quand je dis "c'est bon", j'entends par là que je suis "assez content" de ce que j'ai écrit. Cela ne veut surtout pas dire qu'il n'y a pas de coquilles. D'ailleurs si tu lis attentivement tu vas sûrement en trouver pléthore.
@Cyrano : "Tiens, quels sont les axiomes "minimaux" (les plus faibles possibles) à
ajouter à ZFC pour qu'il n'y ait pas d'entiers non-standards ? "
Je viens de me rendre compte que j'avais oublié de répondre à ta question. D'autres y ont répondu avant moi mais j'aimerais ajouter mon grain de sel. Je le ferai demain. Envoie-moi un MP si j'oublie.
P.S. : Ces plantages à répétition du forum commencent à me faire ch...
À propos de la suprématie du formalisme et de la dépréciation de l'intuitif voire de son rejet pur et simple comme il semble de mise sur ce forum, j'avais été impressionné par le pamphlet de Harthong et Reeb intitulé "Intuitionnisme 84" dont voici deux extraits :
2. Voici donc - autant annoncer la couleur tout de suite - nos principales thèses: nous considérons
a) que la mathématique formelle (la théorie axiomatique des ensembles de Zermelo-Fraenkel, qu'on nous a toujours présentée, lorsque nous étions étudiants et naïfs, comme le fondement absolu et éternel de la mathématique) n'est qu'une théorie scientifique éventuellement sujette à la réfutation (nous dirons plus loin comment), une simple interprétation d'une réalité qui lui est extérieure, et non la réalité mathématique elle-même;
b) que ce qu'il y a de scientifique dans la mathématique, c'est l'articulation entre la théorie (quelle qu'elle soit) et cette réalité, et non le caractère formel et abstrait de la théorie qui n'est qu'un instrument ;
c) que cette articulation entre la théorie et la réalité repose sur la méthode expérimentale dans les sciences de la nature, mais sur la méthode constructive dans la mathématique ;
d) que, l'idéologie formaliste ayant nié cette réalité extérieure à la théorie en prétendant que la seule réalité mathématique est la théorie formelle elle-même, sa domination écrasante pendant un demi-siècle a eu pour conséquence de prendre cette théorie beaucoup trop au sérieux, d'en oublier toute la relativité historique et sémantique, d'en faire un dogme pesant et tyrannique, une langue de bois qui interdit toute expression personnelle, qui change le travail du mathématicien en publications standardisées et insipides, et les chercheurs en robots.
Et plus loin :
La correspondance des mathématiciens du début du siècle, Borel, Hadamard, Lebesgue, Zermelo, et tant d'autres montre qu'il fut une époque où l'on discutait volontiers des fondements des mathématiques. De nos jours, de telles activités contemplatives sont plutôt mal vues ; toute interrogation se voit aussitôt recouverte pudiquement d'un voile épais essentiellement cousu d'une phraséologie technique ultra-formalisée[c'est moi qui souligne]. Aujourd'hui un scientifique, en particulier un mathématicien, n'a plus rien d'un humaniste: c'est un fonctionnaire chargé d'exécuter une tâche extrêmement parcellaire. Dans ces conditions nouvelles dominent des idéologies appelées positivisme logique ou idéologie de l'expert selon lesquelles il n'y a plus de problème philosophique ou politique: tous les choix peuvent être décidés par le calcul, et en particulier le problème des fondements des mathématiques doit être décidé uniquement par du calcul logique formel ; ces idées, que nous jugeons fort malsaines, reposent sur le présupposé grossièrement faux que l'activité du mathématicien est identique à la déduction entièrement codifiée que postule toujours la logique mathématique ; au contraire selon l'intuitionnisme la logique mathématique est une théorie et l'activité mathématique humaine est une réalité qui n'a aucune raison de coïncider avec le modèle d'une machine de Turing pratiquant la déduction mécanique chère à Peano.
@cohomologies et @Médiat : J'ai raté les deux à un an près (pas
dans le même sens). J'ai fait le M2 en 2003/2004. L'année d'avant
c'était Krivine qui faisait le cours de théorie des modèles / théorie
des ensembles, mon année c'était Gabriel Sabbagh. (Un grand Monsieur).
Pour le cours de récursivité / calculabilité, mon année c'était Ramez
Labib-Sami, et l'année suivante c'était... Paul Rozière.
Petit, pas petit ?
Mr Ramez Labib-Sami, le prof le plus sympathique que j'ai jamais eu. Être son étudiant était un grand honneur pour moi.
@GG Je pense que sur ce forum il y a plus de personnes anti-formalisme que des pro-formalisme. Moi je suis pro-formalisme pour les raisons que j'ai cité plus haut.
"Idéologie formaliste" m'a littéralement fait éclater de rire, autant que m'avait fait éclater de rire la critique "Les platoniciens, ces gens qui croient en une licorne rose invisible".
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
À propos de la suprématie du formalisme et de la dépréciation de l'intuitif voire de son rejet pur et simple comme il semble de mise sur ce forum, j'avais été impressionné par le pamphlet de Harthong et Reeb intitulé "Intuitionnisme 84" dont voici deux extraits :
Jacques Harthong ? Qui a enseigné à Strasbourg ? J’ai conservé son cours de probabilités.
Algebraic symbols are used when you do not know what you are talking about. -- Schnoebelen, Philippe
Qu'un prof de probabilités déteste le formalisme, ce n'est pas surprenant. Différence entre "formaliste" et "naïf": Faisons une analogie avec des ingénieurs. On demande à un formaliste de construire une fusée, il prendra comme seul outil une barre de fer et mettra 10 ans à faire sa construction, on demande à un naïf de construire une fusée, il prendra un moteur russe, une barre de fer, des batteries nucléaires, des plans de fusée fait auparavant, peut-être même des fusées 😅, mais il aura terminé sa construction en 1 an.
Le formalisme élimine ce qui est superflu, mais prend plus de temps à mettre en pratique, et objectivement, ça demande plus d'efforts d'être formaliste. Mais ce qui est bien, c'est que l'informatique peut venir en aide au formaliste et réduire le temps nécessaire à son travail.
Je mets des numéros pour permettre aux intervenants qui le souhaitent de me répondre sans être obligés de me citer
GG a dit : À un certain stade, la considération
d'ensembles intuitifs, d'assemblages intuitifs, etc, est INÉVITABLE.
Prétendre qu'ils n'existent pas parce qu'on les cache sous le tapis,
c'est le sort des échafaudages
1°) Quand un phénomène est brutalement, irrépressiblement INEVITABLE, ce phénomène est également facile à produire. Je t'invite à trouver dans le site metamath les passages où les auteurs ont dû recourir aux "entiers ou aux ensembles intuitifs" pour construire leur programme. Le site est là: http://us.metamath.org/
2°) (Un peu hors sujet mais tu insistes avec cette expression) la condamnation morale -malheureusement très française- d'une personne qui a accédé à la richesse sans faire pour autant partie de la richesse dynastique, procède en fait d'une mentalité d'ancien régime. "Ce sale serf n'est pas à a place et doit retourner vivre dans la boue comme eux (voire pire comme nous pense l'esclave de maison)". Dans la société des droits de l'homme (il paraît que c'est ce qu'on voudrait être) l'ancien riche et le nouveau riche sont identiques en dignité et en obligations morales et ont le même droit à la vie privée.
la citation de GG a dit:
a) que la mathématique formelle (la théorie axiomatique des ensembles de Zermelo-Fraenkel,
3°) La mathématique formelle n'est pas un système particulier (ZF-NBG-Morse Kelley-whatever). Cela consiste simplement à publier les règles du jeu, support indispensable du raisonnement. Le choix particulier du ZFC Bourbakiste provient de sa très grande expressivité et du fait que la presque totalité des mathématiques (mais pas toutes!) s'y exprime.
la citation de GG a dit :
b) que ce qu'il y a de scientifique dans la
mathématique, c'est l'articulation entre la théorie (quelle qu'elle
soit) et cette réalité, et non le caractère formel et abstrait de la
théorie qui n'est qu'un instrument;
4°) Tu as déjà vu des nombres réels en vrai (et non pas des flottants dans un programme informatique)?
la citation de GG a dit: d) que, l'idéologie formaliste ayant nié cette réalité extérieure à
la théorie en prétendant que la seule réalité mathématique est la
théorie formelle elle-même,
5°) Le formalisme ne nie pas cette "réalité extérieure" (peu importe ce que ça veut dire) il dit qu'elle ne fait pas partie de l'arbitrage de l'activité mathématique correcte.
la citation de GG a dit: Aujourd'hui un scientifique, en particulier un mathématicien, n'a plus rien d'un humaniste:
6°) Ce qu'il ne faut pas lire. La plupart des membres de Bourbaki avaient en dehors de leur activité mathématique une vie militante riche. Mais peu importe: les mathématiques consistent à faire des mathématiques et pas autre chose.
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$.
@Cyrano : je réponds enfin à ta question concernant l'existence de modèles standard.
Dans son livre "Set Theory and the Continuum Hypothesis", Paul Cohen propose de rajouter un axiome (SM) à ZFC (ou à NBG) pour dire : "il existe un modèle standard de ZFC". Mais juste après il remarque que ce n'est pas une très bonne idée, car cela revient à sortir du langage du premier ordre de la théorie des ensembles. En effet, (SM) s'écrit : "$\forall \alpha \in \omega \exists n \in \mathbb{N}, \alpha=S^n(0)$", où $S$ est la fonction successeur définie par $S^n(x)=x \cup \{x\}$, et où $S^n$ désigne l'itérée nième de $S$. Tu vois donc que dans cette formule on quantifie sur $\mathbb{N}$, qui est un objet extérieur au monde de ZFC.
En fait Cohen a besoin de plus que ça : il lui faut un modèle transitif dénombrable de ZFC pour pouvoir développer sa méthode du forcing. Il postule donc l'existence d'un tel modèle, puis à la fin du livre il explique qu'en fait on peut s'en passer. Plus précisément on peut se contenter de supposer que ZFC est consistante (donc elle a un modèle) et ensuite "faire comme si" il existait un modèle transitif dénombrable de ZFC. Je pourrai développer si ça intéresse quelqu'un.
Revenons aux modèles standard proprement dits, i.e. aux modèles dans lesquels tout élément de $\omega$ est de la forme $S^n(0)$ pour un certain entier intuitif $n$. Il est facile de démontrer que si ZFC est consistante alors elle admet au moins un modèle non standard. Il y a au moins 3 méthodes pour faire ça :
1) L'argument de compacité développé ci-dessus par @Foys
2) Construction d'une ultrapuissance de l'univers $\mathbb{V}^\omega/\mathscr U$, où $\mathscr U$ est un ultrafiltre non principal sur $\omega$ : tu vois alors que la classe de la suite $(0,1,2,...,n,...)$ est strictement plus grande que tout entier standard.
3) Un argument "à la Gödel" : supposons $Cons(ZFC)$. Tu sais par le second théorème d'incomplétude que $ZFC \not \vdash Cons(ZFC)$, donc par complétude, si ZFC est consistante il existe au moins un modèle, disons $(M,E)$, de $ZFC+\neg Cons(ZFC)$. Un tel modèle est nécessairement non standard. En effet, supposons qu'il soit standard. Comme il satisfait $\neg Cons(ZFC)$, l'habitant du modèle dispose d'une démonstration de $0=1$ à partir des axiomes de ZFC. Mais, comme nous disposons des mêmes entiers que lui, nous pouvons recopier chez nous sa démonstration, et on arrive à $ZFC \vdash 0=1$, i.e. $\neg Cons(ZFC)$, contradiction avec l'hypothèse.
Si l'ensemble des entiers non standard est non vide, alors il a un minimum $\gamma$, $\gamma$ n'est pas 0 et $\gamma\in \omega$ , donc $\gamma$ est un successeur, soit $\delta :=\gamma -1$, on a $\delta < \gamma $ donc $\delta$ est standard, or $\gamma $ est le successeur de $\delta$, donc $\gamma $ est standard. Donc nous avons une contradiction.
Qui peut me dire ce qui cloche dans ce raisonnement ?
@Martial : Merci pour cette réponse. Le truc que je n'ai toujours pas compris c'est si on a bien $$ZFC \vdash \text{il existe un entier non standard}$$ ou non. Foys parlait d'extension conservative ce qui me laisse penser que $ZFC$ seul ne suffit pas à prouver ce fait.
@Foys : Si je prends une page au hasard de metamath : http://us.metamath.org/mpeuni/eirr.html je vois des entiers intuitifs absolument partout. Ils n'ont peut-être pas été utilisés pour concevoir le programme mais ils sont essentiels pour pouvoir communiquer. En ce sens ils sont bel et bien inévitables. (Le fait de savoir s'ils existent "réellement" dans un monde platonique ou autre est une question purement philosophique, je pense que ce n'est pas l'enjeu ici) De plus, comme on l'a déjà remarqué un ordinateur a naturellement $0$ et $1$ intégrés dans son fonctionnement. Ce que j'avais oublié de mentionner, c'est qu'un ordinateur est aussi muni de "switch" permettant d'allumer ou d'éteindre les lampes, donc d'une fonction qui fait passer $0$ à $1$ et $1$ à $0$. D'une certaine façon c'est la fonction successeur et donc tous les entiers intuitifs sont dans la machine même s'ils s'expriment en base $2$.
S'il est facile de démontrer l'existence d'un modèle non standard on va voir en revanche qu'on ne peut pas, sur la base de la simple consistance de ZFC, prouver l'existence d'un modèle standard. Supposons que $ZFC+Cons(ZFC) \vdash$ "il existe un modèle standard", soit $(M,E)$. Comme il dispose des mêmes entiers que nous, l'habitant du modèle peut, de chez lui, recopier la preuve du théorème de complétude, donc il sait qu'il existe, chez lui, un modèle $(N,E')$ de ZFC. Mais nous, qui voyons le modèle $(N,E')$ à l'intérieur du modèle $(M,E)$, pouvons en déduire qu'il existe un modèle de $ZFC+Cons(ZFC)$. Par la partie facile du théorème de complétude, c'est donc que la théorie $ZFC+Cons(ZFC)$est consistante.
Moralité : on a prouvé que $ZFC+Cons(ZFC) \vdash Cons(ZFC+Cons(ZFC))$, ce qui est interdit par Gödel.
Conclusion : la théorie $ZFC+$ "il existe un modèle standard de ZFC" est strictement plus forte que $ZFC+Cons(ZFC)$, et elle entraîne $Cons(ZFC+Cons(ZFC))$. Le même argument montre que l'existence d'un modèle standard entraîne $Cons(ZFC+Cons(ZFC+Cons(ZFC+Cons(ZFC)))$, and so on.
@cohomologies : la réponse est très simple. Si $(M,E)$ est un modèle non standard de ZFC, alors l'ensemble des entiers non standard n'existe pas.
Preuve : il suffit de recopier ton message ci-dessus. Si un tel ensemble existait blablabla, contradiction.
Pire : ce truc n'est même pas une classe propre, car, si c'était une classe (définissable), comme elle est incluse dans $\omega$, par remplacement ce serait un ensemble, contradiction.
Donc la "tribu" des entiers non standard n'existe tout simplement pas au sens de ZFC.
@Cyrano : non, ZFC ne démontre pas qu'il existe un entier non standard. Sinon ça voudrait dire qu'il n'existe pas de modèles standard. Plus précisément elle démontre qu'il existe un modèle non standard, et elle ne démontre pas qu'il existe un modèle standard. Mais cela ne veut pas dire qu'il n'en existe pas.
La situation est un peu comparable aux cardinaux inaccessibles. Notons $CI$ l'hypothèse "il existe un cardinal (fortement) inaccesssible".
$ZFC+CI \vdash Cons(ZFC)$. ZFC ne démontre pas CI, et $Cons(ZFC)$ n'entraîne pas $Cons(ZFC+CI)$. Mais à ce jour on ne dispose pas, dans ZFC, d'une preuve de $\neg CI$. (Thanks God, car sinon il y a beaucoup de settheorists qui se retrouveraient à Pôle emploi du jour au lendemain).
Cyrano a dit : @Foys : Si je prends une page au hasard de metamath : http://us.metamath.org/mpeuni/eirr.html je vois des entiers intuitifs absolument partout. Ils n'ont peut-être pas été utilisés pour concevoir le programme mais ils sont essentiels pour pouvoir communiquer. En ce sens ils sont bel et bien inévitables.
Il ne s'agit en l'espèce que de numéros pour référencer des parties du texte. On pourrait les enlever totalement, en rendant le texte encore moins lisible. Ils ne sont l'objet d'aucun raisonnement, c'est comme les numéros des pages d'un livre.
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$.
J'en rajoute une petite couche : La formule dépendant de $x$ définie par $\exists y (s^5(y)=x)$ est-elle une formule utilisable dans AP (arithmétique de Peano) ? 1) clairement NON, puisque ni l'exponentiation, ni 5 ne sont des éléments du langage, néanmoins, tout le monde la comprend. 2) clairement OUI, puisque c'est juste une façon facilement lisible d'écrire $\exists y (s(s(s(s(s(y)))))=x)$
Si on remplace 5 par 1000 ou par gogolplex, c'est même la seule façon d'écrire ces formules.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Dans la construction de l'ensemble des termes du langage L avec laquelle je travaille (dans une partie du monoïde libre de base L), $\exists y\ s^5y=x$ prend tout son sens. L'exponentiation correspond à l'exponentiation associée à la loi du monoïde, cette dernière étant notée multiplicativement.
Édit. A la modération : la syntaxe de $\exists y\ s^5y=x$ est correcte (donc j'ai enlevé la virgule que vous aviez placé juste après le quantificateur, mais merci pour l'intention), cependant, si on voulait être correct à 100% alors on choisirait un tout nouveau symbole pour "=" (disons $\sim$) et on le noterait en préfixe : $\exists y \sim s^5y x$. Mais sous cette forme ça choquerait trop les gens.
Et comment définissez-vous cela sans utiliser des entiers naïfs ? Que cela ait du sens, je le sais bien, d'ailleurs, c'est ce que je dis dans mon message.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Pour en revenir aux entiers "intuitifs", ils sont en tout cas utilisés pour certaines démonstrations (méta-démonstrations en fait) portant sur les énoncés de ZFC. Il y a des propositions dans le Krivine dont la méta-démonstration commence par "On montre, par récurrence (au sens intuitif) sur la longueur de l'énoncé que..." . La longueur de l'énoncé étant un entier intuitif.
raoul.S Lorsqu'il fait cela, Krivine donne des instructions au lecteur pour qu'il puisse, pour chaque énoncé donné, construire une certaine preuve. Ce sont des algorithmes inductifs servant à construire des schémas de théorèmes (un par énoncé différent). [Inutile de reproduire le message précédent. AD]
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$.
@Martial et @Foys Pourquoi ne peut-on pas faire un raisonnement par induction sur l'ensemble intuitif des entiers non standards ? Mon raisonnement plus haut peut s'y appliquer, n'est-ce pas ? (Car l'ensemble intuitif qui a les mêmes éléments que $\omega$ reste bienfondé). Rappel et modification (plutôt que de parler de l'ensemble, je parle de l'ensemble intuitif). Si l'ensemble intuitif des éléments non standards de $\omega$ est non vide, alors il a un minimum γ, γ n'est pas 0 et γ∈ω , donc γ est un successeur, soit δ:=γ−1, on a
δ<γ donc δ est standard, or γ est le successeur de δ, donc γ est standard.
Donc nous avons une contradiction. Il doit y avoir une erreur quelque part, encore une fois, sinon il n'y aurait jamais de non standard.
cohomologies, tu peux démontrer que toute classe propre d'ordinaux a un plus petit élément mais les entiers non-standards ne sont même pas une classe propre. Donc tu ne peux pas dire qu'il sont bien ordonnés à priori...
@cohomologies et @raoul.S : ni même a posteriori. La "collection" des entiers non standard n'est pas bien ordonnée (si elle est non vide) pour la raison suivante : soit $\alpha$ un entier non standard. Comme il n'est pas nul il a un prédécesseur $\alpha -1$, qui lui-même a un prédécesseur $\alpha-2$ etc. Donc l'ensemble
@Martial C'est une suite strictement décroissante d'ordinaux que tu viens de construire, mais la classe des ordinaux munie de l'appartenance est bienfondée. Cela contredit l'existence des entiers non standard. @raoul.S je ne parlais pas de "classe" mais d'ensemble intuitif.
Édit. Désolé j'ai répondu un peu vite car j'avais un problème de voisinage. @raoul.S ta remarque est très pertinente (je t'ai répondu beaucoup trop vite), j'ai essayé de contourner cette histoire de "non classe" en parlant directement de l'ensemble intuitif dont les éléments sont les non standard.
@Médiat_Suprème Merci, ta réponse a montré l'erreur dans ma démo. Et tu l'as fait avec moins de 2 lignes. En effet, j'ai eu tord de dire que l'ensemble intuitif des éléments de $\omega$ était bienfondé. Excusez moi les gars, je suis hors de ma zone de confort avec ces non standard. Et je vous remercie pour vos éclaircissements, surtout @Martial et @Médiat_Suprème et @raoul.S. Plutôt que de prendre autant de votre temps je devrais chercher sur une feuille un peu. Vous êtes les meilleurs. Merci. (La prochaine fois, je cherche sur une feuille avant d'écrire sur le forum, ma promesse).
Par contre cette histoire de suite strictement décroissante d'ordinaux m'intrigue. Je vais étudier ça demain.
Pas de problème, au contraire, c'est la raison d'être d'un tel forum. Une application sympa des suites décroissantes d'ordinaux : les suites de Goodstein.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Réponses
C'est la même chose que de dire je peux lister tous les entiers, alors que quelques soit l'étape je n'en ai listé qu'un nombre fini
J'affirme péremptoirement que toute affirmation péremptoire est fausse
C'est un univers, une collection, ou quel que soit le nom qu'on lui donne, d'objets appelés ensembles (muni d'une relation binaire).
Cet univers est un ensemble intuitif, et les énoncés de ZFC sont des assemblages intuitifs de signes.
Maintenant, on peut dire : "Pas du tout". Cet univers est un ensemble M d'un univers M', modèle d'une théorie des ensembles T' (ZFC ou une autre, peu importe) et les énoncés de ZFC sont des suites finies d'ensembles de M' pris comme symboles.
Mais alors, qu'est-ce que ce modèle M' de la théorie T' ?
C'est un ensemble intuitif, et les énoncés de T' sont des assemblages intuitifs de signes.
Maintenant, on peut dire : "Pas du tout". Cet univers M' est un ensemble d'un univers M'' d'une théorie T'', etc.
On voit qu'on s'engage dans une absurde régression à l'infini. À un certain stade, la considération d'ensembles intuitifs, d'assemblages intuitifs, etc, est INÉVITABLE. Prétendre qu'ils n'existent pas parce qu'on les cache sous le tapis, c'est le sort des échafaudages et l'attitude du nouveau riche.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
L'intérêt de la théorie formelle des ensembles c'est que :
1) elle permet de limiter au strict minimum l'utilisation de la théorie naïve (on se repose sur aussi peu de théorèmes naïfs que possible) ;
2) la manipulation de la théorie formelle est très élégante et ne conduit pas à des erreurs (en supposant qu'il n'y a pas d'erreurs de démonstration du minimum de théorèmes naïfs dont on s'est servi) ;
3) les démonstrations en théorie formelle sont ultra-précises sans possibilité d'erreurs (encore une fois, en supposant qu'il n'y a pas d'erreurs dans les démonstrations du minimum de théorèmes naïfs).
P.S. Moi ce à quoi la théorie formelle des ensembles me fait penser c'est la matrice du film Matrix.
Le monde est petit.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
J'affirme péremptoirement que toute affirmation péremptoire est fausse
-- Schnoebelen, Philippe
@GG
Je pense que sur ce forum il y a plus de personnes anti-formalisme que des pro-formalisme. Moi je suis pro-formalisme pour les raisons que j'ai cité plus haut.
"Idéologie formaliste" m'a littéralement fait éclater de rire, autant que m'avait fait éclater de rire la critique "Les platoniciens, ces gens qui croient en une licorne rose invisible".
J'affirme péremptoirement que toute affirmation péremptoire est fausse
-- Schnoebelen, Philippe
Différence entre "formaliste" et "naïf":
Faisons une analogie avec des ingénieurs.
On demande à un formaliste de construire une fusée, il prendra comme seul outil une barre de fer et mettra 10 ans à faire sa construction, on demande à un naïf de construire une fusée, il prendra un moteur russe, une barre de fer, des batteries nucléaires, des plans de fusée fait auparavant, peut-être même des fusées 😅, mais il aura terminé sa construction en 1 an.
Le formalisme élimine ce qui est superflu, mais prend plus de temps à mettre en pratique, et objectivement, ça demande plus d'efforts d'être formaliste. Mais ce qui est bien, c'est que l'informatique peut venir en aide au formaliste et réduire le temps nécessaire à son travail.
À un certain stade, la considération d'ensembles intuitifs, d'assemblages intuitifs, etc, est INÉVITABLE. Prétendre qu'ils n'existent pas parce qu'on les cache sous le tapis, c'est le sort des échafaudages
et l'attitude du nouveau riche.
2°) (Un peu hors sujet mais tu insistes avec cette expression) la condamnation morale -malheureusement très française- d'une personne qui a accédé à la richesse sans faire pour autant partie de la richesse dynastique, procède en fait d'une mentalité d'ancien régime. "Ce sale serf n'est pas à a place et doit retourner vivre dans la boue comme eux (voire pire comme nous pense l'esclave de maison)". Dans la société des droits de l'homme (il paraît que c'est ce qu'on voudrait être) l'ancien riche et le nouveau riche sont identiques en dignité et en obligations morales et ont le même droit à la vie privée.
3°) La mathématique formelle n'est pas un système particulier (ZF-NBG-Morse Kelley-whatever). Cela consiste simplement à publier les règles du jeu, support indispensable du raisonnement. Le choix particulier du ZFC Bourbakiste provient de sa très grande expressivité et du fait que la presque totalité des mathématiques (mais pas toutes!) s'y exprime.
4°) Tu as déjà vu des nombres réels en vrai (et non pas des flottants dans un programme informatique)?
d) que, l'idéologie formaliste ayant nié cette réalité extérieure à la théorie en prétendant que la seule réalité mathématique est la théorie formelle elle-même,
5°) Le formalisme ne nie pas cette "réalité extérieure" (peu importe ce que ça veut dire) il dit qu'elle ne fait pas partie de l'arbitrage de l'activité mathématique correcte.
Aujourd'hui un scientifique, en particulier un mathématicien, n'a plus rien d'un humaniste:
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Si l'ensemble des entiers non standard est non vide, alors il a un minimum $\gamma$, $\gamma$ n'est pas 0 et $\gamma\in \omega$ , donc $\gamma$ est un successeur, soit $\delta :=\gamma -1$, on a
$\delta < \gamma $ donc $\delta$ est standard, or $\gamma $ est le successeur de $\delta$, donc $\gamma $ est standard.
Donc nous avons une contradiction.
Qui peut me dire ce qui cloche dans ce raisonnement ?
@Foys : Si je prends une page au hasard de metamath : http://us.metamath.org/mpeuni/eirr.html je vois des entiers intuitifs absolument partout. Ils n'ont peut-être pas été utilisés pour concevoir le programme mais ils sont essentiels pour pouvoir communiquer. En ce sens ils sont bel et bien inévitables. (Le fait de savoir s'ils existent "réellement" dans un monde platonique ou autre est une question purement philosophique, je pense que ce n'est pas l'enjeu ici) De plus, comme on l'a déjà remarqué un ordinateur a naturellement $0$ et $1$ intégrés dans son fonctionnement. Ce que j'avais oublié de mentionner, c'est qu'un ordinateur est aussi muni de "switch" permettant d'allumer ou d'éteindre les lampes, donc d'une fonction qui fait passer $0$ à $1$ et $1$ à $0$. D'une certaine façon c'est la fonction successeur et donc tous les entiers intuitifs sont dans la machine même s'ils s'expriment en base $2$.
La formule dépendant de $x$ définie par $\exists y (s^5(y)=x)$ est-elle une formule utilisable dans AP (arithmétique de Peano) ?
1) clairement NON, puisque ni l'exponentiation, ni 5 ne sont des éléments du langage, néanmoins, tout le monde la comprend.
2) clairement OUI, puisque c'est juste une façon facilement lisible d'écrire $\exists y (s(s(s(s(s(y)))))=x)$
Si on remplace 5 par 1000 ou par gogolplex, c'est même la seule façon d'écrire ces formules.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Dans la construction de l'ensemble des termes du langage L avec laquelle je travaille (dans une partie du monoïde libre de base L), $\exists y\ s^5y=x$ prend tout son sens. L'exponentiation correspond à l'exponentiation associée à la loi du monoïde, cette dernière étant notée multiplicativement.
Édit. A la modération : la syntaxe de $\exists y\ s^5y=x$ est correcte (donc j'ai enlevé la virgule que vous aviez placé juste après le quantificateur, mais merci pour l'intention), cependant, si on voulait être correct à 100% alors on choisirait un tout nouveau symbole pour "=" (disons $\sim$) et on le noterait en préfixe : $\exists y \sim s^5y x$. Mais sous cette forme ça choquerait trop les gens.
Que cela ait du sens, je le sais bien, d'ailleurs, c'est ce que je dis dans mon message.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Lorsqu'il fait cela, Krivine donne des instructions au lecteur pour qu'il puisse, pour chaque énoncé donné, construire une certaine preuve. Ce sont des algorithmes inductifs servant à construire des schémas de théorèmes (un par énoncé différent).
[Inutile de reproduire le message précédent. AD]
Pourquoi ne peut-on pas faire un raisonnement par induction sur l'ensemble intuitif des entiers non standards ?
Mon raisonnement plus haut peut s'y appliquer, n'est-ce pas ? (Car l'ensemble intuitif qui a les mêmes éléments que $\omega$ reste bienfondé).
Rappel et modification (plutôt que de parler de l'ensemble, je parle de l'ensemble intuitif).
Si l'ensemble intuitif des éléments non standards de $\omega$ est non vide, alors il a un minimum γ, γ n'est pas 0 et γ∈ω , donc γ est un successeur, soit δ:=γ−1, on a
Il doit y avoir une erreur quelque part, encore une fois, sinon il n'y aurait jamais de non standard.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
C'est une suite strictement décroissante d'ordinaux que tu viens de construire, mais la classe des ordinaux munie de l'appartenance est bienfondée. Cela contredit l'existence des entiers non standard.
@raoul.S je ne parlais pas de "classe" mais d'ensemble intuitif.
Édit. Désolé j'ai répondu un peu vite car j'avais un problème de voisinage. @raoul.S ta remarque est très pertinente (je t'ai répondu beaucoup trop vite), j'ai essayé de contourner cette histoire de "non classe" en parlant directement de l'ensemble intuitif dont les éléments sont les non standard.
Merci, ta réponse a montré l'erreur dans ma démo. Et tu l'as fait avec moins de 2 lignes.
En effet, j'ai eu tord de dire que l'ensemble intuitif des éléments de $\omega$ était bienfondé.
Excusez moi les gars, je suis hors de ma zone de confort avec ces non standard. Et je vous remercie pour vos éclaircissements, surtout @Martial et @Médiat_Suprème et @raoul.S. Plutôt que de prendre autant de votre temps je devrais chercher sur une feuille un peu. Vous êtes les meilleurs. Merci. (La prochaine fois, je cherche sur une feuille avant d'écrire sur le forum, ma promesse).
Par contre cette histoire de suite strictement décroissante d'ordinaux m'intrigue. Je vais étudier ça demain.
Une application sympa des suites décroissantes d'ordinaux : les suites de Goodstein.
J'affirme péremptoirement que toute affirmation péremptoire est fausse