# Schema di assiomi di specificazione

Nella teoria degli insiemi, lo schema di assiomi di specificazione, o schema di assiomi di separazione, è uno schema di assiomi della teoria degli insiemi di Zermelo-Fraenkel. È anche detto schema di assiomi di comprensione, benché il termine sia usato anche per la comprensione non ristretta, discussa più avanti.
Sia P un generico predicato in una variabile che non usa il simbolo B. Allora nel linguaggio formale degli assiomi di Zermelo-Fraenkel, l'assioma si scrive:
    $\forall A,\exists B,\forall C:C\in B\iff C\in A\land P(C)$
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 C è un elemento di A e P vale per C.
Si noti che esiste un assioma per ogni predicato P di quella forma; quindi questo è uno schema di assiomi.
Per comprendere questo schema di assiomi, si noti che B deve essere un sottoinsieme di A. Quindi, quello che l'assioma sta realmente dicendo è che, dato un insieme A e un predicato P, possiamo trovare un sottoinsieme B di A i cui elementi sono precisamente gli elementi di A che soddisfano P. Per l'assioma di estensionalità questo insieme è unico. Denotiamo usualmente questo insieme, mediante la rappresentazione per caratteristica, come {C ∈ A : P(C)}. Quindi l'essenza dell'assioma è:
    Ogni sottoclasse di un insieme definita da un predicato è essa stessa un insieme.
Lo schema di assiomi di specificazione è generalmente considerato non controverso, e appare in questa forma o in una forma equivalente in quasi tutte le assiomatizzazioni della teoria degli insiemi. In realtà molte formulazioni alternative della teoria degli insiemi cercano di trovare uno schema di assiomi ancora più generoso, invece di fermarsi allo schema di assiomi della comprensione (non ristretta) menzionato più avanti.

## Relazione con lo schema di assiomi di rimpiazzamento

Lo schema di assiomi di specificazione può essere derivato quasi completamente dallo schema di assiomi di rimpiazzamento.
Per prima cosa, richiamiamo questo schema di assiomi:
    $\forall A,\exists B,\forall C:C\in B\iff \exists D:D\in A\land C=F(D)$
per ogni predicato funzionale F in una variabile che non usa i simboli A, B, C o D. Dato un opportuno predicato P per l'assioma di specificazione, si definisce l'applicazione F come F(D) = D se P(D) è vera e F(D) = E se P(D) è falsa, dove E è un generico elemento di A tale che P(E) è vero. Allora l'insieme B, garantito dall'assioma di rimpiazzamento è precisamente l'insieme B richiesto dall'assioma di specificazione. L'unico problema si incontra se l'elemento E cercato non esiste. Ma in questo caso l'insieme B richiesto dall'assioma di separazione è l'insieme vuoto, così l'assioma di separazione segue dall'assioma di rimpiazzamento e dall'assioma dell'insieme vuoto.
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, come si può vedere per esempio nella seguente sezione.

## Comprensione non ristretta

Lo schema di assiomi di comprensione non ristretta si scrive:
    $\exists B,\forall C,C\in B\leftrightarrow P\left(C\right)$
cioè:
    Esiste un insieme B i cui elementi sono esattamente gli oggetti che soddisfano il predicato P.
Questo insieme B è ancora unico, ed è usualmente denotato da {C : P(C)}.
Questo assioma era usato tacitamente nei primi tempi della teoria ingenua degli insiemi, prima che fosse adottata una assiomatizzazione rigorosa. Sfortunatamente questo assioma porta direttamente al paradosso di Russell, se si prende P(C) come (C non è in C). Quindi nessuna assiomatizzazione della teoria degli insiemi può usare la comprensione non ristretta, almeno non nella logica classica. L'accettazione del solo schema di assiomi di specificazione è stato l'inizio della teoria degli insiemi assiomatica. La maggior parte degli assiomi di Zermelo-Fraenkel (ma non l'assioma di estensionalità o l'assioma di regolarità) allora divennero necessari come sostituti addizionali dello schema di assiomi di comprensione; ciascuno di quegli assiomi afferma che un determinato insieme esiste, e definisce questo insieme fornendo un predicato che i suoi elementi devono soddisfare.

## Nella teoria delle classi di NBG

Nella teoria degli insiemi di von Neumann-Bernays-Gödel viene fatta una distinzione fra insiemi e classi. Una classe C è un insieme se e solo se appartiene a qualche classe E. In questa teoria esiste uno schema di teoremi che si scrive:
    $\exists D,\forall C,C\in D\leftrightarrow \left(P\left(C\right)\land \exists E,C\in E\right)$
cioè:
    Esiste una classe D tale che ogni classe C è un elemento di D se e solo se C è un insieme che soddisfa P.
Questo schema di teoremi è esso stesso una forma ristretta di comprensione, ed evita il paradosso di Russell grazie al requisito che C sia un insieme. Quindi la specificazione per gli insiemi può essere scritta in un singolo assioma:
    $\forall D,\forall A,\left(\exists E,A\in E\right)\rightarrow \exists B,\left(\exists E,B\in E\right)\land \forall C,C\in B\leftrightarrow \left(C\in A\land C\in D\right)$
cioè:
    Data una generica classe D e un generico insieme A, esiste un insieme B i cui elementi sono precisamente quelle classi che sono elementi sia di A che di D;
o ancora più semplicemente:
    L'intersezione di una classe D e di un insieme A è un insieme B.
In questo assioma il predicato P è sostituito dalla classe D, che può essere quantificata.

## Nella logica del secondo ordine

Nella logica del secondo ordine possiamo quantificare i predicati, e lo schema di assiomi di specificazione diventa un semplice assioma. Questo trucco è molto simile a quello usato negli assiomi NBG della sezione precedente, dove il predicato è stato sostituito da una classe che poi è stata quantificata.

## Nella Nuova fondazione di Quine

Nell'approccio alla teoria degli insiemi della Nuova fondazione, aperto da W.V.O. Quine, l'assioma di comprensione per un dato predicato assume la forma non ristretta, ma i predicati che possono essere usati nello schema sono ristretti. Il predicato (C non è in C) è proibito, perché lo stesso simbolo C appare in entrambi i membri del simbolo di appartenenza; quindi il paradosso di Russel è evitato. Tuttavia, prendendo P(C) come (C = C), che è permesso, possiamo definire l'insieme di tutti gli insiemi.