Je fais remonter ce fil pour vous informer que je viens de publier la plus grande partie de la section 2 du Chap 26, consacrée à la théorie des types de Russell, Je n'ai pas encore tout à fait fini mais j'ai pas mal avancé.
C'est annexe mais il y a en logique du premier ordre un moyen simple d'exprimer, étant donné deux formules $D,F$ dont $x$ est une variable libre, l'énoncé "l'unique objet à qui satisfait $x\mapsto D$ satisfait $x\mapsto F$" : il suffit de prendre systématiquement $\forall x (D\Rightarrow F)$. La preuve de $\exists !x D$ est à faire séparément.
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$.
Merci pour ce partage. Je n'ai jamais eu le courage de m'attaquer à la théorie qui permet de démontrer qu'une proposition est indécidable, mais c'est tout de même avec cette idée sous-jacente que j'ai commencé à lire ce que tu présentes ici (j'ai bien dit commencé). Je me reconnais quand tu parles de ceux qui n'arrivent pas à voir l'implication autrement que comme un lien de cause à effet et j'aurais tendance à soupçonner que c'est ainsi qu'elle a été pensée au début. Et pour m'auto-aider à le voir autrement je me dis que le plus simple simple est de concevoir l'implication uniquement comme une relation ensembliste (l'inclusion pour ne pas la nommer).
Cela dit, même si cela permet d'arrêter de s'énerver sur les "dérivable => continue" ou encore sur les "faux => vrai", je couine quand même à l'idée que les élèves penseront que c'est par la dérivabilité que l'on obtient la continuité et ne se poseront pas la question d'où vient la dérivabilité.
Bref mon esprit résiste encore, et doit-on ne voir l'implication que comme l'inclusion, ou pas ?
The fish doesnt think. The Fish doesnt think because the fish knows. Everything. - Goran Bregovic
[[Inutile de reproduire le message précédent. AD]]
Soc.
La différence entre inclusion et implication mathématique réside dans le rôle des variables.
On appelle "formule (de théorie des ensembles) à $n$" variables une suite de caractères construite de la manière suivante:
1°) $\Box \in \Delta$ où $\Box$ et $\Delta$ sont des lettres ou bien $\# \mathbf k$ où $\mathbf k$ est un numéro - un entier- compris entre $0$ et $n-1$
2°) $nand(\mathbf A,\mathbf B )$ où $\mathbf A$ et $\mathbf B$ sont des formules à $n$ variables
3°) $hab(C)$ où $C$ est une formule **à $n+1 $ variables**
I) Sémantique élémentaire:
La signification intuitive de ces symboles est la suivante :
$machin \in truc$ signifie "machin appartient à truc"; les ensembles sont des objets premiers de la théorie et tout est ensemble dans ce paradigme.
$nand(F,G)$ signifie que les deux phrases $F,G$ ne sont pas toutes les deux vraies.
$hab(C)$ signifie qu'il y a au moins une valeur de la nouvelle variable ($n+1$ dans la définition) pour laquelle la phrase $C$ est vraie ("$hab$" est un truc de mon crû, emprunté à la théorie des types et voulant dire "habité" si vous voulez).
Les autres symboles logiques sont des abréviations, définies comme suit:
-$"\text{non } A":=\neg A:= nand (A;A)$
-$"A\text{ et } B":= A \wedge B := \neg nand(A,B )$
-$"A\text{ ou } B":= A \vee B:= nand (\neg A, \neg B )$
-$"A \text{ implique } B":= A \Rightarrow B:= nand (A,\neg B )$
-$"A \text{ équivaut à } B":=A \Leftrightarrow B:= (A\Rightarrow B ) \wedge (B \Rightarrow A)$.
Ainsi l'implication mathématique entre $A$ et $B$ signifie qu'on n'a pas à la fois $A$ vraie et $B$ fausse - et rien d'autre (dans les logiques classiques en tout cas mais ce sont les seules qui concernent les gens avant bac+quelque chose).
Par exemple "si $4$ est un nombre premier alors $3$ est un nombre premier" est vraie.
II) Variables (à comprendre !!)
Il n'y a jamais de numéros #0,#1,#2, ... dans les formules écrites couramment par les mathématiciens. Voici ce qui se passe:
Si $n$ est un entier, $\mathbf t$ une lettre quelconque et $\mathbf P$ une formule à $n+1$ variables , alors $\{\mathbf t\mid \mathbf P \}$ est la formule à $n$ variables dans laquelle toutes les occurrences de $\mathbf t$ ont été remplacées par $n$ et tous les numéros $k$ strictement supérieurs à $n$ ont été remplacés par leur successeur (autrement dit étant donné la formule à $3$ variables $(x \in \#2) \wedge(x \in y) \wedge hab( \#3 \in x)$ (dont le sens intuitif serait "$x$ appartient à l'intersection de $\#2$ et de $y$; et $x$ possède au moins un élément"),
$\{ x \mid (x \in \#2) \wedge (x \in y )\wedge hab( \#3 \in x)\}$ est la formule à $4$ variables $(\#3 \in \#2) \wedge (\#3 \in y) \wedge hab(\#4 \in \#3)$.
$ IMPORTANT: \{\mathbf t \mid \mathbf F\}$ est donc une formule où la lettre $\mathbf t$ n'apparaît pas !!!
On dit qu'une lettre figurant dans une expression mathématique est une variable liée lorsqu'elle disparaît de l'expression lorsqu'on la met sous sa forme explicite. Ainsi, $x$ est liée dans la formule de l'exemple ci-dessus; plus généralement la lettre $m$ est liée dans $\{m \mid N\}$.
Définition: Pour tout numéro $n$, toute formule à $n$ variables $\mathbf A$ et toute lettre $\mathbf p$, on note $\exists \mathbf p \mathbf A$ la formule $hab \{\mathbf p | \mathbf A\}$; qui se lit "il existe $\mathbf p$ tel que $A$".
Dans l'exemple ci-dessus, l'énoncé à 3 variables (dans sa construction on a 3 variables puis 4 variables puis 3 variables) $\exists x\left [ (x \in \#2) \wedge (x \in y )\wedge hab(\# 3 \in x)\right ]$ dit que $(\#3 \in \#2) \wedge (\#3 \in y) \wedge hab(\#4 \in \#3)$ est habité, autrement dit qu'il y a des objets non vides dans l'intersection de $\#2$ et de $y$, celui-ci peut également s'écrire $\exists x\left [ (x \in \#2) \wedge (x \in y )\wedge \exists z( z \in x)\right ] $
Les maths ensemblistes peuvent toutes s'exprimer avec des formules à $0$ variables, construites à l'aide d'emplois répétés de $nand$ et des connecteurs logiques $\Rightarrow,\wedge,\vee, \neg$ définis ci-dessus et des notations $\{\cdot | \cdot\}$, $\exists$.
Définissons également l'abréviation "$\forall x P := \neg (\exists x \neg P)$" et qui dit qu'il n'y a aucun contre-exemple à la propriété $\{x:P\}$) (cela se lit "pour tout $x$, P").
Les formules à $1$ variables sont appelées "classes" et désignent des propriétés générales exprimées à l'aide d'une variable (qui à nouveau n'apparaît pas dans l'énoncé écrit sous sa forme complète -en "langage machine mathématique" pourrait-on dire-).
III) Inclusion et implication au sens courant.
Si $P,Q$ sont des classes, $P\subseteq Q$l'abréviation de $\neg \left ( hab \left ( \neg (P \Rightarrow Q)\right )\right )$. Cette formule est syntaxiquement différente de $P$ implique $Q$
($P\subseteq Q$ est dans ce qui précède, une formule à $0$ variables
alors que $P\Rightarrow Q$ est une formule à 1 variable).
Autrement dit, lorsque $F,G$ sont des formules à $0$ variables et $x$ est une lettre, $\{x \mid F\} \subseteq \{x \mid G\}$ n'est rien d'autre (voir notations du II) que $\forall x (F \Rightarrow G)$ et signifie que "tout objet vérifiant la propriété $F$ vérifie la propriété G".
L'absence d'explicitation des règles de quantification/liaison des variables dans les cours usuels font que les gens ressentent confusément cette différence. L'implication de la langue courante est en fait très souvent une inclusion. Par exemple l'énoncé "fumer implique de tomber malade" (peu importe sa véracité ou sa pertinence) se formalise en fait par $\{x\mid fumeur (x) \} \subseteq \{x \mid x \text { tombe malade}\}$
IV) remarques annexes sur la théorie des ensembles.
La théorie des ensembles de base assimilait classes/propriétés et ensembles. Ceci crée des contradictions (il ne peut exister d'objet $u$ égal à $\{x \mid \neg x \in x\}$ car sinon $u\in u \Leftrightarrow\neg u \in u$).
Aujourd'hui on emploie des axiomes spécifiques établissant des conditions pour affirmer que telle où telle classe va être un ensemble.
On pose $A = B:= A \subseteq B \wedge B \subseteq A$ lorsque $A,B$ sont des classes.
L'énoncé "$A = (\#0 \in x)$" (qui est aussi "$A = \{y\mid y \in x\}$ lorsque $y$ est une lettre différente de $x$)" signifie "$A$ est l'ensemble $x$" et
$P \in \{v \in G\}$ abrège $\exists v \left (P \text{ est l'ensemble }v \wedge G \right )$ où $P$ est une classe et $v$ n'apparait pas dans $P$.
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$.
Remarques: l'écriture de maths formalisées est réellement pénible; en pratique tout est écrit en prose et en abréviations. Si on n'écrit pas tout en formules come ci-dessus ce n'est pas pour des raisons philosophiques ou "pédagogiques" mais pratiques; le moindre énoncé vraiment signifiant prendrait des années à écrire (sans parler des problèmes de lisibilité même pour des énoncés courts). Même en utilisant une définition plus compacte de $\neg X$ (prendre
$nand (X,V)$ ou $V$ est un énoncé tautologique comme $\forall x (x\in x
\Rightarrow x \in x)$ sans quoi on se retrouve avec des copies de $X$)
il n'est pas évident qu'un énoncé tel que $\int_{-\infty} ^{+\infty}
\exp\left ( -\frac {x^2} 2\right ) dx = \sqrt {2\pi}$ puisse tenir sur
un disque dur, ou même ait une existence physique...Mais disqualifier le formalisme mathématique sous prétexte que "ce n'est pas comme ça que les gens font" serait du niveau de disqualifier le langage machine en informatique sous prétexte que personne n'écrit en langage machine. Celui-ci doit être documenté (en maths: nous ne sommes pas dans la situation où de nouveaux langages et hardwares apparaissent toutes les décennies) et sa documentation rendue accessible à mon avis.
Les livres "Basic set theory" (A.Levy) et "Introduction to axiomatic set theory" (G.Takeuti et W.M.Zaring) contiennent une introduction au langage ensembliste similaire.
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$.
Edit. Ma vision me joue des tours, je croyais avoir lu: " il existe une bijection" et non, "il n'existe pas de bijection". Désolé. Il n'y a pas de coquille. J'ai fait une mauvaise lecture.
Petite question pour Martial car je suis en train de lire ton livre et j'ai un truc qui me chiffonne (et qui m'a d'ailleurs toujours chiffonné lorsque j'ai eu mon premier cours de logique). Tu définis une structure à partir d'un ensemble $M$ non-vide. Quel est le statut de cet "ensemble" ? Est-ce un ensemble au sens naïf du terme ? Il semblerait bien que ça doive être le cas. En effet quel sens y aurait-il à dire que $(M,E)$ est un modèle de $ZFC$ si $M$ lui-même est un ensemble au sens de $ZFC$. Ce serait comme le serpent qui se mord la queue. Mais d'autre part si, comme je le pense, $M$ est un ensemble au sens naïf alors je suis dubitatif devant l'entreprise générale de formalisation de la théorie des ensembles. En effet, beaucoup de théorèmes de set theory vont être prouvés via la théorie des modèles qui elle-même repose sur des ensembles naïfs. Donc au final tout est naïf et les paradoxes peuvent se cacher partout ...
@Cyrano: la théorie des ensembles peut carrément "implémenter" la théorie des modèles de la manière suivante: soient $M$ un énoncé à une variable libre $\alpha$ et $R$ un énoncé à deux variables libres $\alpha, \beta$. Soit $\mathcal C$ un contexte (un ensemble de variables fini; ici "ensemble" est une structure définissable en informatique) disjoint de $\{\alpha,\beta\}$.
On définit une formule "$(M,R)\vDash F$"par induction sur la taille d'une formule $F$ de théorie des ensembles dont toutes les variables libres sont dans $\mathcal C$ (on dit "une formule du contexte $\mathcal C$"), de la manière suivante:
(iii) $(M,R)\vDash (G \Box H):= \left ((M,R)\vDash G\right ) \Box \left ((M,R)\vDash H \right)$ (avec $\Box$=$\vee,\wedge$ ou $\Rightarrow$)
(iv) $(M,R)\vDash \neg G:= \neg \left ((M,R)\vDash G \right)$
enfin, dans les clauses suivantes,$x \notin\mathcal C \cup \{\alpha,\beta\}$ et $K$ est une formule du contexte $\mathcal C \cup \{x\}$
(v) $(M,R)\vDash \exists x K := \exists x \left (M[\alpha:=x] \wedge (M,R)\vDash K \right )$
(vi) $(M,R)\vDash \forall x K := \forall x \left (M[\alpha:=x] \Rightarrow (M,R)\vDash K \right )$
Il est routinier de vérifier que pour toutes telles formules, si $\mathcal C =\{a_1,...,a_d\}$ et si $F$ est une formule de $\mathcal C$ qui est un théorème de logique du premier ordre, alors (par induction sur la taille de la preuve),
$\left (\bigwedge_{i=1}^d M[\alpha:=a_i] \right ) \wedge (M,R)\vDash F$ est un théorème de logique du premier ordre. Ainsi, tous les concepts de théorie des modèles s'importent.
Parfois $M$ est un ensemble au sens suivant: on peut montrer qu'il existe $t$ tel que pour tout $x$, $x\in t$ si et seulement si $M(x)$. Mais pas toujours (par exemple quand on veut montrer que l'axiome de fondation est consistant avec ZF sans cet axiome, $M$ va être la classe des objets dans un $V_{\alpha}$ pour au moins un ordinal, où $\alpha \mapsto V_{\alpha}$ est la hiérarchie de Von Neumann).
$R$ va être souvent $\alpha \in \beta$, bref l'appartenance elle-même.
Un livre où on voit cette idée explicitée: "Introduction to axiomatic set theory" par Takeuti et Zaring.
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, cela me rappelle mon désaccord irréductible avec CC qui prétend que les entiers intuitifs n'existent pas.
Sans admettre l'existence des objects intuitifs que sont les entiers naïfs, les signes, les assemblages de signes, et les ensembles intuitifs, il serait tout bonnement impossible de construire, ou même simplement de décrire ce que sont les théories formalisées comme PA ou ZFC, les réalisations et les modèles de ces théories, ni d'expliquer pourquoi on utilise les règles de déduction formelles de la logique classique plutôt que d'autres.
ce n'est pas parce qu'ensuite, dans ZFC on peut définir les entiers formels ( $\omega $, qui d'ailleurs ne représente qu'imparfaitement les entiers naïfs puisque il peut contenir des entiers non standard), les assemblages formels, les théories, les modèles formels, etc, qu'il faut oublier ce qui a permis ces constructions et les justifient.
C'est un peu comme si, après qu'ils ont servi à ériger le bâtiment, on rangeait soigneusement les échafaudages dans leur caisse, en prétendant de mauvaise foi qu'ils n'ont jamais existé.
Ou encore comme ces nouveaux riches qui effacent soigneusement toute trace de leurs humbles origines en prétendant qu'ils ont toujours appartenu à la famille qui les accueille.
@Cyrano : @Foys t'a répondu de façon détaillée, mais je vais quand même donner mon point de vue.
Il y a effectivement une circularité sous-jacente dans cette histoire. Les modélistes te disent que pour démontrer tel ou tel théorème on se base sur des résultats de ZFC (par exemple $\kappa \times \lambda = max(\kappa, \lambda)$ pour tous cardinaux infinis $\kappa$ et $\lambda$), et que c'est aux ensemblistes de justifier leurs résultats. Les ensemblistes appliquent Löwenheim-Skolem à tous les coins de rue en te disant que c'est aux modélistes de justifier tout ça.
En fait, tant que tu ne te spécialises que dans une de ces disciplines il n'y a pas de problème. Mais quand tu veux exposer les deux en même temps à un néophyte (c'est ce que j'essaye de faire), c'est là que les ennuis commencent.
Quand tu arriveras au Chapitre 16 tu verras qu'au début je m'étends un peu sur ces questions.
Selon mon analyse on peut adopter deux points de vue différents.
1) Soit on vit dans un monde "normal", on y fait des maths "normalement", en particulier de la théorie des modèles. On démontre le théorème de complétude, et après on dit : après tout ZFC est une théorie comme les autres, donc si elle est consistante elle a un modèle. Puis tu émets la profession de foi selon laquelle ZFC est consistante, donc elle a un modèle. (Pas besoin de AC pour démontrer le théorème de complétude dans ce cas-là puisque le langage est dénombrable). Là où les ennuis commencent c'est quand tu dis par exemple : puisque ZFC a un modèle infini, par LS elle a aussi un modèle dénombrable (résultat qui sert souvent). LS a été démontré sur la base de ZFC, et qui te dit que la preuve "tient encore" dans notre vrai monde ?
2) Soit tu considères qu'on vit déjà dans un modèle $(\mathbb{V}, \in)$ de ZFC, dans lequel on a démontré tous les théorèmes connus de théorie des modèles. Et ensuite tu t'amuses à construire des sous-modèles et des extensions génériques de $\mathbb{V}$, des modèles non standard, des modèles avec des indiscernables et toutim. Ce point de vue est celui de CC, et aussi des platoniciens en général. Au Chap 16 j'explique (peut-être que je raconte des salades) que la différence est essentiellement philosophique (voire psychologique) et qu'elle a peu d'impacts au plan strictement mathématique. Je ne prends pas réellement position mais je dis quand même à mots couverts que dans la suite on va plutôt privilégier le second point de vue.
Il y a quand même un truc qui me chiffonne avec le second point de vue, mais il y a peut-être une façon de résoudre le problème.
Quand tu veux écrire la liste des axiomes de ZFC tu dois à un moment exposer les schémas de compréhension et de remplacement. Prenons la compréhension parce que c'est plus facile (et puis il n'y a pas besoin du remplacement pour construire $\omega$). Ecrivons-le en toutes lettres :
"Pour tout entier naturel $n$ et pour toute formule $\varphi$ à $n+1$ variables libres, l'énoncé suivant est un axiome :
$$\forall x_1...\forall x_n \forall a \exists b \forall x [x \in b \leftrightarrow x \in a \land \varphi(x,x_1,...,x_n)]".$$
Problème : c'est quoi un entier naturel ? C'est quoi une formule ? Tu vois bien que pour pouvoir écrire ce truc tu as forcément consacré un chapitre (ou renvoyé à un autre bouquin) pour expliquer ce qu'est l'ensemble des formules. Et cet ensemble est parfaitement naïf, puisque construit à partir de $\mathbb{N}$, qui lui-même est un ensemble intuitif.
Alors certes on peut arithmétiser la syntaxe, mais cela ne me satisfait pas pleinement. Je vais donner mon idée dans un instant.
Voilà mon idée, je ne sais pas si elle marche. Tu commences directement par la théorie des ensembles, mais, au lieu d'énoncer le schéma de compréhension, tu listes toutes ses instances dont tu as besoin pour arriver jusqu'à la construction de $\omega$, sans oublier les axiomes du calcul des prédicats. Ça en fait beaucoup, mais un nombre fini. Une fois que tu as $\omega$ tu peux construire l'ensemble des formules, tu démontres tous les théorèmes de théorie des modèles dont tu as besoin, puis tu listes les axiomes de ZFC. Evidemment ce serait un travail de Titan, et le livre serait totalement illisible, mais j'ai l'impression qu'en théorie ça doit être faisable.
Cyrano, cela me rappelle mon désaccord irréductible avec CC qui prétend que les entiers intuitifs n'existent pas. Sans admettre l'existence des objets intuitifs que sont les entiers naïfs, les signes, les assemblages de signes, et les ensembles intuitifs, il serait tout bonnement impossible de construire, ou même simplement de décrire ce que sont les théories formalisées comme PA ou ZFC, les réalisations et les modèles de ces théories, ni d'expliquer pourquoi on utilise les règles de déduction formelles de la logique classique plutôt que d'autres.
C'est faux, on peut construire tous les systèmes de réécriture à la base des maths sans évoquer les entiers. Je rappelle qu'on construit des ordinateurs et leurs systèmes d'exploitation à partir de rien.
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 que c'est aux ensemblistes de justifier leurs résultats. Les ensemblistes appliquent Löwenheim-Skolem à tous les coins de rue en te disant que c'est aux modélistes de justifier tout ça.
Krivine démontre lui-même ce théorème dans son 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$.
@Foys : Je suis entièrement d'accord, d'où l'intérêt de leur usage au titre de la simplification des écritures.
Le point important, pour moi, étant le théorème de compacité, qui, ici, dit que toute démonstration utilisant un "schéma d'axiomes" utilise en fait un nombre fini des axiomes "représentés" par le schéma (donc pas de souci).
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Un système de réécriture est une liste finie de règles qu'on applique successivement pour produire de nouvelles chaînes de caractères à partir d'anciennes.
Pour définir le schéma de substitution, il suffit de définir ce qu'est une clôture universelle d'un ensemble $X$ de formules. C'est toute formule obtenue par application successive des règles suivantes:
-une formule de $X$ est dans la clôture universelle de $X$ (édité!)
-pour toute $F$ et toute lettre $t$, si $F$ est dans la clôture universelle de $X$ alors $\forall t F$ aussi.
Une définition inductive ne suppose en réalité rien, c'est juste une
liste d'opérations autorisées, appelant potentiellement un résultat
obtenu par ces mêmes règles. Si vous pouvez exhiber le fait que l'objet
en question a été construit en respectant toutes ces règles donnant le
droit de dire que "l'objet est un blabla", alors l'objet est un blabla (d'ailleurs à chaque fois que vous pourrez vraiment prouver que l'objet est un blabla avec ces règles, l'objet en question sera automatiquement bien fondé, peu importe ce que la règle autorise car nous vivons dans un monde essentiellement finitiste).
C'est d'ailleurs pour cela que
@GG a écrit C'est un peu comme si, après qu'ils ont servi à ériger le bâtiment, on
rangeait soigneusement les échafaudages dans leur caisse, en prétendant
de mauvaise foi qu'ils n'ont jamais existé.
Ou encore comme ces
nouveaux riches qui effacent soigneusement toute trace de leurs humbles
origines en prétendant qu'ils ont toujours appartenu à la famille qui
les accueille.
Au contraire l'idée du formalisme est de laisser l'échafaudage accessible pour ceux qui voudraient le voir même si il sera effacé pour raisons d'esthétisme, de lisibilité et de concision.
Bon je commence à mieux comprendre, merci pour ces réponses. Le fait qu'il n'y ait pas de rigueur absolue en maths et qu'on soit toujours obligé de se reposer sur du "méta" ou du "naïf" ne m'était pas inconnu mais j'avais du mal à voir comment ça pouvait s'agencer au niveau des modèles. De ce que je comprends, il y a une dialectique entre le ZFC formel et "interne" et le ZFC (ou bien pourrait-on dire "true set theory" si on est platonicien ?) externe. Un modèle $(M,E)$ du ZFC interne est un couple où $M$ est un ensemble au sens du ZFC externe. Mais évidemment ce qu'on apprend comme vérité au niveau du ZFC interne peut être retransféré à l'externe pour éviter de faire des couillonnades. Ai-je à peu près compris ?
@Foys : J'ai du mal avec la version purement informatique. Par ailleurs tu dis qu'on part de rien mais à priori pour construire un ordinateur et le faire fonctionner, on a besoin d'électricité. Or qui dit électricité, dit lampe éteinte/lampe allumée, autrement dit 0/1. Il semblerait donc bien que les deux entiers de base sont déjà présents au départ.
L'existence d'un ensemble à deux éléments n'est pas un grand acte de foi non plus...
D'autre part ce n'est pas parce que ZF permet de parler d'une échelle très riche de méta (puis de méta sur du méta etc à travers toute une hiérarchie d'univers-modèles de la théorie des ensembles imbriqués les uns dans les autres, pourvu qu'il en existe au moins un) que le recours à ce méta est indispensable pour définir ZF.
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$.
@Foys je ne vois pas comment tu peux réécrire des schéma d'axiomes sans supposer les nombres entiers intuitifs. Plus précisément, le schéma d'axiomes de substitution commence par $\forall x_1,\ldots,\forall x_k \text{ etc.}$. Tu fais comment pour réécrire ce bout de texte ?
Si vous avez un axiome à écrire avec une formule qui est quantifiée sur 5 variables, vous pouvez écrire $\forall x_1\forall x_2\forall x_3 \forall x_4 \forall x_5$, Mais vous pouvez aussi écrire $\forall a,\ \forall b,\ \forall c,\ \forall d,\ \forall e$, et exit les entiers.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
On dit qu'une formule $F$ est une instance du schéma de substitution si
(i) $F$ est de la forme $(\forall x \exists ! y G) \to \exists z \forall y (y \in z \leftrightarrow \exists x (x \in u \wedge G)$ où $G$ est une formule et $x,y,z,u$ des lettres
(ii) ou bien $F$ est de la forme $\forall t H$ où $H$ est une instance du schéma de substitution et $t$ une lettre.
À chaque fois qu'on voudra l'invoquer il faudra passer par cette phase qui établit qu'une formule est bien une instance du schéma de substitution.
Mais justement il n'y a pas qu'une formule à écrire autrement le problème serait réglé. Je vais être encore plus précis. Dans le Krivine le schéma de substitution est présenté comme suit : On voit bien que l'on utilise les entiers intuitifs. Comment s'en débarrasser selon les règles de réécriture de Foys ? Edit : j'ai posté sans me rendre compte de la réponse ci-dessus.
Il ne faut pas confondre deux choses : la liste des axiomes définissant une théorie et le but est essentiellement de la communication (un schéma d'axiomes remplis ce rôle) et la liste des axiomes dont on a besoin pour une démonstration et cette dernière liste (que l'on peut construire grâce au schéma) est finie !
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
@Foys finalement le problème est la clôture universelle d'un ensemble de formules comme tu l'as indiqué dans ton lien. Sauf que... je n'arrive pas à te déchiffrer (tu as trop côtoyé cc on dirait...). Plus précisément c'est cette affirmation que je ne comprends pas : "une formule de $X$ est dans $X$".
Ben oui si $X$ est un "ensemble" de formules alors une formule de $X$ est dans $X$. C'est quoi la différence entre ce "de" et ce "dans" ? Je parle de ton message ICI.
Moi, j'approche la théorie formelle des ensembles en prenant la théorie des modèles comme point de départ comme le fait Mr René Cori. Dans cette optique l'ensemble de base d'une structure est un ensemble intuitif. Cela fait qu'on a besoin de la théorie naïve (non formelle) des ensembles pour développer la théorie formelle des ensembles.
Après les proof-theorists ont une autre façon de faire.
@Foys ok mais dans ce cas la clôture universelle peut contenir des formules avec des variables libres. Il suffit que $X$ en ait. À moins que ça ne pose pas de problème, j'avoue être ignorant dans le domaine.
Voici ce que l'on peut lire dans le deuxième tome de Cori-Lascar, page 140 :
Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
@nicolas.patrois : de 0 à 20 c'est bon. 21 à peu près. 22 fortement déconseillé. 23 OK. 24 et 25 à peu près. 26 en cours d'écriture mais a priori ce qui est déjà écrit tient la route.
Désolé de déranger (si tel est le cas) sinon, je ne vois pas pourquoi on ne peut pas montrer par induction sur Omega que chaque élément de Omega est (edit) standard (si j'ai bien compris, cela veut dire "être l'image d'un entier intuitif"), et l'application des entiers intuitifs vers Omega, on peut la définir par recursion transfinite, si l'ensemble des entiers intuitifs est bien fondé. Je n'ai rien rédigé, mais je ne vois pas pourquoi ça ne marcherait pas, éclairez moi s'il vous plaît. Je ferais une rédaction de ça demain si ma fièvre me le permet.
Edit. Je voulais dire "standard" pas "non standard".
@Cyrano il n'existe pas vraiment de moyen réaliste d'évacuer ce problème. Soit $T$ une théorie contenant ZFC (bref lui ajoutant des axiomes). On considère une nouvelle lettre $c$ ne figurant pas dans les lettres libres de $T$ et on considère (pour $d$ chaîne de caractères écrite uniquement avec $0,1,2,...,9$ bref ce que certains appeleront un "entier intuitif") une phrase $P_d:= c \in \N \wedge \overline d < c$ où $\overline d$ est la traduction de Gödel de $d$ (bref $P_d$ est une formule gigantesque écrite uniquement avec des connecteurs et $\in$ et qui exprime que "l'entier $c$ est plus grand que $d$; par ex $P_{17}:= "17" < c$...).
1°) Si on ajoute un nombre fini de phrases $P_{d_1},...P_{d_k}$ à $T$, on ne modifie pas $T$ au sens où si $Q$ est un énoncé quelconque où $c$ ne figure pas et $\pi$ est une preuve de $Q$ à partir de $T \cup \{P_{d_i},1 \leq i \leq k\}$, on peut construire une preuve de $Q$ à partir de $T$ seul, en effet il suffit de considérer $m:= max\{d_1, d_2,...,d_k\}$ (qui est une bête liste finie de nombres explicites en base 10) et de remplacer $c$ par $m+1$ dans la preuve: chaque instance de $P_k$ va être remplacée par un banal théorème d'arithmétique valable dans $T$ puisque valable dans ZFC qu'elle étend.
On dit que $T \cup \{P_{d_1},...,P_{d_k}\}$ est une extension conservative de $T$: on a étendu le langage mais les énoncés exprimables dans le système formel de base et qui sont des théorèmes dans le nouveau système, sont des théorèmes dans l'ancien.
2°) C'est maintenant que les choses se gâtent
On considère cette fois la théorie $T'$ obtenue en rajoutant pour toutes les chaînes de caractères sur l'alphabet $\{0,1,2,...,9\}$, l'énoncé $P_{d}$ à $T$.
(on lui adjoint un nouveau schéma d'axiomes donc).
Que se passe-t-il si un énoncé $Q$ ne comportant aucune occurrence de $c$, est néanmoins prouvable dans cette nouvelle théorie $T'$?
Réponse: cet énoncé admet une preuve qui est un objet fini, où il n'y a qu'un nombre fini d'énoncés de la forme $P_{d}$. Recensons les tous: $P_{d_1}, ... P_{d_k}$; $Q$ est conséquence de $T \cup \{P_{d_i},1 \leq i \leq k\}$ et donc de $T$ comme au 1°).
Ce n'est pas une blague: on peut rajouter en toute impunité à $T$ un schéma d'axiomes qui dit ouvertement qu'il existe un entier plus grand que tous les entiers que vous pouvez écrire.
Hier j'avais proposé une histoire de pays ou il y a une infinité de banques dans un fil d'OShIne. Derrière cette comptine se cachait évidemment cette pathologie diabolique
que change élément de Omega est non standard (si j'ai bien compris, cela veut dire "être l'image d'un entier intuitif"),
Être non standard pour un élément de $\omega$ signifie ne pas être l'image d'un entier intuitif par l'application décrite dans le post de Thierry Poma.
que change élément de Omega est non standard (si j'ai bien compris, cela veut dire "être l'image d'un entier intuitif"),
Être non standard pour un élément de $\omega$ signifie ne pas être l'image d'un entier intuitif par l'application décrite dans le post de Thierry Poma.
Oui je voulais dire "standard", j'ai fait l'édit. (Heureusement que j'avais mis le sense que j'entendais, oof), merci.
Un théoricien des modèles je pense qu'il vous ferait ça avec un couple de modèles $A$ et $B$, vérifiant les axiomes de $T$, tels que l'ensemble des entiers de $A$ est strictement contenu dans celui des entiers de $B$, mais avec $A$ et $B$ élémentairement équivalents (mais comme je ne fais pas de théorie des modèles je ne suis pas sûr il faudrait l'avis d'un spécialiste).
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$.
@Foys : Que veut dire "Prouver, séparément, pour tout entier $n$ (explicite) l'énoncé $P(n)$" ? À la main, on ne peut de toute façon prouver séparément qu'un nombre fini de $P(n)$ avec $n$ explicite.
Réponses
└─ B
-- Schnoebelen, Philippe
Il semblerait bien que ça doive être le cas. En effet quel sens y aurait-il à dire que $(M,E)$ est un modèle de $ZFC$ si $M$ lui-même est un ensemble au sens de $ZFC$. Ce serait comme le serpent qui se mord la queue.
Mais d'autre part si, comme je le pense, $M$ est un ensemble au sens naïf alors je suis dubitatif devant l'entreprise générale de formalisation de la théorie des ensembles. En effet, beaucoup de théorèmes de set theory vont être prouvés via la théorie des modèles qui elle-même repose sur des ensembles naïfs. Donc au final tout est naïf et les paradoxes peuvent se cacher partout ...
Y aurait-il quelque chose qui m'échappe ?
Sans admettre l'existence des objects intuitifs que sont les entiers naïfs, les signes, les assemblages de signes, et les ensembles intuitifs, il serait tout bonnement impossible de construire, ou même simplement de décrire ce que sont les théories formalisées comme PA ou ZFC, les réalisations et les modèles de ces théories, ni d'expliquer pourquoi on utilise les règles de déduction formelles de la logique classique plutôt que d'autres.
ce n'est pas parce qu'ensuite, dans ZFC on peut définir les entiers formels ( $\omega $, qui d'ailleurs ne représente qu'imparfaitement les entiers naïfs puisque il peut contenir des entiers non standard), les assemblages formels, les théories, les modèles formels, etc, qu'il faut oublier ce qui a permis ces constructions et les justifient.
C'est un peu comme si, après qu'ils ont servi à ériger le bâtiment, on rangeait soigneusement les échafaudages dans leur caisse, en prétendant de mauvaise foi qu'ils n'ont jamais existé.
Ou encore comme ces nouveaux riches qui effacent soigneusement toute trace de leurs humbles origines en prétendant qu'ils ont toujours appartenu à la famille qui les accueille.
Le point important, pour moi, étant le théorème de compacité, qui, ici, dit que toute démonstration utilisant un "schéma d'axiomes" utilise en fait un nombre fini des axiomes "représentés" par le schéma (donc pas de souci).
J'affirme péremptoirement que toute affirmation péremptoire est fausse
C'est un peu comme si, après qu'ils ont servi à ériger le bâtiment, on rangeait soigneusement les échafaudages dans leur caisse, en prétendant de mauvaise foi qu'ils n'ont jamais existé.
Ou encore comme ces nouveaux riches qui effacent soigneusement toute trace de leurs humbles origines en prétendant qu'ils ont toujours appartenu à la famille qui les accueille.
Le fait qu'il n'y ait pas de rigueur absolue en maths et qu'on soit toujours obligé de se reposer sur du "méta" ou du "naïf" ne m'était pas inconnu mais j'avais du mal à voir comment ça pouvait s'agencer au niveau des modèles. De ce que je comprends, il y a une dialectique entre le ZFC formel et "interne" et le ZFC (ou bien pourrait-on dire "true set theory" si on est platonicien ?) externe. Un modèle $(M,E)$ du ZFC interne est un couple où $M$ est un ensemble au sens du ZFC externe. Mais évidemment ce qu'on apprend comme vérité au niveau du ZFC interne peut être retransféré à l'externe pour éviter de faire des couillonnades. Ai-je à peu près compris ?
@Foys : J'ai du mal avec la version purement informatique. Par ailleurs tu dis qu'on part de rien mais à priori pour construire un ordinateur et le faire fonctionner, on a besoin d'électricité. Or qui dit électricité, dit lampe éteinte/lampe allumée, autrement dit 0/1. Il semblerait donc bien que les deux entiers de base sont déjà présents au départ.
-- Schnoebelen, Philippe
Plus précisément, le schéma d'axiomes de substitution commence par $\forall x_1,\ldots,\forall x_k \text{ etc.}$. Tu fais comment pour réécrire ce bout de texte ?
Mais vous pouvez aussi écrire $\forall a,\ \forall b,\ \forall c,\ \forall d,\ \forall e$, et exit les entiers.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
On voit bien que l'on utilise les entiers intuitifs. Comment s'en débarrasser selon les règles de réécriture de Foys ?
Edit : j'ai posté sans me rendre compte de la réponse ci-dessus.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
@Foys finalement le problème est la clôture universelle d'un ensemble de formules comme tu l'as indiqué dans ton lien. Sauf que... je n'arrive pas à te déchiffrer
Ben oui si $X$ est un "ensemble" de formules alors une formule de $X$ est dans $X$. C'est quoi la différence entre ce "de" et ce "dans" ? Je parle de ton message ICI.
Moi, j'approche la théorie formelle des ensembles en prenant la théorie des modèles comme point de départ comme le fait Mr René Cori. Dans cette optique l'ensemble de base d'une structure est un ensemble intuitif.
Cela fait qu'on a besoin de la théorie naïve (non formelle) des ensembles pour développer la théorie formelle des ensembles.
Après les proof-theorists ont une autre façon de faire.
Je n'ai rien rédigé, mais je ne vois pas pourquoi ça ne marcherait pas, éclairez moi s'il vous plaît. Je ferais une rédaction de ça demain si ma fièvre me le permet.
Edit. Je voulais dire "standard" pas "non standard".
J'affirme péremptoirement que toute affirmation péremptoire est fausse
À la main, on ne peut de toute façon prouver séparément qu'un nombre fini de $P(n)$ avec $n$ explicite.