Bonjour tout le monde !
Je découvre depuis peu les axiomes de ZF, et je trouve que certaines choses ne sont pas claires dans l'énoncé du schéma d'axiomes de substitution/remplacement tel que j'ai pu le trouver dans différents ouvrages ou autres documents.
Tout d'abord, voici sous quelle forme j'ai choisi les axiomes en question pour ce message (\(R\) désigne une formule ensembliste) : $$ \forall p_1,...,p_n \ \forall A \ {\Huge[} {\huge(} \forall x \forall y \forall z \ {\Large[} ( R) \wedge (R [y \leftarrow z]) {\Large]} \Rightarrow y=z {\huge)} \Rightarrow {\huge(} \exists B \ \forall y \ {\Large[} \ y \in B \Leftrightarrow {\large(} \exists x \in A \ \ (R) {\large)} \ {\Large]} {\huge)} {\Huge]} $$ Ce que je ne trouve pas clair, c'est les conditions qu'on doit imposer à R, x, y, z, A et B pour que la formule ci-dessus soit bien un axiome de substitution. C'est ma question et le sujet de ce message.
\({\large[}\)
Avant de poursuivre, je précise les notations que j'utilise dans la suite :pour
toute formule \(R\) :
\( \ \ \ \ V(R)\) désigne l'ensemble des variables de \(R\)
\( \ \ \ \ FV(R)\) désigne l'ensembles des variables libres de \(R\)
\( \ \ \ \ \bar { \forall } \ R\) désigne une cloture universelle quelconque de \(R\)\({\large]}\)
J'ai cherché une réponse dans différents livres et cours d'université. Le problème, c'est que les sources divergent sur ce point, voire ne mentionnent aucune condition.
Deux choses me
semblent évidentes néanmoins :
* x, y, z, A et B doivent être distinctes les unes des autres
* z ne doit pas figurer dans \(R\)
* Aucune occurrence libre de \(B\) ne doit figurer dans \(R\) (Par exemple, si \(R\) est la formule \( x=y \wedge x \notin B\), on arrive à une contradiction)
Certains auteurs imposent d'autres conditions. Dehornoy, par exemple, impose \(A \notin FV(R)\), tandis que pour Krivine, x et y sont des variables libres de R (et pas seulement des variables éventuelles de R).
Il me semble que ces conditions ne sont pas nécessaires pour les raisons suivantes :
Supposons que l'énoncé du schéma d'axiomes soit le suivant :
\(\boxed{\text{Soient x, y, z, A et B cinq variables distinctes les unes des autres.} \\ \text{Soit R une formule ensembliste.} \\ \text{Soit } S_R \text{ la formule suivante :} \\ \quad \quad \bar { \forall } \ \forall A \ {\Huge[} {\huge(} \forall x \forall y \forall z \ {\Large[} ( R) \wedge (R [y \leftarrow z]) {\Large]} \Rightarrow y=z {\huge)} \Rightarrow {\huge(} \exists B \ \forall y \ {\Large[} \ y \in B \Leftrightarrow {\large(} \exists x \in A \ \ (R) {\large)} \ {\Large]} {\huge)} {\Huge]} \\ \text{Si } z \notin V(R) \text{, } x \in FV(R) \text{, } y \in FV(R) \text{, } A \notin FV(R) \text{ et } B \notin FV(R) \text{, } \text{alors } S_R \text { est un axiome de substitution en R.}}\)
Si maintenant, étant données 5 variables distinctes x, y, z, A et B, on se donne simplement une formule \(R\) telle que \(z \notin V(R)\) et \(B \notin FV(R)\), sans conditions sur x, y, ou A :
Soit \(a \notin \{ x, y, z, A , B\}\) une variable ne figurant pas dans \(R\).
Soit \(P\) la formule \(x=x \wedge y=y \wedge (R[A \leftarrow a])\).
Alors x, y, z, A, B et P vérifient bien les conditions imposées, donc \(S_P\) est bien un axiome de substitution en \(P\). Ensuite, à partir de \(S_P\), on déduit \(^{(1)}\) \(S_R \) . Donc on peut affaiblir les hypothèses dans l'énoncé du schéma d'axiomes et laisser x et y tranquilles (elles peuvent ou non figurer dans R, être libres ou liées), et autoriser les occurrences libres de \(A\) dans \(R\).
Le problème, c'est que je ne suis pas du tout sûr de ce que j'ai fait (cf ci-dessous). Je ne maitrise pas les raisonnements portant sur les formules, c'est un peu au feeling, et je mélange certainement syntaxe et sémantique. Donc j'aimerais avoir vos lumières sur la question. Quelles propriétés doivent vérifier une formule R et des variables x, y, z, A et B pour que \(S_R\) soit bien un axiome de substitution en R ? Et surtout, comment vous faites pour savoir ça, étant donnée la faible cohérence des sources sur le sujet ?
Merci !
\(^{(1)}\) ma démonstration de \(S_P \Rightarrow S_R\) :
Soient \(p_1,...,p_n\) les variables libres de \(R\) autres que x, y ou A. Alors, à une cloture universelle près, \(S_P\) est la formule : $$ \forall p_1,...,p_n \ \forall a \ \forall A \ {\Huge[} {\huge(} \forall x \forall y \forall z \ {\Large[} (P) \wedge (P [y \leftarrow z]) {\Large]} \Rightarrow y=z {\huge)} \Rightarrow {\huge(} \exists B \ \forall y \ {\Large[} \ y \in B \Leftrightarrow {\large(} \exists x \in A \ \ (P) {\large)} \ {\Large]} {\huge)} {\Huge]} $$ Soit T l'ensemble des axiomes de substitution (obtenus d'après le schéma d'axiomes tel qu'énoncé dans l'encadré). Donc \(S_P \in T\).
Dans un modèle quelconque de T :
Soient \(p_1\),..., et \(p_n\). Soit A. On suppose \(\forall x \forall y \forall z \ {\Large[} (R) \wedge (R[y \leftarrow z]) {\Large]} \Rightarrow y=z. \quad \ \ \ \ \ (1)\)
\(A = A\) donc \(\exists a \ a=A\). Soit un tel \(a\).
Soient x, y et z tels que \(P\) et \(P[y \leftarrow z]\). Alors \(R[A \leftarrow a]\) et \({\large[}R[A \leftarrow a]{\large]}[y \leftarrow z]\).
Donc, comme \(a=A\), on a \(R\) et \(R[y \leftarrow z]\) (
Là, il me semble que \({\large[}R[A \leftarrow a]{\large]}[y \leftarrow z]\) est équivalent à \(R[y \leftarrow z]\), mais c'est seulement au feeling. J'ai besoin d'une confirmation.)
Donc, d'après l'hypothèse \((1)\) ci-dessus, on a \(y=z\).
Donc : \( \forall x \forall y \forall z \ {\Large[} (P) \wedge (P[y \leftarrow z]) {\Large]} \Rightarrow y=z\).
Donc, d'après \(S_P\), \( \exists B \ \forall y \ {\Large[} \ y \in B \Leftrightarrow {\large(} \exists x \in A \ \ (P) {\large)} {\large]}\). Soit un tel B. Alors pour tout \(y\) : \( {\large(} y \in B {\large)} \) est équivalent à \({\Large(} \exists x \in A \ {\large[} x=x \wedge y=y \wedge (R[A \leftarrow a]) {\large]} {\Large)}\), qui est équivalent à \({\large(} \exists x \in A \ \ (R) {\large)}\).
Donc \( \exists B \ \forall y \ {\Large[} \ y \in B \Leftrightarrow {\large(} \exists x \in A \ \ (R) {\large)} {\large]}\).
Donc \( {\huge(} \forall x \forall y \forall z \ {\Large[} (R) \wedge (R[y \leftarrow z]) {\Large]} \Rightarrow y=z {\huge)} \Rightarrow {\huge(} \exists B \ \forall y \ {\Large[} \ y \in B \Leftrightarrow {\large(} \exists x \in A \ \ (R) {\large)} {\large]} {\huge)} \).
Donc : $$ \forall p_1,...,p_n \ \ \forall A \ {\Huge[} {\huge(} \forall x \forall y \forall z \ {\Large[} (R) \wedge (R[y \leftarrow z]) {\Large]} \Rightarrow y=z {\huge)} \Rightarrow {\huge(} \exists B \ \forall y \ {\Large[} \ y \in B \Leftrightarrow {\large(} \exists x \in A \ \ (R) {\large)} \ {\Large]} {\huge)} {\Huge]} $$ On retrouve bien \(S_R\), c'est-à-dire l'axiome de substitution en R, mais sans avoir imposé de conditions à x, y ou A.
