Schéma d'axiome de remplacement
Dans la théorie axiomatique des ensembles et dans les branches de la logique, des mathématiques, et de l'informatique, le schéma d'axiome de remplacement est un schéma d'axiome dans la théorie des ensembles de Zermelo-Fraenkel.
Supposons que P soit un prédicat quelconque à deux arguments qui n'emploie pas le symbole B. Alors dans le langage formel de l'axiomatique de Zermelo-Fraenkel, le schéma d'axiome s'écrit:
ou avec des mots:
- si pour un ensemble quelconque X, il existe au plus un ensemble Y tel que P soit vérifiée en X et Y, alors, étant donné un ensemble quelconque A, il existe un ensemble B tel que, pour tout ensemble C, C est un élément de B si et seulement si, il existe un ensemble D tel que D soit un élément de A et P soit vérifiée en D et C.
Notez qu'il y a un axiome pour chaque prédicat P ; il s'agit donc bien d'un schéma d'axiome.
Pour comprendre cet axiome, notons tout d'abord que la clause placée dans la première paire de parenthèses ci-dessus représente exactement ce dont nous avons besoin pour construire un prédicat fonctionnel F à un argument tel que, F (X) = Y si et seulement si P ( X , Y) est vraie. En effet, si nous formalisons dans le langage de la logique des prédicats, alors le schéma d'axiome peut être récrit de la façon suivante:
à remplacer par
- pour tout prédicat fonctionnel dérivé F à un argument;
ce qui en d'autres termes s'écrit:
- étant donné un ensemble quelconque A, il existe un ensemble B tel que, pour tout ensemble quelconque C, C est un élément de B si et seulement s’il existe un ensemble D tel que D soit un élément de A et que C soit égal à la valeur de F en D.
Ensuite, notez que la clause entre parenthèses dans la nouvelle formulation ci-dessus (équivalente à la deuxième clause entre parenthèses dans la proposition d'origine) affirme simplement que C est la valeur de F en un certain élément D de A. Ainsi, le schéma d'axiome indique que pour un ensemble A quelconque, nous pouvons trouver un ensemble B dont les éléments sont précisément les valeurs prises par F en les éléments de A.
Nous pouvons employer l'axiome d'extensionnalité pour démontrer que cet ensemble B est unique. Nous appelons l'ensemble B l'image de A par F, et la notons F (A) ou (en utilisant une forme de notation de définition en compréhension) 
. Ainsi le schéma d'axiome affirme essentiellement que:
- l'image d'un ensemble par une « fonction » est un ensemble.