Discussion:Schéma d'axiomes de remplacement

Whouah, c'est dense, prévoir les aspirines !!! Je pense que quand j'aurai compris, je proposerai une version « éclaircie ». Sinon, je serais très content si quelqu'un m'épargnais cette peine !! ;-) --Ąļḋøø 26 aoû 2004 à 13:33 (CEST)

Vu qu'il y en a plusieurs, j'aurai tendance à mettre un pluriel à axiome, dans "schéma d'axiomes". C'est ce que fait Krivine (Théorie axiomatique des ensembles). Sauf si quelqu'un peut justifier le singulier il faudrait corriger. Proz 24 juillet 2006 à 14:42 (CEST) Finalement ça m'a semblé assez évident pour le faire directement, j'ai essayé aussi d'améliorer un peu. L'explication de la formule peut me semble-t-il être améliorée. Il reste à préciser de "vraies" applications, donner un historique (Fraenkel ?)etc. Proz 24 juillet 2006 à 15:32 (CEST)

J'ai ajouté des paramètres à l'énoncé de l'axiome, ce qui est nécessaire, et pour que l'on puisse en déduire le schéma de compréhension. J'ai pas mal reformulé à l'occasion : présentation informelle avant présentation formelle en gros. Proz 7 septembre 2006 à 20:14 (CEST)

--- Pourquoi faire simple quand on peut faire compliqué?

extrait:

Voyons comment écrire l'axiome dans le langage de la théorie des ensembles. Tout d'abord, étant donnée un prédicat à deux arguments, c’est-à-dire une formule F à deux variables libres x et y plus d'éventuels paramètres a1 … ap, on doit écrire que la relation entre x et y décrite par cette formule est fonctionnelle (a1 … ap étant fixés) :

   ∀x ∀y ∀y' [(F x y a1 … ap et F x y' a1 … ap) ⇒ y = y' ].

On peut donc écrire formellement le schéma d'axiomes ainsi (l'emploi des majuscules pour A et B, qui n'a aucune signification propre — il n'y a que des ensembles en théorie des ensembles — ne sert qu'à la lisibilité) :

∀a1 … ap { ∀x ∀y ∀y' [(F x y a1 … ap et F x y' a1 … ap) ⇒ y = y' ] ⇒ ∀A ∃B ∀ y [y ∈ B ⇔ ∃ x(x ∈ A et F x y a1 … ap) ] }

ce pour toute formule F n'ayant d'autres variables libres que x, y, a1, … ,ap.

Notez qu'il y a un axiome pour chaque prédicat F ; il s'agit donc bien d'un schéma d'axiomes. La formule F, les paramètres a1 … ap et l'ensemble A étant fixé, l'ensemble B ainsi défini est unique par l'axiome d'extensionnalité.

commentaire:

À quoi servent tous ces paramètres? Les prédicats F x y a1 … ap (a1 … ap étant fixés) sont exactement les prédicats F' x y! (en posant F' = λ x y. F x y a1 … ap), ce qui simplifierait le tout (sans gain ni perte de généralité) en:

Voyons comment écrire l'axiome dans le langage de la théorie des ensembles. Tout d'abord, étant donnée un prédicat à deux arguments, c’est-à-dire une formule F à deux variables libres x et y, on doit écrire que la relation entre x et y décrite par cette formule est fonctionnelle :

   ∀x ∀y ∀y' [(F x y ∧ F x y') ⇒ y = y' ].

On peut donc écrire formellement le schéma d'axiomes ainsi (l'emploi des majuscules pour A et B, qui n'a aucune signification propre — il n'y a que des ensembles en théorie des ensembles — ne sert qu'à la lisibilité) :

   ∀x ∀y ∀y' [(F x y ∧ F x y') ⇒ y = y' ] ⇒ ∀A ∃B ∀ y [y ∈ B ⇔ ∃ x(x ∈ A ∧ F x y) ] }

ce pour toute formule F n'ayant d'autres variables libres que x et y.

Notez qu'il y a un axiome pour chaque prédicat F ; il s'agit donc bien d'un schéma d'axiomes. La formule F et l'ensemble A étant fixé, l'ensemble B ainsi défini est unique par l'axiome d'extensionnalité.

Il faut aussi changer les "et" en "∧" dans les formules.

Cédric, le 15 Novembre 2008

Les paramètres sont formellement des variables libres (paramètre renvoie à la façon dont ils sont utilisés). Ils sont indispensables, le schéma est plus faible sans, et il ne faut pas oublier qu'en théorie des ensembles axiomatique il n'y a pas de constantes, celles qu'on utilise sont des "abréviations" (ou on fait de l'extension par définition). L'ensemble vide par exemple c'est un x vérifiant ∀ y y ∉ x. Ca mérite probablement une explication "douce", mais on ne peut pas les retirer. Ou alors on considère que les paramètres sont implicites, acceptable peut-être en théorie naïve.

Changer les "et" en "∧" dans les formules (pourquoi il faut ?!) : pure convention de notation. Deux lettres ou une, ça me semble tout autant lisible. Celles de l'article présent conviennent bien, et sont celles par exemple de Jean-Louis Krivine, Théorie des ensembles [détail des éditions] (à tout prendre autant suivre les références en français disponibles). Ce même livre utilise d'ailleurs ∧, ∨, → ... pour une version formalisée en th. des ens. des formules (bien commode). Proz (d) 15 novembre 2008 à 16:18 (CET)

la restriction d'une classe fonctionnelle à un ensemble définit une fonction

Il ne me semble pas avoir vu l'expression « classe fonctionnelle » ; relation fonctionnelle oui, mais c'est une relation à 2 variables ; Krivine définit les classes comme des relations à 1 variable libre (mais je n'ai pas la dernière version de Théorie axiomatique des ensembles). Michel421 _{parfaitement agnostique} 8 septembre 2011 à 00:42 (CEST)

Ce vocabulaire ne vient pas du Krivine (qui parle de relation et de collection), mais il est assez utilisé, on trouve des exemples sur le web, sites universitaires. Il s'agit d'une classe de couples (décrite par une formule à deux variables libres, mais on sait coder les couples) qui est fonctionnelle, et . Le vocabulaire tant en anglais qu'en français n'est pas très fixé. Ca semble utile de distinguer ici clairement les relations comme classe de celles qui sont des ensembles, et c'est défini. Proz (d) 8 septembre 2011 à 19:14 (CEST)

Oui, c'est compréhensible, et je trouve que c'est même plus joli (du fait que ça se fait en présence de l'axiome de compréhension, ça permet de mieux voir le rôle de l'axiome de remplacement), mais je n'avais pas souvent vu le remplacement formulé ainsi en ZF (en NBG oui forcément). Michel421 _{parfaitement agnostique} 11 septembre 2011 à 18:06 (CEST)

Indécidabilité

Je suppose que ce schéma et l'une (bien choisie) de ses négations sont relativement consistants avec Z^{[réf. souhaitée]}… Anne 16/11/16

Capture de la variable y' ?

Dans le test que F est une relation fonctionnelle, il y a la substitution F x y' (où y est remplacé par y'). Or si la formule F quantifie la variable y', il se peut qu'elle soit capturée et que

∀x ∀y ∀y' [(F x y a1 … ap et F x y' a1 … ap) ⇒ y = y' ]

ne teste plus vraiment que F est fonctionnelle. Je pense qu'il faut préciser : "ce pour toute formule F n'ayant d'autres variables libres que x, y, a1, … ,ap et n'ayant pas du tout la variable y'." — Le message qui précède, non signé, a été déposé par Vincent Semeria (discuter), le 24 janvier 2018 à 12:25 (CET)