Tre modi di considerare gli
insiemi:
le teorie ZF, GB(G), GB(B).
Il perchè delle teorie
• L’assiomatizzazione di Frege
La teoria proposta da Frege considera un solo predicato binario
primitivo  per indicare l’appartenenza e due assiomi:
Assioma di estensionalità:
Se due insiemi hanno gli stessi elementi allora sono identici.
(x)(y)((z)(zx↔zy)→xy)
Assioma di comprensione:
(x)(y)(yx↔A(y))
Pochi assiomi, chiari, intuitivi. La teoria è però talmente potente da
riuscire a dimostrare una contraddizione.
• Il paradosso (e anche antinomia) di Russell
La contraddizione si scopre considerando questa occorrenza dello
schema di comprensione:
(x)(y)(yx↔¬(yy))
a
Per recuperare la teoria degli insiemi si è allora cercato un sistema di
assiomi in cui non fosse così semplice derivare una contraddizione.
Sono state elaborate varie teorie nel tentativo di approdare a una teoria
consistente.
Russell propose un sistema in cui si dava una gerarchia alle variabili in
modo che la formula considerate per dimostrare la contraddizone non
fosse più nemmeno ben formata.
Altri pensarono di limitare o escludere lo schema di assiomi di
comprensione.
Le teorie Z e ZF
L’idea di queste teorie è di rinunciare al principio di comprensione.
Non si ha un insieme in corrispondenza di ogni condizione
determinante o di ogni proprietà. Per evitare le contraddizioni
secondo Zermelo si devono infatti considerare insiemi solo entità a
cui non appartenga un eccessivo numero di elementi.
La teoria Z
Per entrambe le teorie si danno come simboli primitivi :
-I simboli logici di un linguaggio del prim’ordine con identità.
-Il predicato binario .
La teoria si compone di 7 tipi di assiomi (6 assiomi e uno schema).
1.
Assioma di Estensionalità. Se due insiemi hanno gli stessi elementi
allora sono identici:
(x)(y)((z)(zx↔zy)→xy)
Attraverso il solo assioma di estensionalità possiamo dimostrare uno schema di
teoremi utile per estendere la teoria con nuovi simboli funzionali:
Sia A una formula e xLib(A) allora:
2.
(!!x)(y)(yx↔A(y))
Schema di assiomi di Isolamento. Per ogni formula, esiste l’insieme
composto dagli elementi che appartengono a un insieme e soddisfano
la formula:
Per ogni formula B:
(x)(y)(z)(zy↔zxB(z))
L’assioma di isolamente ci permette già di dimostrare l’esistenza di
alcuni insiemi, ad esempio l’insieme vuoto:
E di conseguenza una volta dimostratane l’unicità di estendere la teoria
introducendo una nuova costante individuale:
Ax.∅
(y)¬(y∅)
3.
Assioma dell’Unione. Per ogni insieme esiste l’insieme che è l’unione
di tutti i suoi elementi:
(x)(z)(y)(yz↔(u)(yuux))
Introduzione del predicato binario  di inclusione
Considerando la formula:
(u)(ux→uy)
Estendiamo la teoria con un nuovo predicato binario  attraverso un assioma:
Ax. (x)(y)(xy↔(u)(ux→uy))
Leggeremo la formula xy come x è sottoinsieme di y.
Assioma della Potenza. Preso un insieme qualunque esiste l’insieme
al quale appartengono tutti e soli i suoi sottoinsiemi:
(x)(y)(z)(zy↔zx)
Si è ora in grado di dimostrare il teorema necessario all’introduzione del
simbolo funzionale unario per indicare la potenza di un insieme (ma
noi non lo introdurremo).
4.
5.
Assioma della Coppia. Esiste l’insieme a cui appartengono due
insiemi:
(x)(y)(z)(u)(uz↔uxuy)
Introduzione del simbolo funzionale binario della coppia
Grazie all’assioma della coppia e all’assioma di estensionalità otteniamo:
(x)(y)(!z)(u)(uz↔uyux)
Estendiamo quindi la teoria introducendo un nuovo simbolo funzionale binario
{-,-} il comportamento del quale sarà regolato dal seguente assioma
definitorio:
Ax. {-,-}
(x)(y)(u)(u{x,y}↔uyux)
Introduciamo inoltre mediante definizione esplicita il simbolo {-} per indicare
il singoletto di un insieme:
{x}{x,x}
Introduzione del simbolo funzionale binario di intersezione.
Attraverso l’assioma di isolamento è possibile ottenere:
(x)(y)(!z)(u)(uz ↔ ux  uy)
Estendiamo la teoria attraverso l’introduzione di un nuovo simbolo funzionale
binario  regolato dal seguente assioma definitorio:
Ax. (x)(y)(u)(uxy ↔ ux  uy)
6.
Assioma di Fondazione. Ogni insieme non vuoto è disgiunto da
qualche suo elemento:
(x)(¬(x∅)→(y)(yxxy∅))
Attraverso il precedente assioma possiamo dimostrare l’inesistenza di cicli
all’interno della teoria ossia l’esistenza di catene di insiemi come xx.
E’ infatti un teorema della teoria (x)¬(xx).
Introduzione del simbolo funzionale unario dell’unione
Grazie all’assioma dell’unione e all’assioma di estensionalità otteniamo:
(x)(!z)(u)(uz↔(y)(uyyx))
estendiamo la teoria introducendo un nuovo simbolo funzionale unario di
unione , regolato dal seguente assioma definitoro:
Ax. 
(x)(u)(u(x)↔(y)(uyyx))
introduciamo inoltre il simbolo di unione binaria U attraverso la seguente
definizione esplicita:
xUy({x,y})
Il comportamento di questo simbolo è proprio quello atteso in quanto è un
teorema di Z la formula: uxUy↔uxuy.
Infatti dall’assioma dell’unione:
(u)(u({x,y})↔(z)(uzz{x,y}))
Introduzione del predicato unario di ereditarietà
Introduciamo la costante individuale 0 e il simbolo funzionale unario (…)+
definendoli esplicitamente come segue:
0∅
x+xU{x}
Chiaeremo x+ il successore di x. Come si può desumere dalla definizione il
successore di x appartengono tutti gli elementi che appartengono a x e
x stesso.
Consideriamo ora la formula:
0x(y)(yx→y+x)
E introduciamo il predicato unario Ered attraverso il seguente assioma
definitorio:
Ax. Ered
(x)(Ered(x)↔0x(y)(yx→y+x))
7.
Assioma dell’infinito. Esiste un insieme ereditario:
(x)Ered(x)
La teoria ZF
ZF si ottiene sostituendo dalla lista di assiomi di Z lo schema di
assiomi di isolamento e (potenzialmente) l’assioma della coppia
con lo schema di assiomi di rimpiazzamento.
1.
Schema di assiomi di rimpiazzamento. esiste l’insieme ottenuto da
quello dato sostituendo ognuno dei suoi elementi con al più un altro
elemento:
Presa una formula A in cui x e y non sono libere:
(u)(!!z)A(u,z)→(x)(y)(z)(zy↔(u)(uxA(u,z))
E’ possibile provare ogni occorrenza dello schema di isolamento in ZF usando
un’occorrenza dello schema di rimpiazzamento. Possiamo così
considerare tutte le occorrenze di quello che in Z era lo schema di
isolamento come teoremi di ZF.
La teoria GB nello stile di Gödel
• La sintassi di GB(G) è costruita pensando agli individui di un
ipotetico suo modello non in termini di insiemi ma in termini di classi.
• Tutti gli insiemi sono classi ma non tutte le classi sono insiemi.
• Le classi che non sono insiemi sono dette classi proprie.
• GB(G) permette di recuperare uno schema di assiomi di
comprensione (opportunamente limitato) tra gli assiomi della teoria.
• GB(G) permette di esprimere l’esistenza di classi come la classe di
Russell o la Classe di tutti gli insiemi senza incorrere nelle
contraddizioni nel modo consueto.
• E’ equicoerente rispetto a ZF: se abbiamo fiducia in ZF dovremmo
averne anche in GB(G)
La teoria GB(G) si compone di 10 tipi di assiomi:
1.
Assioma di Estensionalità. Se due classi hanno gli stessi elementi allora
sono identiche:
(x)(y)((z)(zx↔zy)→xy)
L’assioma di estensionalità GB(G) è sintatticamente identico all’assioma di
estensionalità di Z e ZF, tuttavia il significato inteso è differente. Le
variabili individuali di GB(G) infatti variano su classi e non su insiemi e
come vedremo i due termini non sono sinonimi.
Introduzione del predicato unario Set(…)
Considerata la formula: (x)(yx), estendiamo la teoria mediante definizione
introducendo il predicato unario Set(…) attraverso il seguente assioma
definitorio
Ax.Set
(y)(Set(y)↔(x)(yx))
Formule relativizzate e formule predicative
Definizione 1. Una formula è detta relativizzata se ogni quantificatore che vi
compare opera su una formula B del tipo seguente:
Nel caso si tratti di un quantificatore universale:
Nel caso si tratti di un quantificatore esistenziale:
Definizione 2. Una formula A èdetta predicativa se è esiste una formula B
relativizzata tale che:
2.
Assioma di comprensione. Per ogni formula predicativa esiste la
classe di tutti e soli gli insiemi che la soddisfano:
Sia A predicativa e sia x ∉Lib(A); allora è un assioma:
(1.1.1) (x)(y)(yx↔Set(y)A)
Ne è una formulazione equivalente:
(1.1.2) (x)(y)(Set(y)→(yx↔A))
Introduzione della costante individuale U per indicare la classe universo
Grazie alla comprensione è ora possibile considerare l’esistenza della classe a
cui appartengono tutti gli insiemi:
(x)(y)(Set(y)→ yx)
e tramite l’assioma di estensionalità non è difficile ottenere:
(!!x)(y)(Set(y)→ yx)
Permettendoci così di ottenere:
(!x)(y)(Set(y)→ yx)
Introduciamo ora il simbolo U mediante il seguente assioma definitorio:
Ax.U
(y)(Set(y)→ yU)
A differenza di Z e ZF, la teoria GB(G) risulta quindi essere in grado di
esprimere l’esistenza di un entità a cui appartengono tutti gli insiemi non
essendo quest’ultima a sua volta un insieme.
È infatti un teorema della teoria ¬Set(U)
Per la dimostrazione del precedente teorema possiamo ricorrere
all’assioma di fondazione:
Oppure in modo apparentemente più laborioso farne a meno:
Inoltre dalla definizione di Set(…) si ha:
(yU)(Set(y))
Poché se una classe appartiene a qualche classe è un insieme, possiamo
stabilire con un teorema l’equivalenza tra l’essere un insieme e
l’appartenere alla classe universo:
(y)(yU↔Set(y))
Ogni volta che incontriamo una formula in cui compare il predicato Set
possiamo ottenere una formula equivalente sostituendo le presenze
di Set(…) all’interno della formula con …U.
In particolare possiamo riformulare l’assioma di comprensione nel
modo seguente:
Per ogni formula predicativa A che non contenga presenze
libere di y:
(y)(xU)(xy↔A)
Introduzione della costante individuale ∅ per indicare la classe
vuota
Come nel caso della classe universo attraverso l’assioma di
comprensione otteniamo l’esistenza della classe che ci interessa e
attraverso l’assioma di estensionalità la sua unicità.
(!x)(y)(¬(yx))
Possiamo quindi introdurre (mediante definizione) la nuova costante
individuale ∅ con assioma definitorio:
Ax.∅
(y)(¬(y∅))
Introduzione del simbolo funzionale binario della coppia
In ZF l’introduzione del simbolo per indicare la coppia richiedeva un
assioma specifico. In GB(G) il teorema necessario per la
formulazione dell’assioma definitorio si ottiene direttamente dagli
assiomi di comprensione e di estensionalità.
Ax.{-,-}
(u)(z)(yU)(y{u, z}↔yuyz)
Si rivelerà inoltre utile introdurre accanto al simbolo funzionale della
coppia anche il simbolo funzionale unario di singoletto e quello binario
di coppia ordinata attraverso delle definizioni esplicite:
– {x}{x,x}
– x,y{{x,y},{x}}
Coppie di Classi
In GB(G) ha senso non solo parlare di coppie di insiemi ma anche di
coppie di classi proprie e di coppie “miste”. I comportamenti di tali
simboli funzionali saranno diversi in relazione al tipo di individui su cui
opereranno.
•
Set(x)¬Set(y)→{x,y}{x}
•
¬Set(x)¬Set(y)→{x,y}∅
Per assicurarsi che la classe formata dalla coppia di due classi si
comporti sugli insiemi come ci si potrebbe aspettare, è necessario
introdurre l’apposito assioma.
3.
Assioma della Coppia. Se due classi sono insiemi allora lo è
anche la loro coppia:
(y)(x)(Set(x)Set(y)→Set({x,y}))
Questo assioma garantisce anche per le coppie ordinate.
Introduzione del predicato binario  di inclusione
Considerando la formula (u)(ux→uy) si estende la teoria attravero
il seguente assioma:
Ax.
(x)(y)(xy↔(u)(ux→uy))
Introduzione del simbolo funzionale unario P(…) della potenza
Attraverso gli assiomi di comprensione e di estensionalità si ottiene:
(u)(!x)(yU)(yx↔yu))
Estendiamo la teoria con un nuovo simbolo funzionale unario P(…):
Ax.P
(u)(yU)(yP(u)↔yu)
Leggeremo il simbolo P(u) come la potenza di u.
Sottolineiamo inoltre che ad una classe potenza non appartengono tutte
le sottoclassi di una classe ma soltanto tutti i suoi sottoinsiemi.
4.
Assioma della potenza. se una classe è un insieme allora lo è
anche la classe di tutti i suoi sottoinsiemi:
(x)(Set(x)→Set(P(x))
Introduzione del simbolo funzionale  per indicare l’insieme
unione
La formula (y)(yxuy) è predicativa. Possiamo così considerare una
occorrenza dello schema di comprensione ad essa corrispondente:
(x)(z)(uU)(uz↔(y)(yxuy))
Attraverso l’assioma di estensionalità si ottiene :
(x)(!z)(uU)(uz↔(y)(yxuy))
Si può ora estendere la teoria con un nuovo simbolo funzionale unario
 mediante il seguente assioma definitorio:
Ax. 
(x)(uU)(u(x)↔(y)(yxuy))
Introduzione del simbolo funzionale binario u di unione binaria
Per preservare il comportamento “corretto” dell’unione binaria non possiamo
definire il simbolo funzionale corrispondente in modo esplicito come
abbiamo fatto in ZF. Infatti:
¬Set(x)¬Set(y)→({x,y}) ∅
Attraverso gli assiomi di comprensione e di estensionalità si ottiene:
((x)(y)(!u)(zU)(zu↔zxzy)
Estendiamo quindi la teoria mediante il seguente assioma:
Ax. U
(x)(y)(zU)(zxuy↔ zxzy)
Definiamo inoltre il simbolo di successiva di una classe attraverso la seguenti
identità:
x+xu{x}
5.
Assioma dell’unione. se una classe è un insieme allora lo è anche la
classe composta da tutti gli insiemi appartenenti agli elementi della
prima:
(x)(Set(x)→Set((x)))
Introduzione del simbolo funzionale binario  di intersezione
binaria
Attraverso gli assiomi di comprensione e di estensionalità si ottiene:
(x)(y)(!u)(zU)(zu↔zxzy)
Si può ora estendere la teoria con un nuovo simbolo funzionale binario
 mediante il seguente assioma definitorio:
Ax. 
(x)(y)(zU)(zxy↔ zxzy)
6.
Assioma di isolamento. L’intersezione di un insieme con una
classe è un insieme:
(x)(Set(x)→(y)Set(xy))
Grazie al precedente assioma possiamo facilmente dimostrare che ogni
sottoclasse di un insieme è un insieme:
(x)(y)(Set(x)yx→Set(y))
7.
Assioma di fondazione. Ogni insieme non vuoto è disgiunto da
qualche suo elemento:
(xU)(¬(x∅)→(y)(yx(yx∅))
Introduzione del predicato unario per indicare le classi relazionali
Considerando la formula (y)(yx→(uU)(zU)( y<u,z>)) si estende la
teoria introducendo il predicato Rel(…) mediante seguente assioma:
Ax. Rel
Rel(x)↔(y)(yx→(uU)(zU)(y<u,z>))
Diremo essere relazionali le classi soddisfacenti il predicato Rel.
Introduzione del predicato unario per indicare le classi univoche
Considerata la formula (yU)(uU)(zU)((<y,u>x<y,z>x)→uz), si
estende la teoria introducendo il predicato unario Un(…) mediante il
seguente assioma:
Ax.Un
Un(x)↔(yU)(uU)(zU)((<y,u>x<y,z>x)→uz)
Diremo essere univoche le classi soddisfacenti il predicato Un.
Introduzione del predicato unario Fun(…) per indicare le classi
funzionali
Considerando la formula Rel(x)Un(x) si estende la teoria introducendo il
predicato Fun(…) mediante il seguente assioma:
Ax. Fun
Fun(x)↔ Rel(x)Un(x)
Diremo essere funzionali le classi soddisfacenti il predicato Fun.
Introduzione del simbolo funzionale unario Im(…) per indicare
l’immagine di una classe
Attraverso gli assiomi di comprensione e di estensionalità si ottiene:
(x)(!z)(uU)(uz↔(yU)(<y,u>x))
Estediamo quindi la teoria mediante il seguente assioma :
Ax. Im
(x)(uU)(u Im(x)↔(yU)(<y,u>x))
Introduzione del funzionale unario unario Dom(…) per indicare il
dominio di una classe
Attraverso gli assiomi di comprensione e di estensionalità si ottiene:
(x)(!z)(uU)(uz↔(yU)(<u,y>x))
Estendiamo la teoria mediante il seguente assioma:
Ax. Dom
8.
(x)(uU)(uDom(x)↔(yU)(<u,y>x))
Assioma di rimpiazzamento. Se una classe è funzionale e il dominio di
quella classe è un insieme, allora anche l’immagine di quella classe è
un insieme:
Fun(x)Dom(x)U→Im(x)U
Introduzione del predicato unario Ered(…) per indicare le classi
ereditarie
Introduciamo un nuovo predicato unario attraverso il seguente assioma:
Ax. Ered
Ered(x)↔∅x(y)(yx→y+x)
Introduzione della costante individuale E per indicare la classe
degli insiemi ereditari
Attraverso l’assioma di estensionalità e l’opportuna occorrenza dello schema
di comprensione otteniamo che:
(!z)(uU)(uz↔Ered(u))
Estendiamo la teoria con una nuova costante individuale E con il seguente
assioma:
Ax. E
(uU)(uE↔Ered(u))
A questo punto del suo sviluppo la teoria GB(G) è in grado di
provare l’esistenza di classi ma non l’esistenza di insiemi. La
classe vuota potrebbe infatti non essere un insieme.
Per parlare di insiemi dobbiamo introdurre un apposito assioma.
9.
Assioma dell’insieme vuoto. la classe vuota è un insieme:
Set(∅)
Il precedente assioma permette attraverso l’assioma di
comprensione di ottenere enunciati che si pronunciano
sull’esistenza di classi ereditarie, tuttavia non basta per
assicurare l’esistenza di insiemi ereditari.
La minima classe ereditaria
L’assioma dell’insieme vuoto è però sufficiente per dimostrare:
Ered((E))
Il precedente teorema segnala anche che nel caso ci fossero insiemi
ereditari (E) sarebbe la minima classe ereditaria. Infatti dalla
definizione di intersezione si ha: (x)(x(E)↔(z)(zE→xz))
da cui si ottiene: (x)(xE→(E)x) .
10.
Assioma dell’infinito. L’intersezione della classe delle classi
ereditarie è un insieme:
Set((E))
La teoria GB nello stile di Bernays
Al contrario di GB(G), GB(B) distingue nettamente tra ciò che è una
classe e ciò che è un insieme.
Tale differenza nel sistema precedente era parzialmente nascosta, qui
invece si vuole mettere in luce la natura differente dei due tipi di enti.
Gli uni (le classi) sono originate da considerazioni meramente logico
linguistiche (estensioni di predicati).
Gli altri sono gli oggetti della matematica indipendenti dalle astrazioni
linguistiche.
Il linguaggio
Il linguaggio di GB(B) si compone dei seguenti simboli primitivi:
• I simboli logici di una logica del prim’ordine con l’identità
• I predicati unari C e S
• I predicati binari e e g
La teoria GB(B)
1.
Non vi sono altri enti oltre alle classi e agli insiemi:
(x)(C(x)S(x))
2.
Nessuna classe è un insieme:
(x)(S(x)→¬C(x))
3.
Se un elemento afferisce a un altro elmento allora sono
entrambi insiemi.
(x)(y)(xey→S(x)S(y))
4.
Se un elemento soddisfa un altro elemento allora il primo è un
insieme e il secondo una classe.
(x)(y)(xgy→S(x)C(y))
5.
Assioma di estensionalità.
–
Per insiemi: se a due insiemi afferiscono gli stessi
elementi allora sono identici:
(xS)(yS)((zS)(zey↔zex)→xy)
–
Per classi: se due classi sono soddisfatte dagli stessi
elementi allora sono la stessa classe:
(xC)(yC)((zS)(zgy↔zgx)→xy)
6.
Schema di assioma di comprensione. Per ogni formula
predicative A esiste la classe soddisfatta dagli insiemi che
soddisfano A.
Sia A una formula predicativa e sia Lib(A)={x1,…,xm,u} e sia 0km
ponendo yi=xk+i in modo che x1,…,xm=x1,…, xk, y1,…, yn con
n=m-k, allora è un assioma dello schema:
(x1,…, xkS)(y1,…, ynC)(zC)(uS)(ugz↔A)
Lo schema di comprensione a differenza della comprensione di GBB
non si presenta come la chiusura universale di un esistenziale ma
piuttosto come la chiusura universale di una implicazione.
I simboli funzionali che introdurremo saranno quindi condizionati.
Simboli funzionali condizionati
Data una teoria del primo ordine T, siano A(x1,…, xk) e B(x1,…,xk,y)
due formule tali che:
(x1,…, xk)(A(x1,…, xk)→ (!y)B(x1,…, xk, y))
Allora possiamo estendere definitorimente T a T ' aggiungendo un
simbolo funzionale (k-ario) f con un opportuno assioma:
(x1,…, xk)(A(x1,…, xk)→B(x1,…, xk, f(x1,…, xk)))
L’introduzione di simboli funzionali condizionati risulterà
particolarmente utile per introdurre simboli funzionali il cui
comportamento è interessante solo riguardo a particolari tipi di
termini
Introduzione della costante individuale ∅
La formula ¬(uu) è predicativa dunque è un assioma:
(xC)(uU)(ugx↔¬(uu))
Attraverso l’assioma di estensionalità per classi, si ottiene poi:
(!xC)(uS)(¬(ugx))
Possiamo quindi introdurre (mediante definizione) la nuova costante
individuale ∅ con assioma definitorio:
Ax. ∅
C(∅)(uS)(¬(ug∅))
Introduzione della costante individuale U per indicare la classe
universo
Poiché la formula (uu) è predicativa possiamo considerare
l’opportuna occorrenza dello schema di assiomi di comprensione e
attraverso l’estensionalità per classi dimostrare il seguente teorema:
(!xC) (uS)(ygx)
Introduciamo ora il simbolo U mediante il seguente assioma:
Ax.U
C(∅)(yS)(ugU)
Introduzione del predicato binario R per indicare la relazione di
rappresentazione
Sia gli insiemi che le classi, accettando come elementi delle proprie
estensioni unicamente gli insiemi, dànno luogo alla possibilità che
un insieme e una classe, abbiano la stessa estensione. Quando ciò si
verifica, si dice che la classe è rappresentata dal dato insieme o che
l’insieme rappresenta la classe.
Per esprimere esplicitamente tale relazione si introduce il seguente
predicato binario R:
Ax. R
R(x,y)↔S(x)C(y)(zS)(z y↔z x)
Introduzione del predicato unario Rep
Una classe è detta rappresentabile se esiste un insieme che la
rappresenta:
Ax. Rep
Rep(y)↔(x)(R(x,y))
Come non è difficile immaginare non tutte le classi saranno
rappresentabili.
È un teorema di GB(B):
¬Rep(U)
Per ogni classe che in GB(G) risultava essere propria qui avremo il
teorema per affermare che la “corrispondente” di quella classe non è
rappresentabile.
Introduzione del simbolo funzionale unario c
Attraverso gli assiomi di comprensione e di estensionalità si ottiene:
(xC)(!u)(zS)(zgu↔(y)(ygx→zey)
Estendiamo la teoria mediante il seguente assioma:
Ax.c
(xC)(zS)(zgc(x)↔(y)(ygx→zey)
Si definisce esplicitamente l’intersezione di due insiemi:
xssyc({x,y}ss)
Introduzione del simbolo funzionale binario sc
Attraverso gli assiomi di comprensione e di estensionalità si ottiene:
(xS)(yC)(!u)(zS)(ugx↔uexugy)
Si può ora estendere la teoria con un nuovo simbolo funzionale binario:
Ax.sc
(xS)(yC)(uS)(ugxscy↔uexugy)
7.
Assioma di isolamento. L’intersezione tra un insieme e una
classe è rappresentabile:
(x)(S(x)→(y)Rep(xscy))
8.
Assioma di fondazione. Ogni insieme non vuoto è disgiunto da
qualche suo elemento.
(xS)(¬(x∅)→(y)(yex(yssx∅))
Introduzione del simbolo funzionale s per indicare l’unione di un
insieme
Poiché (yS)(ueyyex) è predicativa, attraverso gli assiomi di
comprensione e di estensionalità si ottiene:
(xS)(!z)(uS)(ugz↔(yS)(ueyyex)
Estendiamo ora la teoria mediante il seguente assioma:
Ax.s
9.
(xS)(uS)(u s(x)↔(yS)(yexuey)
Assioma dell’unione. La classe unione di un insieme è
rappresentabile:
(x)(S(x)→Rep(s(x)))
Grazie al precedente assioma siamo in grado di dimostrare che
(x)(Rep(x)→Rep(c(x))
Introduzione del simbolo funzionale unario rs
Dalla comprensione e dall’estensionalità si ottiene:
(yS)(!x)R(y, x)
Per indicare la classe rappresentata da un insieme introduciamo un
nuovo simbolo mediante il seguente assioma:
Ax. rs
(yS)R(y, rs(y))
Introduzione del simbolo funzionale unario rc
Attraverso l’assioma di estensionalità otteniamo:
(xC)(!y)(Rep(x)→xrs(y))
Per indicare l’insieme che rappresenta una classe introduciamo un
nuovo simbolo funzionale mediante apposito assioma:
Ax.rc
(xC)(Rep(x)→xrs(rc (x)))
Introduzione del simbolo funzionale binario {-,-}ss , coppia di
insiemi
Dalla comprensione e dall’estensionalità si ottiene:
(xS)(yS)(!z)(uS)(ugz↔uxuy)
Introduciamo ora il simbolo {-,-}ss mediante il seguente assioma:
Ax. {-,-}ss
(xS)(yS)((uS)(ug{x,y}ss↔xuyu)
10.
Assioma della coppia: La coppia di due insiemi è
rappresentabile.
(x)(y)(S(x)S(y)→Rep({x,y}ss))
Coppia ordinata
Similmente a quanto fatto in GB(G) si definisce esplicitamente il
singoletto di un insieme:
{x}s{x,x}ss
Definiamo invece il simbolo di coppia ordinata nel modo seguente:
x,yrc({rc({x,y}ss),rc({x}ss)}ss)
Introduciamo mediante definizione esplicita il simbolo binario di
unione tra due insiemi e il simbolo di coppia ordinata:
xUssys(rc({x,y}ss))
x+rc({x}s)Ussx
11.
Assioma della potenza: La classe potenza di un insieme è
rappresentabile.
(x)(S(x)→Rep(Ps(x) ))
Grazie al precedente assioma siamo in grado di dimostrare che:
(x)(Rep(x)→Rep(Pc(x))
12.
Assioma di rimpiazzamento. Se una classe è funzionale e il
dominio di quella classe è rappresentabile, allora anche
l’immagine di quella classe è rappresentabile.
Func(x)Rep(Domc(x))→Rep(Imc(x))
13.
Assioma dell’insieme vuoto: La classe vuota è rappresentabile.
Rep(∅)
Introduzione della costante individuale 0 per indicare l’insieme
vuoto
Grazie all’assioma dell’insieme vuoto e poiché se una classe è
rappresentabile allora esiste un solo insieme che la rappresenta,
possiamo introdurre attraverso definizione esplicita la costante
individuale riferita all’insieme vuoto:
rc (∅)0
14.
Assioma dell’infinito. L’intersezione della classe degli insiemi
ereditari è rappresentabile:
Rep(c(E) )
FINE