# Schema di assiomi di rimpiazzamento

Nella teoria degli insiemi, lo schema di assiomi di rimpiazzamento è uno schema di assiomi della teoria degli insiemi di Zermelo-Fraenkel.
Sia P una generica relazione in due variabili che non usa il simbolo B. Allora, nel linguaggio formale degli assiomi di Zermelo-Fraenkel, lo schema di assiomi si scrive:
    $(\forall X,\exists !\,Y:P(X,Y))\rightarrow \forall A,\exists B,\forall C:C\in B\iff \exists D:D\in A\land P(D,C)$
oppure a parole:
    Se, dato un generico insieme X, esiste un unico insieme Y tale che P vale per X e Y, allora, dato un generico insieme A, esiste un insieme B tale che, dato un generico insieme C, C è un elemento di B se e solo se esiste un insieme D tale che D è un elemento di A e P vale per D e C.
Si noti che esiste un assioma per ogni predicato P di quel tipo; quindi questo è uno schema di assiomi.
Per comprendere questo assioma, si noti per prima cosa che la clausola nel primo insieme di parentesi è esattamente quella necessaria alla costruzione di un predicato funzionale F in una variabile tale che F(X) = Y se e solo se P(X,Y). Infatti, se si formalizza il linguaggio del primo ordine in modo da ammettere l'uso di predicati funzionali derivati negli schemi di assiomi, allora lo schema di assiomi può essere riscritto come:
    $\forall A,\exists B,\forall C:C\in B\iff \exists D:D\in A\land C=F(D)$
per ogni predicato funzionale derivato F in una variabile; oppure a parole:
    Dato un generico insieme A, esiste un insieme B tale che, dato un generico insieme C, C è un elemento di B se e solo se esiste un insieme D tale che D è un elemento di A e C è uguale al valore di F in D.
Si noti che la clausola fra parentesi in questa riformulazione (equivalente alla seconda clausola fra parentesi dell'espressione originale) semplicemente afferma che C è il valore di F per un certo elemento D di A. Quindi quello che lo schema di assiomi sta dicendo è che, dato un insieme A, possiamo trovare un insieme B i cui elementi sono precisamente i valori di F sugli elementi di A.
Possiamo usare l'assioma di estensionalità per mostrare che questo insieme B è unico. Chiamiamo l'insieme B immagine di A mediante F, e lo indichiamo con F(A) oppure (usando una forma di rappresentazione per caratteristica) {F(D) : D ∈ A}.
Quindi l'essenza dell'assioma è:
    L'immagine di un insieme mediante un'applicazione è un insieme.

## Storia e filosofia

La maggior parte delle applicazioni in cui il rimpiazzamento può essere usato ingenuamente di fatto non richiedono l'assioma. Ad esempio, sia f una funzione da un insieme S a un insieme T. Allora possiamo costruire un predicato funzionale F tale che F(x) = f(x) ogni volta che x è un elemento di S, lasciando che F(x) assuma un valore qualsiasi negli altri casi (non è importante in questo caso). Allora, dato un sottoinsieme A di S, applicando lo schema di assiomi di rimpiazzamento F si ottiene l'immagine f(A) del sottoinsieme A mediante la funzione f; e questo è proprio F(A). Tuttavia il rimpiazzamento non è necessario in questo caso, perché f(A) è un sottoinsieme di T, perciò possiamo costruire la sua immagine, usando lo schema di assiomi di specificazione, come l'insieme {y in T : per qualche x in A, y = f(x)}. In generale la specificazione è sufficiente quando i valori di F sugli elementi di A appartengono tutti a un determinato insieme T precedentemente costruito; il rimpiazzamento è necessario solo quando tale T non è già disponibile.
Secondo alcuni matematici è preferibile applicare la specificazione su un insieme come T, poiché la specificazione è logicamente più debole del rimpiazzamento (come spiegato nella prossima sezione). In realtà il rimpiazzamento non è necessario nella matematica ordinaria, e serve solo per determinati risultati della teoria assiomatica degli insiemi. Ad esempio il rimpiazzamento è necessario per costruire l'ordinale di von Neumann da ω$_2$ in avanti, e gli ordinali di von Neumann servono in alcune aree della teoria degli insiemi. Tuttavia il rimpiazzamento non è necessario alla costruzione degli ordinali usati nella teoria degli insiemi ben ordinati. Alcuni matematici che lavorano sui fondamenti della matematica, in particolare quelli che si concentrano sulla teoria dei tipi, considerano questo assioma non necessario in ogni caso e quindi non lo includono nelle loro fondazioni. Il rimpiazzamento è difficilmente esprimibile nelle fondazioni costruite sulla teoria dei topos, quindi, è spesso tralasciato. Ciò nonostante il rimpiazzamento non è controverso nel senso che qualcuno ritiene le sue conseguenze necessariamente false (un senso nel quale l'assioma della scelta, ad esempio, è controverso); viene semplicemente considerato superfluo.
Lo schema di assiomi di rimpiazzamento non era parte dell'assiomatizzazione della teoria degli insiemi del 1908 di Ernst Zermelo (Z); la sua introduzione da parte di Adolf Fraenkel nel 1922 è quella che rende la moderna teoria degli insiemi Zermelo-Fraenkel (ZF). L'assioma è stato indipendentemente scoperto da Thoralf Skolem più tardi nello stesso anno, ed è di fatto la versione finale della lista di assiomi stilata da Skolem quella usata oggi - ma in genere non gli viene tributato il merito perché ciascun assioma era stato sviluppato precedentemente da Zermelo o da Fraenkel. L'inclusione del rimpiazzamento comporta una grande differenza dal punto di vista della teoria della dimostrazione: l'aggiunta di questo schema agli assiomi di Zermelo rende questo sistema logicamente molto più forte, permettendo la dimostrazione di molte più affermazioni. In particolare, in ZF è possibile provare la coerenza di Z mediante la costruzione dell'universo di von Neumann V$_{ω2}$ come modello. (Naturalmente il secondo teorema di incompletezza di Gödel mostra che nessuna di queste teorie può dimostrare la propria coerenza.)

## Relazione con lo schema di assiomi di specificazione

Lo schema di assiomi di specificazione può essere derivato quasi completamente dallo schema di assiomi di rimpiazzamento. Vedi relazione con lo schema di assiomi di rimpiazzamento nell'articolo Schema di assiomi di specificazione.
Per questa ragione lo schema di assiomi di separazione è spesso omesso negli elenchi moderni degli assiomi di Zermelo-Fraenkel. Tuttavia è ancora importante per ragioni storiche, e per i paragoni con le assiomatizzazioni alternative della teoria degli insiemi. Ad esempio la derivazione dello schema di assiomi di specificazione sfrutta il principio del terzo escluso, e quindi la specificazione non può essere omessa in una teoria degli insiemi intuizionistica.