Remplacement
![[Utilisateur supprimé]](https://wf.vanillicon.com/f9001f61ce4677a47bf2bb21f24a110a_100.png)
Axiome de remplacement:
$\forall f \forall a\exists b\forall z(z\in b\leftrightarrow \exists c(c\in a\wedge z=fc))$
Ici, $f$ est une variable fonctionnelle d'arité 1, les autres variables étant des variables fonctionnelles d'arité 0.
Le schéma d'axiomes de remplacement est une théorie du premier ordre qui est équivalente à la formule du second ordre que j'ai écrite plus haut. Pourquoi ça a l'air beaucoup plus naturel le second ordre ?
$\forall f \forall a\exists b\forall z(z\in b\leftrightarrow \exists c(c\in a\wedge z=fc))$
Ici, $f$ est une variable fonctionnelle d'arité 1, les autres variables étant des variables fonctionnelles d'arité 0.
Le schéma d'axiomes de remplacement est une théorie du premier ordre qui est équivalente à la formule du second ordre que j'ai écrite plus haut. Pourquoi ça a l'air beaucoup plus naturel le second ordre ?
Réponses
-
Pourquoi serait-ce moins naturel ?
Votre question n'est pas mathématique et concerne votre ressenti, comment pourrions-nous répondre ?Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse -
En effet, il s'agit d'une question vague. En fait je suis stupéfait par le second ordre et je crois que cette formulation du schéma d'axiomes de remplacement est l'idée que Fraenkel avait derrière la tête lorsqu'il a proposé le schéma d'axiomes de remplacement. En gros je suis seulement en train de dire ici que je suis fan du second ordre.
-
Malheureusement on perd pas mal de théorèmes dont celui de complétude.Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse -
Je crois cependant qu'on commet une grosse erreur lorsque l'on interprète les formules du second ordre. C'est une énorme erreur de laisser les variables du second ordre parcourir toutes les parties intuitives des puissances cartésiennes de l'univers. Il faudrait au contraire laisser les variables parcourir les ensembles définissables seulement. Si on fait cette restriction, alors la formule du second ordre plus haut sera logiquement équivalente au schéma de remplacement. Sinon alors la formule plus haut a pour conséquence le schéma de remplacement, mais ne lui est pas équivalente.
-
C'est vrai, le second ordre n'aime pas beaucoup la théorie de la démonstration.Médiat_Suprème a dit :Malheureusement on perd pas mal de théorèmes dont celui de complétude. -
C'est vrai, le second ordre n'aime pas beaucoup la théorie de la démonstration.
Ah bon ? C'est passer un peu vite sur les travaux de J-Y. Girard, par exemple : https://fr.wikipedia.org/wiki/Syst%C3%A8me_F
-
Oui, en effet. J'en suis arrivé à cette restriction après avoir boycotté le second ordre pendant des années car je trouvais que ce n'était pas naturel du tout. Récemment, lorsque je travaillais sur la théorie des ensembles, je me suis rendu compte qu'on pouvait travailler dans un univers (comme dans le Cori-Lascar, d'ailleurs je considère que Mr René Cori est de loin le meilleur prof de logique qui ait jamais existé) mais en enrichissant le langage de telle sorte à rajouter des symboles qui auront pour interprétations toutes les parties définissables et les fonctions définissables. On ne change pas les parties définissables de l'univers en faisant cet enrichissement de language, et on obtient des formules beaucoup plus intelligibles dans ce langage... après quelques centaines de pages et plus d'une année de ce travail, j'ai commencé à sentir que le second ordre était la suite naturelle à rajouter puisque tout ce que je faisais me poussait vers le second ordre...Il m'a semblé beaucoup plus naturel que les variables du second ordre parcourent les symboles de notre enrichissement plutôt que des parties arbitraires des puissances cartésiennes de l'univers. J'ai voulu faire des tests pour voir si ma restriction donnait quelque chose de naturel, et j'ai pris les schémas d'axiomes de remplacement et de compréhension, quand j'ai vu que ma restriction permettait d'exprimer chaque schéma par une formule du second ordre équivalente au schéma, je me suis dit "jackpot".Martial a dit :@Igbinoba : si tu laisses ta variable du second ordre ne parcourir que les parties définissables de l'univers, ça revient au schéma de remplacement au premier ordre.
-
Je disais ça dans le sens que la construction à la Henkin ne marche pas pour le second ordre, j'aurais dû être plus clair.GaBuZoMeu a dit : https://les-mathematiques.net/vanilla/index.php?p=/discussion/comment/2342506/#Comment_2342506[Inutile de recopier un message présent sur le forum. Un lien suffit. AD]
-
Elle marche lorsqu'on ne considère pas exclusivement des modèles pleins (où $X^Y$ s'interprète systématiquement comme l'ensemble des fonctions de $Y$ dans $X$).IGBINOBA a dit :Je disais ça dans le sens que la construction à la Henkin ne marche pas pour le second ordre, j'aurais dû être plus clair.
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$. -
Désolé ma question est mal posée, et j'aurais dû y réfléchir un minimum avant de la poser (la fatigue). Je vais de toute façon essayer de vérifier par moi même si la construction à la Henkin marche encore dans le second ordre (contrairement à ce que je pensais), mais avant de faire ce travail, j'aimerais savoir si tu es certain qu'à toute théorie cohérente du second ordre, on peut construire un modèle (non plein) ?
-
@Foys. Aucun rapport avec la choucroute mais je profite du contexte pour te poser cette question.J'ai du mal avec ces histoires de modèle plein ou pas plein, et avec la logique du second ordre. Connais-tu une bonne référence BASIQUE sur la logique du second ordre ?Je précise que je n'ai jamais rien compris au livre de David, Nour et Raffali : "Introduction à la logique", et pas grand-chose à celui de Dirk van Dalen : "Logic and structure", donc ça serait sympa de ta part si tu pouvais m'en proposer un troisième. Merci d'avance.
-
@Martial: je partage ta frustration malheureusement je n'ai jamais trouvé pour l'instant que des documents épars sur le net. Il me semble que Christophe et Maxtimax avaient cité un contre-exemple au théorème de complétude pour les modèles pleins sur le forum.Idée: soit $T$ l'ensemble des sortes sur lesquelles on peut quantifier; un modèle général (non nécessairement plein) va livrer une famille d'ensembles $(D_x)_{x\in T}$ et pour tous $x,y$ tels que $x\to y\in T$ on a également une fonction $eval_{x,y}$ de $D_{x\to y} \times D_x$ dans $D_y$. Les modèles pleins sont la situation particulière où $D_{x\to y}$ est égal à l'ensemble tout entier des applications de $D_x$ dans $D_y$ et où $eval_{x,y} (f) (t)=f(t)$ pour tous $f\in D_{x\to y}$ et $t\in D_x$.Pour la complétude sans plénitude, on considère une signature $\sigma$ dénombrable (sinon on adapte avec Zorn) on peut procéder comme suit. Soit $C$ l'ensemble des constantes de la signature. Pour toute sorte $s \in T$ on se donne un ensemble $\{c^s_n \mid n \in \N \}$ de lettres ne figurant pas dans $C$.Soit $\{F_n\mid n \in \N\}$ l'ensemble (dénombrable) de toutes les formules écrites sur $\sigma \cup \coprod_{s\in T} \{c^s_n \mid n \in \N\}$.Quitte à réordonner (ou à faire jouer des surjections de $\N$ sur $\N^2$ telle que $n\mapsto (p,q)$ où $2^p(2q+1) -1 =n$) on peut supposer que toute formule apparait une infinité de fois dans l'énumération $n\mapsto F_n$. (Ceci sert à garantir le bon comportement du procédé ci-dessous, qui produit un ensemble non contradictoire maximal de formules).La notion de preuve utilisée va être celle de démonstration naturelle avec contexte. Soit $H$ une partie non contradictoire de $\{F_n,n\in \N\}$ et dont toutes les variables libres sont dans $C$.On construit $(H_n)_{n\in \N}$ et $(C_n)_{n\in \N}$ par récurrence comme suit:(i) $C_0:=C$ et $H_0:=H$.-si $H_n$ et $C_n$ sont construits (ci-dessous,$X$ contradictoire signifie "$X$ prouve $\perp$ en déduction naturelle dans le contexte $C_n$")(ii) si $F_n$ possède des variables libres qui ne figurent pas dans $C_n$ on pose $C_{n+1}=C_n$ et $H_{n+1}:=H_n$.(iii) si toutes les variables libres de $F_n$ sont dans $C_n$ et $H_n\cup \{F_n\}$ est contradictoire, $H_{n+1}:=H_n$ et $C_{n+1}:=C_n$.(iv) si toutes les variables libres de $F_n$ sont dans $C_n$, $H_n\cup \{F_n\}$ est non contradictoire, et $F$ n'est pas de la forme $\exists (x:s), G$,alors $H_{n+1}:=H_n\cup \{F_n\}$ et $C_{n+1}:=C_n$.(v) si toutes les variables libres de $F_n$ sont dans $C_n$, si $F_n$ est de la forme $\exists (x:s), G$, et si $H_n \cup \{F_n\}$ est non contradictoire, soit $k$ le plus petit entier tel que $c^s_k\notin C_n$.On pose $H_{n+1}:= H_n\cup \{F_n\} \cup \{G[x:=c^s_k]\}$ et $C_{n+1}:= C_n \cup \{c^s_k\}$On pose $C_{\infty}:=\bigcup_{n\in \N} C_n$ et $H_{\infty}:=\bigcup_{n\in \N} H_n$. Cet ensemble est non contradictoire lorsque $H_0$ l'est.On pose pour tout $s\in T$, $\mathcal D_s:=$ l'ensemble des termes de sorte $s$ construits sur $C_{\infty}$ (et $D_s:=\mathcal D_s/\simeq_s$ où pour tous $v,w \in \mathcal D_s$, $v\simeq_s w:= H_{\infty} \vdash_{C_{\infty}} v =_s w$ si la théorie ambiante est égalitaire).Si $A$ est un autre contexte contenant $C:=C_0$ et $e$ un environnement sur $A$ (une fonction envoyant les éléments de $A$ de sorte $s$ sur des éléments de $D_s$ pour tout $s$) prolongeant l'identité $id_C:C\to C$, l'interprétation d'une formule $f$ de $A$ se fait comme en théorie des modèles de logique du premier ordre. On dit qu'une formule est vraie si son image par une telle application est dans $H_{\infty}$.On voit que toutes les formules de $H$ sont alors vraies, qu'une formule $\exists (x:s):G$ est vraie si et seulement si il existe un élément $d\in D_s$ tel que $G[x:=d]$ est vraie, que $P\wedge Q$ est vraie ssi $P$ et $Q$ le sont, que $\neg P$ est vraie ssi $P$ n'est pas vraie etc.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$.
-
En tout cas merci @Foys, je pense que ton commentaire est correct (je n'ai pas encore vérifié) et c'est une chose superbe, c'est une raison de plus pour se rendre compte que prendre les modèles plein pour modèles par défaut est une erreur de jugement et c'est la seule chose (à mon avis) qui n'inspire pas les gens à travailler davantage dans le second ordre plutôt que de tout ramener au premier ordre.
-
Foys : je n'ai pas tout lu , mais effectivement, c'est pas compliqué de trouver un contre-exemple à la complétude pour les modèles pleins : la théorie des bons ordres est facilement exprimable dans $\{<\}$ au second ordre. Je rajoute alors un paquet de constantes $c_n,n\in\mathbb N$ et les axiomes $c_n < c_m$ pour $m<n$.
Alors 1) cette théorie n'a pas de modèle plein (évident, $\{c_n, n\in\mathbb N\}$ n'a pas de minimum); 2) il n'y a pas de contradiction qui puisse s'obtenir en un nombre fini d'étapes (preuve : une telle contradiction n'utilise qu'un nombre fini de constantes $c_n$, mais alors la théorie a plein de modèles si on se restreint à ces constantes).
Un élément essentiel de ce contre-exemple est la finitude des preuves, mais aussi du nombre d'axiomes utilisé par étape de la preuve. Le premier me semble essentiel à la notion de preuve (quoique ça a certainement été étudié), mais dans des logiques plus bizarres on peut imaginer des preuves où une étape est $\bigvee_{i\in I}\varphi_i$, $\varphi_i$ des axiomes ou théorèmes, $I$ non nécessairement fini (je ne sais pas comment faire un gros $\land$ donc je m'en tiens à $\vee$ mais vous voyez ce que je veux dire) - typiquement en $L_{\kappa,\lambda}$, même si ça je n'y connais rien. -
Martial : ah oui, \wedge et pas \land :-D (en plus je connais \bigwedge pour les puissances extérieures, mais comme je pensais vraiment à \land ça ne m'est pas venu à l'esprit)
-
Je réagis tardivement mais merci Maxtimax pour cette réponse.
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$.
Connectez-vous ou Inscrivez-vous pour répondre.
Bonjour!
Catégories
- 163.1K Toutes les catégories
- 8 Collège/Lycée
- 21.9K Algèbre
- 37.1K Analyse
- 6.2K Arithmétique
- 53 Catégories et structures
- 1K Combinatoire et Graphes
- 11 Sciences des données
- 5K Concours et Examens
- 11 CultureMath
- 47 Enseignement à distance
- 2.9K Fondements et Logique
- 10.3K Géométrie
- 62 Géométrie différentielle
- 1.1K Histoire des Mathématiques
- 68 Informatique théorique
- 3.8K LaTeX
- 39K Les-mathématiques
- 3.5K Livres, articles, revues, (...)
- 2.7K Logiciels pour les mathématiques
- 24 Mathématiques et finance
- 312 Mathématiques et Physique
- 4.9K Mathématiques et Société
- 3.3K Pédagogie, enseignement, orientation
- 10K Probabilités, théorie de la mesure
- 772 Shtam
- 4.2K Statistiques
- 3.7K Topologie
- 1.4K Vie du Forum et de ses membres
In this Discussion
Qui est en ligne 5
+4 Invités