Circolarità

Minor Thesis

Dott. Marco Giovanni Benini

Dottorato di Ricerca XI Ciclo

Dipartimento di Scienze dell’Informazione

Università degli Studi di Milano

Sommario

In questo lavoro analizzeremo il concetto di circolarità, ovvero come sia possi-bile definire una teoria matematica generale in cui dare definizioni autoreferenziali,garantendo l’esistenza ed unicità del definendo.

L’esempio più semplice é dato dalle definizioni induttive, ma, in questo lavorointendiamo analizzare metodi più generali di individuazione di oggetti che non sianoriducibili al caso di definizione per induzione.

Per fare ciò, descriveremo la teoria degli insiemi non ben fondati, ed in essasvilupperemo alcuni esempi particolarmente significativi, tratti dall’Informatica edalla Matematica.

Mostreremo come la teoria generale di cui trattiamo sia al contempo sufficente-mente potente da fornire per ognuno degli esempi una soluzione esatta, con tuttele proprietà che ragionevolmente possiamo attenderci da essa, ma anche come taleteoria generale sia naturale, ovvero il tipo di formalizzazione che daremo per ogniesempio rispecchia fedelmente, e semplicemente, l’idea intuitiva soggiacente.

15 marzo 1998

Indice

1 Introduzione . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

1.1 Fenomeni Circolari . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

1.2 Paradossi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2 Teoria degli Insiemi Non Ben Fondati . . . . . . . . . . . . . . . . . . . . . . . . . 9

2.1 ZF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

2.2 ZFA. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

2.3 Consistenza di ZFA . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

2.4 Punti Fissi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

2.5 Bisimulazione . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

3 Applicazioni . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

3.1 Esempi Introduttivi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

3.2 Soluzione ai Paradossi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

3.3 Insiemi Ereditariamente Finiti . . . . . . . . . . . . . . . . . . . . . . . . . . . 45

4 Conclusioni . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

Riferimenti bibliografici . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51

Indice analitico . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55

i

1 Introduzione

In questo lavoro intendiamo analizzare il concetto di circolarità ed illustrareun insieme di strumenti e tecniche per modellare fenomeni circolari.

Il concetto di circolarità é facilmente definibile in termini matematici:

Definizione 1 Una relazione binaria R si dice non ben fondata se esiste unasequenza infinita b0, . . . , bn, . . . tale che, per ogni n ∈ N, bn+1 R bn.

Definizione 2 Una relazione binaria R si dice circolare se esiste una se-quenza finita b0, . . . , bk con b0 ≡ bk tale che bn+1 R bn, per ogni n, 0 ≤ n <k.

Il punto di partenza per la nostra analisi é dato dalla osservazione:

Proposizione 3 Una relazione circolare é non ben fondata.

Lo scopo di questa introduzione é triplice:

• mostrare come l’idea di circolarità ricorra frequentemente in molti campidella Matematica e dell’Informatica;• illustrare i problemi che, storicamente, questa nozione ha introdotto;• discutere brevemente, e tecnicamente, il significato che una teoria della

circolarità induce nell’usuale pratica matematico/informatica.

Per quanto il taglio di questo lavoro sia teorico, da alcuni anni, specialmentenelle discipline legate all’Intelligenza Artificiale, molte applicazioni pratichedei concetti che illustreremo sono state efficacemente usate per risolvere prob-lemi difficili [Pau92,Pau93,Bar89].

1.1 Fenomeni Circolari

In questa prima sezione, illustreremo alcuni fenomeni che, in modo più o menodiretto, danno il sapore del concetto di circolarità.

Prima di addentrarci nei dettagli, vorremmo dare giustificazione del modo incui presenteremo tali esempi. Innanzitutto useremo la parola circolare in modomolto informale, cercando, prima di affrontare un’analisi matematica precisa,di “costruire” una intuizione del concetto.

In secondo luogo, cercheremo di definire qual’é un’attesa ragionevole per unateoria della circolarità.

1

In modo informale sempre, cercheremo di suggerire che, in un certo senso, ladescrizione di un fenomeno circolare si riduce a dare una definizione mate-matica di cui occorre garantire la bontà, ovvero che il definendo esista e siaunivocamente determinato.

Questa sarà la chiave che consentirà, con una generalizzazione verso strutturenon ben fondate, come già accennato in precedenza, di costruire una teoriache permetta di trattare i fenomeni che stiamo per descrivere soddisfacendotutti i requisiti che andremo a delineare.

1.1.1 Sequenze

Alcune strutture dati concrete sono difficili da caratterizzare in forma di unmodello matematico astratto [AHU83].

Un esempio comune é il file: esso é descrivibile come una sequenza di datiaventi tutti lo stesso tipo. L’idea chiave di sequenza pone qualche difficoltà.

Ciò che vorremmo catturare é una definizione formale che esprima una se-quenza come una lista potenzialmente infinita.

Una lista (il tipo di dato lista) é descritto come:

• Nil é una lista di α;• se a é un oggetto di tipo α, e l é una lista di α, allora Cons a l é una lista

di α;• niente altro é una lista di α.

Questa definizione é circolare, ma la clausola finale forza ad una definizioneinduttiva, quindi la definizione é ben data.

Vorremmo poter definire in modo analogo una sequenza di α, con la possibilitàdi dimostrare le proprietà rilevanti di questa struttura dati, quali quelle chela distinguono dalle liste: l’equazione

x = Cons a x

non ammette soluzioni se x é una lista, mentre ammette come soluzione lastringa di lunghezza infinita composta di sole a, se x é una sequenza.

Questo esempio ci dice che una teoria della circolarità “accettabile”, devecontenere l’induzione (per poter trattare le liste), ma non deve limitarsi adessa: in particolare deve permettere di definire strutture dati infinitarie comele sequenze.

2

1.1.2 Chiusure

Una costruzione algebrica [MB65,Lan65] spesso utilizza lo strumento dellachiusura: data una relazione τ , si definisce la relazione τ c come la più piccolarelazione contenente τ che sia chiusa rispetto ad una o più operazioni e/oproprietà.

Un esempio é la chiusura riflessiva e transitiva: se τ é una relazione su S, τ ∗ éla più piccola relazione su S tale che:

• τ ⊆ τ ∗ ,• ∀x ∈ S. x τ ∗ x ,• ∀x, y, z ∈ S. x τ ∗ y ∧ y τ ∗ z → x τ ∗ z .

Una definizione per chiusura é circolare: formalizzando il concetto di “piùpiccola relazione tale che”, otteniamo, nel caso dell’esempio

∀ρ. ρ ⊆ τ ∧ (∀x ∈ S. x ρ x) ∧ (∀x, y, z ∈ S. x ρ y ∧ y ρ z → x ρ z)→ τ ∗ ⊆ ρ .

La circolarità é dovuta al fatto che “per ogni ρ” significa “anche per τ ∗”.Questa forma di circolarità é nota come impredicatività [Bar84,JH56].

Il concetto di chiusura suggerisce naturalmente una costruzione duale: datauna relazione τ , si definisce la relazione τc come la più grande relazione con-tenuta in τ che sia chiusa rispetto ad una o più operazioni e/o proprietà.Converremo di chiamare questa costruzione co-chiusura, sfruttando il mododi dare nomi ai concetti duali tipico della Teoria delle Categorie [Mac71].

Queste considerazioni ci portano a desiderare una teoria della circolarità chedescriva i fenomeni di impredicatività, ma che permetta anche di identificare,in modo uniforme, costruzioni duali.

1.1.3 Auto-Applicazione

Una delle caratteristiche salienti del λ-Calcolo [Bar84] e della Logica Combi-natoria [HS86,CF58] é la possibilità di applicare un operatore a se stesso. Lapossibilità é ampiamente sfruttabile per codificare, ad esempio, la ricorsione[Tur37]. Tuttavia possono presentarsi fenomeni di natura patologica, che sonooggetto di studio in queste discipline.

Consideriamo i combinatori:

I = S KK

3

e

ω = λx. x x

dove, al solito,

S = λx y z.(x z)(y z)

e

K = λx y. x .

Sfruttando le regole di riduzione dei rispettivi sistemi, possiamo dedurre che:

• I I = S KK I = K I (K I) = I ,• ω ω = (λx. x x)ω = ω ω = . . . ,• I ω = S K K ω = K ω (K ω) = ω ,• ω I = (λx. x x) I = I I = I .

Come vediamo I I,I ω e ω I ammettono una forma normale, mentre ω ω noné riducibile che a se stesso.

Se, come consuetudine quando si usi il λ-Calcolo per modellare qualche altrosistema, immaginiamo un termine come una “definizione” per (l’unico) “va-lore” costituito dalla sua forma normale, Ω = ω ω é una definizione circolareche non individua alcun elemento.

L’accento in questi esempi é posto sulla convergenza della definizione circolare:I I converge ad I, mentre ω ω diverge. indexdivergenza

Un criterio che ci aspettiamo emergere dalla teoria della circolarità, é unadescrizione/discriminazione tra criteri “convergenti” e “divergenti”. I primipermetteranno di definire un oggetto, i secondi saranno utili per un’analisiastratta della struttura matematica sottostante al mondo in considerazione.

1.1.4 Concorrenza

Il problema basilare nell’Algebra dei Processi [Mil73] consiste nell’identifi-cazione, ovvero quando due espressioni sintatticamente differenti designano lostesso fenomeno. A questo scopo viene introdotta la nozione di bisimulazione.

Supponiamo di usare l’algebra dei CCS [Mil89]; un processo P bisimula unprocesso Q (P ≈ Q) se e solo se:

∀α, P ′. Pα−→ P ′ → ∃Q′. Q

α−→ Q′ ∧ P ′ ≈ Q′ (1)

4

e

∀α,Q′. Qα−→ Q′ → ∃P ′. P

α−→ P ′ ∧ P ′ ≈ Q′ (2)

In parole, se, ogni volta che P effettua una azione, riducendosi a P ′, Q puòeffettuare la stessa azione, riducendosi ad un Q′ tale che P ′ bisimuli Q′; lastessa cosa avviene per Q.

É immediato provare che la relazione ≈ é di equivalenza, quindi essa può essereusata come uguaglianza. Si può provare [Mil89] che ≈ é una congruenza, percui é un concetto che ben si adatta all’identificazione di termini.

É anche evidente la circolarità della definizione, ma é facile convincersi chenon si tratta di una definizione per induzione, potendo P ′ essere uguale (sin-tatticamente) a P :

α . µX . α . X ≈ µX . α . X .

Modificando la definizione base si ottengono altre forme utili di bisimulazione:se nel conseguente di (1) e (2) si sostituisce a

α−→, la riduzione osservazionale

α̂=⇒ [Mil80], otteniamo la bisimulazione debole, che identifica processi chehanno lo stesso comportamento sulle azioni osservabili.

Si possono introdurre parecchie modifiche nello schema base di bisimulazione[Mil80], ottenendo un modo di confrontare processi, anche infiniti, che neespleti l’aspetto “comportamentale” rispetto a quello “strutturale”.

Il problema che riveste maggiore interesse dal punto di vista della circolarità é:quando, e perché, una bisimulazione é ben definita ? Ovvero, come é possibilegarantire che esista una, ed una sola, relazione soddisfacente alle condizioni(o a varianti di) (1) e (2) ?

1.2 Paradossi

Qualsiasi forma una teoria della circolarità possa assumere, é necessario cheessa faccia fronte ad un insieme di problemi che sono dati dai paradossi.

Presentiamo ora di seguito una piccola selezione di paradossi; in alcuni ve-dremo come la nozione di circolarità é solo la porta che permette il passaggiodell’inconsistenza, ma in altri casi, la circolarità é il supporto principale su cuiil paradosso poggia.

5

É evidente che ogni teoria soddisfacente della circolarità debba fornire unasoluzione ai paradossi di cui stiamo per parlare.

1.2.1 Russell

Forse il più noto paradosso della matematica é il paradosso di Russell [Rus06].Consideriamo l’insieme R = {x | x 6∈ x}; se R 6∈ R allora deve essere R ∈ R;se R ∈ R allora, per definizione, R 6∈ R. In entrambi i casi otteniamo unacontraddizione.

Come é noto, questo paradosso ammette una semplice soluzione: abbiamoassunto, erroneamente, che R sia un insieme. Se R non é un insieme, R nonpuò essere elemento di un insieme, quindi le espressioni R ∈ R e R 6∈ R sonosintatticamente errate, poichè la relazione di appartenenza ∈ é definita trainsiemi e classi. Il paradosso dice che R é una classe che non é un insieme.

Dal punto di vista della circolarità, vale la pena sottolineare che il parados-so non nasce dall’autoriferimento. Se modifichiamo lievemente l’enunciato,questo fatto risulta evidente:

Rb = {x ∈ b | x 6∈ x} .

Quanto ci dice la costruzione di Russell é, semplicemente, che Rb 6∈ b.

1.2.2 Mentitore

Un paradosso classico che riguarda le asserzioni circolari é il paradosso delmentitore [Kri75,Mar84]: la sua forma più semplice é

io sto dicendo il falso. (3)

Se assumiamo l’asserzione (3) vera, allora (3) deve essere falsa, ottenendo unassurdo. Se (3) é falsa, allora deve essere vera, assurdo.

Una formulazione equivalente é: questa asserzione é falsa.

Come noto dal Teorema di Gödel [Göd31], questo paradosso può essere formu-lato in numerose teorie matematiche, ad esempio l’Aritmetica di Peano, conla conseguenza che esse sono incomplete, ovvero che esistono enunciati inde-cidibili. Di più, esse sono incompletabili, ovvero é sempre possibile estenderetali teorie, ma, in ogni possibile estensione sensata (effettivamente assiomatiz-zabile), é possibile riformulare il paradosso del mentitore, costruendo, di fatto,un enunciato indecidibile [Tar39].

6

La chiave di volta che genera il paradosso, ancora una volta, non é la circo-larità, ma la nostra interpretazione di questa asserzione e di falso: il fatto che“questa” sia formalmente costruibile induce la circolarità nel sistema formale,ma ciò che effettivamente genera il paradosso, come il Teorema di Gödel prova,é che noi assumiamo, arbitrariamente, che ogni asserto sia dimostrabilmentevero oppure dimostrabilmente falso.

1.2.3 Ipergioco

Il paradosso dell’ipergioco [Zwi87] ha una natura lievemente diversa dai prece-denti. La sua formulazione é la seguente: sia G una qualsiasi gioco che si svolgafra due contendenti. Chiameremo regolare un gioco che, dopo un numero finitodi mosse, permetta sempre di designare un vincitore; chiameremo irregolareun gioco che non goda di questa proprietà. Consideriamo l’ipergioco siffatto:se A e B sono i due antagonisti, A sceglie un gioco regolare, B effettua laprima mossa, e, se A vince, allora é anche il vincitore dell’ipergioco, viceversase B vince, allora B é il vincitore dell’ipergioco.

Apparentemente questo gioco é regolare: dovendo A scegliere un gioco regolare,esso termina dopo un numero finito di mosse con un vincitore, quindi anchel’ipergioco termina con il medesimo vincitore.

Tuttavia se l’ipergioco é regolare, allora A può scegliere l’ipergioco. Ma sesia A che B scelgono alternativamente l’ipergioco, esso non terminerà dopoun numero finito di mosse, quindi l’ipergioco é irregolare. Se l’ipergioco éirregolare, allora é facile convincersi che terminerà sempre dopo un numerofinito di mosse, e, per di più, con un vincitore, quindi é regolare.

In questo caso, la soluzione più semplice per rimuovere il paradosso, consistenel notare che la classe dei giochi regolari é grande, ovvero non é un insieme, equindi non esiste un ipergioco, nel senso che la sua definizione é mal fondata.

Questa soluzione é insoddisfacente: non insegna qualcosa, come invece accadeper il paradosso di Russell o per il paradosso del mentitore. Invece sembrache debba esistere una soluzione più profonda, che mostri come la costruzionedi un ipergioco sia impossibile in virtù di una caratteristica strutturale delconcetto di circolarità.

7

8

2 Teoria degli Insiemi Non Ben Fondati

In questa parte del lavoro intendiamo introdurre la teoria degli insiemi nonben fondati. Svilupperemo dapprima una estensione della teoria classica degliinsiemi, e quindi, useremo questa per derivare alcuni risultati sui concetti dipunto fisso e di bisimulazione.

Avendo queste basi, nella parte successiva ci occuperemo di applicare la teoriaai fenomeni circolari per analizzarli e formalizzarli.

2.1 ZF

Lo scopo che ci prefiggiamo in questa sezione é dare le basi su cui fondareuna teoria degli insiemi che contenga gli strumenti per parlare, in generale, diinsiemi non ben fondati, ed in particolare, di concetti circolari.

Noi estenderemo nel prosieguo la teoria degli insiemi di Zermelo e Frænkel(ZF) [Sho77,Hal60,Kun80]. Per chiarezza e semplicità di rifermento riportiamouna tra le possibili formulazioni:

• Estensionalità (Ext)

∀x, y. (∀z. z ∈ x↔ z ∈ y)→ x = y .

• Fondazione (FA)

∀x. (∃y. y ∈ x)→ ∃y. y ∈ x ∧ ¬∃z. z ∈ x ∧ z ∈ y .

• Comprensione (Compr)Per ogni formula ψ con variabili libere in x, z, w1, . . . , wn,

∀z, w1, . . . , wn. ∃y. ∀x. x ∈ y ↔ x ∈ z ∧ ψ .

• Coppia (Pair)

∀x, y. ∃z. x ∈ z ∧ y ∈ z .

• Unione (Un)

∀F. ∃A. ∀x, y. x ∈ y ∧ y ∈ F → x ∈ A .

9

• Rimpiazzamento (Repl)Per ogni formula ψ con variabili libere in x, y, A, w1, . . . , wn,

∀A,w1, . . . , wn. (∀x. x ∈ A→ ∃!y. ψ)→

(∃Y. ∀x. x ∈ A→ ∃y. y ∈ Y ∧ ψ) .

Nel modo usuale [Kun80], con questi assiomi, é possibile definire ⊆ (sot-toinsieme), ∅ (insieme vuoto), S (successore ordinale, S(X) = X ∪ {X}),∪ (unione), e la nozione di buon ordinamento.

Quindi i seguenti assiomi completano la presentazione di ZF:

• Infinito (Inf)

∃x. ∅ ∈ x ∧ ∀y. y ∈ x→ S(y) ∈ x .

• Potenza (Pow)

∀x. ∃y. ∀z. z ⊆ x→ z ∈ y .

• Scelta (Ch)

∀A. ∃R. R bene ordina A .

Gli assiomi importanti dal punto di vista di una estensione come quella che ciapprestiamo a fare sono l’Assioma di Fondazione e l’Assioma di Estensionalitá.

Il significato intuitivo dell’Assioma di Estensionalità é caratterizzare gli insiemicome raggruppamenti di elementi; un insieme é univocamente determinato daisuoi elementi [Sho77].

L’Assioma di Fondazione é l’assioma che serve per caratterizzare il modo lecitodi costruire insiemi al fine di evitare i paradossi quali quello di Russell. Essoafferma che un insieme deve contenere un elemento più semplice dell’insiemestesso. Si può facilmente provare [Sho77,BM91] che questo é equivalente apostulare che ogni insieme é ben fondato, secondo la definizione formale datanell’introduzione.

2.2 ZFA

La nostra euristica [Acz88], per estendere ZF, come accennato nell’intro-duzione, consiste nel costruire un sistema che consenta di modellare insieminon ben fondati. Per fare ciò sostituiremo l’Assioma di Fondazione con unnuovo assioma [BM96,BM91], generando la teoria ZFA (Zermelo-Frænkel conAntifondazione).

10

Sebbene questa sia l’unica modifica necessaria per poter costruire la nostrateoria, per facilitarne l’esposizione e per non appesantire la trattazione concondizioni accessorie, supporremo che l’universo del discorso sia partizionatoin due classi: insiemi e atomi.

Per evitare ambiguità, scriveremo “insieme” intendendo un oggetto della classedegli insiemi di ZFA, ed useremo la scrittura “Insieme” con l’iniziale maiuscolaper indicare un insieme nel senso usuale.

Con queste premesse possiamo definire il concetto chiave della nostra teoria:

Definizione 4 Un sistema (semplice) di equazioni é una tripla

ε = 〈X,C; e〉

dove

• X é un Insieme non vuoto di incognite (detto l’Insieme delle incognite diε).

• C é un Insieme di atomi.• e é una funzione che mappa ogni elemento di X in un sottoinsieme di X∪C.

Inoltre 1

• bv = ev ∩X é l’Insieme delle incognite da cui v ∈ X dipende.• cv = ev ∩ C é l’Insieme degli atomi da cui v ∈ X dipende.• una soluzione per ε é una funzione s con dominio X tale che

sv = {sw | w ∈ bv} ∪ cv .

Notazione 5 Indicheremo con VA[X] la collezione di tutti gli insiemi formatia partire da A ∪X; VA[∅] viene abbreviato in VA.

L’Assioma di Antifondazione 2 , nella sua formulazione più semplice, é:

Assioma 6 (AFA) Ogni sistema semplice di equazioni ε = 〈X,C; e〉 in ununiverso VA[X] ammette una ed una sola soluzione s, ed ogni valore sv ∈ VA.

La teoria ZFA é costituita da tutti gli assiomi di ZF, eccetto che FA ésostituito con AFA.

Per poter usare questo impianto formale, é necessario sviluppare alcuni lemmie teoremi.

1 Spesso useremo la scrittura fx invece di f(x), per evidenziare il fatto che f , e nonx, é il centro della nostra attenzione.2 In letteratura, spesso questo assioma viene chiamato Flat Solution Lemma.

11

Definizione 7 Sia ε = 〈X,A; e〉 un sistema semplice di equazioni, e sia sla sua unica soluzione; per insieme soluzione (notiamo che é un oggettodell’universo del discorso di ZFA) intendiamo {sv | v ∈ X}.

La filosofia di ZFA [BE87] é che ogni insieme deve essere l’insieme soluzionedi un sistema semplice di equazioni. La teoria che stiamo per sviluppare halo scopo precipuo di fornire un criterio di confronto per l’uguaglianza tra dueinsiemi. L’Assioma di Estensionalità, da solo, é insufficente a questo scopo,poichè più di un sistema può descrivere lo stesso insieme; quindi é neces-sario sviluppare uno strumento di confronto che modelli naturalmente il sensodell’Assioma di Estensionalità nella teoria allargata.

Iniziamo a dare un criterio di confronto tra sistemi di equazioni:

Definizione 8 Siano ε = 〈X,C; e〉 e ε′ = 〈X ′, C ′; e′〉 due sistemi semplicidi equazioni; una relazione di bisimilarità (bisimulazione) tra ε e ε′ é unarelazione R su X ×X ′ tale che:

• ∀x ∈ X. ∃x′ ∈ X ′. x R x′ ;• ∀x′ ∈ X ′. ∃x ∈ X. x R x′ ;• ∀x, x′. x R x′ → ∀y ∈ bx. ∃y

′ ∈ bx′. y R y′ ;

• ∀x, x′. x R x′ → ∀y′ ∈ bx′ . ∃y ∈ bx. y R y′ ;

• ∀x, x′. x R x′ → cx = cx′ .

Diciamo inoltre che ε e ε′ sono bisimili (ε ≡ ε′) se esiste una relazione dibisimilarità tra di essi.

Teorema 9 Due sistemi semplici di equazioni, detti ε = 〈X,C; e〉 ed ε′ =〈X ′, C ′; e′〉, hanno lo stesso insieme soluzione se e solo se sono bisimili.

Dimostrazione.

• (→)Siano s ed s′ le soluzioni di ε e ε′ rispettivamente. Sia R ⊆ X × X ′ la

relazione definita come

x R x′ se e solo se sx = s′x′ .

La relazione R é una bisimulazione tra ε e ε′:· sia x ∈ X, allora sx ∈ solution− set(ε) = solution− set(ε

′), quindi esistex′ ∈ X ′ tale che s′x′ = sx, ovvero x R x

′. Analogamente si prova lacondizione simmetrica per x′ ∈ X ′.· siano x ∈ X, x′ ∈ X ′ tali che x R x′, allora, se y ∈ bx, poichè sy ∈ sx = s

′x′ ,

deve esistere y′ tale che y′ ∈ e′x′ , e sy = s′y′ , ovvero y R y

′. Analogamentesi prova la condizione simmetrica.

12

· l’insieme degli atomi in sx é ex∩A poichè tutti gli sy sono insiemi; lo stessovale per s′x′. Se x R x

′, allora sx = s′x′ e quindi cx = ex∩A = e

′x′ ∩A = cx′ .

• (←)Supponiamo che R sia una bisimulazione tra ε e ε′, ed s e s′ siano soluzioni

di ε e ε′ rispettivamente.Poichè abbiamo assunto di avere a disposizione abbastanza incognite,

esistono abbastanza incognite nuove (non in X, nè inX ′) per coprire X×X ′.Per snellire la scrittura le indicheremo con 〈u, u′〉 dove u ∈ X e u′ ∈ X ′.

Sia ε∗ = 〈X∗, C; e∗〉 dove

X∗ = {〈v, v′〉 ∈ X ×X ′ | v R v′} ,

e

e∗〈u,u′〉 = {〈v, v′〉 ∈ X∗ | v ∈ eu ∧ v

′ ∈ eu′} ∪ cu .

Questo é un sistema semplice di equazioni e pertanto ammette una ed unasola soluzione.

Consideriamo s1〈u,u′〉 = su e s2〈u,u′〉 = s

′u′: entrambe sono soluzioni di ε

∗.

Proviamo il fatto per s1, essendo la prova per s2 simmetrica.Dobbiamo mostrare che

s1〈u,u′〉 = {s1〈v,v′〉 | 〈v, v

′〉 ∈ e∗〈u,u′〉} ∪ (e∗〈u,u′〉 ∩ C) .

Sia α ∈ s1〈u,u′〉 = su; poichè s é soluzione di ε, α = sw per qualchew ∈ eu ∩ X, oppure α ∈ eu ∩ C. Nel primo caso, esiste w

′ ∈ e′v ∩ X′

con u R v tale che w R w′, quindi 〈w,w′〉 ∈ X∗; ma questo significa cheα = sw = s

1〈w,w′〉. Nel secondo caso, α ∈ e

∗〈u,u′〉 ∩ C per definizione di e

∗〈u,u′〉.

Questo dimostra che

s1〈u,u′〉 ⊆ {s1〈v,v′〉 | 〈v, v

′〉 ∈ e∗〈u,u′〉} ∪ (e∗〈u,u′〉 ∩ C) .

Sia ora s1〈v,v′〉 ∈ {s1〈w,w′〉 | 〈w,w

′〉 ∈ e∗〈u,u′〉}, ma s1〈v,v′〉 = sv e s

1〈u,u′〉 = su,

quindi, essendo s soluzione di ε, sv = su. Se α ∈ C∩e∗〈u,u′〉, allora α ∈ C∩eu

per definizione di e∗〈u,u′〉, quindi α ∈ s1〈u,u′〉.

In totale

{s1〈v,v′〉 | 〈v, v′〉 ∈ e∗〈u,u′〉} ∪ (e

∗〈u,u′〉 ∩ C) ⊆ s

1〈u,u′〉 .

Quindi s1 é soluzione di ε∗. In modo simmetrico si prova che s2 é soluzionedi ε∗, quindi, per ogni u ∈ X, u′ ∈ X ′ tali che u R u′,

su = s1〈u,u′〉 = s

2〈u,u′〉 = s

′u′ .

Sia β ∈ solution− set(ε), allora β = sx per un qualche x ∈ X. Ma R éuna bisimulazione, quindi esiste x′ ∈ X ′ tale che x R x′.

13

Per quanto sopra, sx = s′x′ = β, quindi β ∈ solution− set(ε

′). Persimmetria vale anche il viceversa, quindi ε e ε′ hanno lo stesso insiemesoluzione. 2

La conseguenza diretta del teorema appena provato é che esiste un buon crite-rio di confronto per gli oggetti del discorso di ZFA; é sufficente considerare isistemi di equazioni che generano gli insiemi per poter confrontare gli insiemistessi.

Il fatto di ragionare con sistemi di equazioni e le loro bisimulazioni é scomodoed inelegante. Quindi deriviamo un criterio di confronto che richieda l’analisisolo di insiemi.

Definizione 10 Una bisimulazione tra insiemi é una relazione binaria R taleche, se a R b, con a e b insiemi,

• ∀c ∈ a. ∃d ∈ b. c R d ,• ∀d ∈ b. ∃c ∈ a. c R d ,• ∀x. x ∈ a↔ x ∈ b ,

dove c, d sono insiemi ed x é un atomo.

Teorema 11 (Estensionalità Forte) Se R é una bisimulazione tra insiemi,allora R ⊆ I, la relazione identica. Ovvero se a R b, allora a = b.

Dimostrazione. Iniziamo notando che I é una bisimulazione, applicandobanalmente la definizione.

Siano a e b due insiemi tali che a R b.

Siano inoltre εa = 〈Xa, Ca; ea〉 e εb = 〈Xb, Cb; e

b〉 i due sistemi canonici per ae b, ovvero

Ca = {x ∈ a+ | x é un atomo} Cb = {x ∈ b

+ | x é un atomo}

Xa = {a}+ \ Ca Xb = {b}

+ \ Cb

eax = x ebx = x

dove α+ é la chiusura transitiva 3 di α.

É immediato verificare che la soluzione di εa e di εb é la funzione identica.

3 α+ = {x | x ∈ α ∨ ∃y. x ∈ y ∧ y ∈ α+}

14

Sia α ∈ Ca, allora α ∈ a′ ∈ a+ per un qualche a′:

a′ = an ∈ . . . ∈ a0 = a .

Poichè R é una bisimulazione, per induzione su n, esiste b′ ∈ Cb tale chea′ R b′, ovvero α ∈ Cb, essendo α un atomo.

Quindi Ca ⊆ Cb; simmetricamente si prova che Cb ⊆ Ca, quindi Ca = Cb.

Sia R∗ la restrizione di R a Xa ×Xb, e sia

Ya = {x ∈ Xa | ∃x′ ∈ Xb. x R

∗ x′} .

Ma a ∈ Ya e se x ∈ Ya e y ∈ x, allora y ∈ Ya, essendo Xb un insieme chiuso pertransitività. Quindi, essendo {a}+ il più piccolo insieme contenente a chiusoper transitività, Xa ⊆ Ya.

Nello stesso modo si dimostra che Xb ⊆ Yb.

Sia ora x R∗ y e x′ ∈ eax∩Xa, quindi x′ ∈ x∩Xa, e x

′ é un insieme. Essendo Runa bisimulazione tra insiemi, esiste y′ ∈ y tale che x′ R y′, e, per transitivitàdi Xb, y

′ ∈ Xb, quindi y′ ∈ eby ∩Xb e x

′ R y′.

Sia x R∗ y, quindi

Ax = {α ∈ x | α é un atomo} = {α ∈ y | α é un atomo} = Ay .

Ma Ax ⊆ Ca e Ay ⊆ Cb, quindi eax∩Ca = x∩Ca = Ax ed e

by ∩Cb = Ay, ovvero

eax ∩ Cs = eby ∩ Cb.

Quindi R∗ é una bisimulazione tra εa e εb. Essendo sa e sb le soluzioni di εa

ed εb ed essendo esse mappe identiche,

a = saa = sbb = b .

2

Il Teorema di Estensionalità Forte ricopre il ruolo che ha l’Assioma di Esten-sionalità in ZF.

Con questi strumenti é possibile sviluppare una teoria della circolarità chesoddisfi tutti i requisiti descritti nell’introduzione.

15

2.3 Consistenza di ZFA

Per quanto non parte di ciò che ci accingiamo a sviluppare, vogliamo breve-mente dare un’idea della prova di consistenza di ZFA [Acz88,BM96].

Supponiamo che U sia un universo modello per ZF. Sia ε = 〈X,C; e〉 unsistema semplice di equazioni e sia x ∈ X; sia Xx il più piccolo insieme conte-nente x tale che, per ogni y ∈ X, by ⊆ Xx. Sia εx il sistema 〈Xx, C; e

x〉 doveex é la restrizione di e ad Xx.

Il lemma basilare che serve (senza dimostrazione) é:

Lemma 12 Sia ε un sistema di equazioni, x un incognita ed s la soluzione diε. Sia s′ la soluzione di εx, allora s

′ é la restrizione di s ad Xx.

Per costruire un modello per ZFA, usiamo coppie 〈ε, x〉 dove ε é una opportunacodifica del sistema ε ed x é la codifica dell’incognita x di ε.

Definiamo 〈ε, x〉 ≡ 〈ε′, x′〉 se e solo se esiste una bisimulazione R tra εx edε′x′, tale che x R x

′. Costruendo il quoziente di U rispetto a ≡, otteniamo ilmodello desiderato, con l’appartenenza definita come: 〈ε, x〉 ∈ 〈δ, y〉 se e solose esiste z ∈ Bδy tale che 〈ε, x〉 ≡ 〈δ, z〉.

Utilizzando tecniche standard é possibile provare che ogni assioma di ZFA évero in questo modello.

Analizzando l’impianto della prova di consistenza ci rendiamo conto che essaassume la consistenza di ZF. Infatti abbiamo assunto di avere un universo Uche fosse modello per ZF, e, mediante una opportuna costruzione, abbiamoimmerso in U un modello per ZFA.

Quindi, la prova della consistenza di ZFA, é, in effetti, una prova di indipen-denza dell’Assioma di Antifondazione.

2.4 Punti Fissi

Uno dei modi più tipici [Smu94] di dare una definizione circolare ha la struttura

X é il più piccolo oggetto tale che X = Γ(X)

per qualche operazione Γ.

Il concetto soggiacente é:

16

Definizione 13 Un punto fisso per la trasformazione Γ: U −→ U é unasoluzione dell’equazione X = Γ(X).

Per poter usare i punti fissi come strumenti definitori, é necessario garantirnel’esistenza ed un modo per selezionarne uno, quello, d’interesse.

La condizione sufficente per garantire l’esistenza di punti fissi é legata alconcetto di monotonicità.

Definizione 14 Un operatore é una qualsiasi funzione che trasforma elemen-ti dell’universo di un modello di ZFA in elementi dello stesso universo.

Definizione 15 Un operatore Γ é detto monotono se, per ogni a, b tali chea ⊆ b, allora Γ(a) ⊆ Γ(b).

Alcuni esempi di operatori monotoni sono:

Γ1(a) = P(a) dove P(a) é l’insieme potenza di a.

Γ2(a) = Pfin(a)

Γ3(a) = A× a per un insieme fissato A.

Γ4(a) = {f | f é una funzione parziale da a in a}

Γ5(a) = P(A× a) per un insieme fissato A.

Proposizione 16 La composizione di operatori monotoni é monotona.

Per nostra comodità definiamo le proprietà interessanti di un operatore mo-notono rispetto ai punti fissi.

Definizione 17 Sia Γ un operatore monotono

• un insieme G é detto Γ-corretto se G ⊆ Γ(G);• un insieme G é detto Γ-chiuso se Γ(G) ⊆ G;• un insieme G é un punto fisso per Γ se é sia Γ-chiuso che Γ-corretto;• un insieme G é il più piccolo punto fisso di Γ se G é un punto fisso per Γ

e, per ogni punto fisso H di Γ, G ⊆ H;• un insieme G é il più grande punto fisso di Γ se G é un punto fisso per Γ

e, per ogni punto fisso H di Γ, H ⊆ G.

Intuitivamente la nozione di minimo punto fisso corrisponde ad una definizioneper induzione.

Come primo passo formalizziamo questa intuizione.

Teorema 18 (Minimo Punto Fisso) Ogni operatore monotono Γ ammetteun minimo punto fisso (denotato con Γ∗). Esso é caratterizzato come

17

• Γ∗ =⋃

α Γα, con α ordinale e Γα =⋃

β

Lemma 21 Sia Γ un operatore monotono, e sia Γ∗ =⋃

{a | a é Γ-corretto}.

(1) Sia a ⊆ Γ∗, allora esiste un insieme b Γ-corretto tale che a ⊆ b.(2) Sia a ⊆ G, con G Γ-corretto, allora esiste b ⊆ G tale che a ⊆ Γ(b).

Dimostrazione.

(1) Per ogni c ∈ a, c ∈ Γ∗, quindi esiste bc tale che c ∈ bc ⊆ Γ(bc), perdefinizione di Γ∗. Sia b =

⋃

c∈a bc, allora a ⊆ b e, per monotonicità b =⋃

c∈a bc ⊆⋃

c∈a Γ(bc) ⊆ Γ(b), quindi b é Γ-corretto.(2) Per ogni c ∈ a, c ∈ G, quindi, essendo G Γ-corretto, esiste bc ⊆ G tale

che c ∈ Γ(bc). Sia b =⋃

c∈a bc, allora a ⊆ Γ(b) per monotonicità di Γ.

2

Teorema 22 (Massimo Punto Fisso) Ogni operatore Γ che sia monotono,ammette un massimo punto fisso, denotato con Γ∗.

Esso é caratterizzato in uno dei seguenti modi:

• Γ∗ =⋃

{a | a é Γ-corretto} ;• Γ∗ é la massima classe Γ-corretta.

Dimostrazione. Sia Γ∗ =⋃

{a | a é Γ-corretto} e sia b ∈ Γ∗, allora esiste atale che b ∈ a ⊆ Γ(a) per definizione di Γ∗, e a ⊆ Γ∗.

Quindi Γ(a) ⊆ Γ(Γ∗) per monotonicità di Γ, ma

b ∈ a ⊆ Γ(a) ⊆ Γ(Γ∗)

ovvero b ∈ Γ(Γ∗), in altre parole Γ∗ ⊆ Γ(Γ∗), ossia Γ∗ é Γ-corretto.

Sia G una classe Γ-corretta: G ⊆ Γ(G). Sia b ∈ G. Definiamo a0 = {b}, a1 ⊆ Gtale che a0 ⊆ Γ(a1), e, in generale

an+1 ⊆ G tale che an ⊆ Γ(an+1) .

Questi insiemi esistono in virtù del lemma precedente.

Sia a =⋃

n∈N an; se d ∈ a, allora per un qualche n,

d ∈ an ⊆ Γ(an+1) ⊆ Γ(a) .

Questo significa che a ⊆ Γ(a), quindi a ⊆ Γ∗. Ma b ∈ a0 ⊆ a, quindi b ∈ Γ∗,

da cui segue che G ⊆ Γ∗, quindi Γ∗ é la massima classe Γ-corretta.

19

Ma per Γ-correttezza, Γ∗ ⊆ Γ(Γ∗); per monotonicità di Γ, Γ(Γ∗) ⊆ Γ(Γ(Γ∗)),quindi Γ(Γ∗) é una classe Γ-corretta, e per massimalità di Γ∗, Γ(Γ∗) ⊆ Γ∗,ovvero Γ∗ é Γ-chiusa, per cui Γ∗ é un punto fisso e, per di più, il massimo. 2

Come in precedenza, il teorema fornisce due metodi per definire nuovi oggettie per analizzarne le proprietà.

Metodo 23 Per provare che G ⊆ Γ∗, mostrare che G ⊆ Γ(G).

Metodo 24 (Coinduzione) Per provare che G ⊆ Γ∗, mostrare che G ⊆Γ(G ∪ Γ∗).

Per dare un’idea di come questi metodi trovano applicazione, consideriamo uncaso semplice: i numeri naturali.

Consideriamo l’operatore

Γ(a) = {∅} ∪ {b ∪ {b} | b ∈ a é un insieme} .

É immediato verificare che Γ é monotono.

In ZFA, dove abbiamo sviluppato la nostra teoria, consideriamo sia Γ∗ cheΓ∗.

• Γ∗ =⋃

α

⋃

β

In forma di regola:

∅ ∈ G

[b ∈ G]····

b ∪ {b} ∈ G

ω ⊆ G

che é la classica regola di induzione per i naturali nella scrittura propriadella teoria degli insiemi.• Coinduzione:

Per provare che G ⊆ ω ∪ Ω, mostrare che G ⊆ Γ(G), ovvero G ⊆ ω ∪ Ωse G ⊆ {∅} ∪ {b ∪ {b} | b ∈ G}.

La regola di induzione consente di provare proprietà che valgono per ω. SiaG = {x | ψ(x)} dove ψ é una proprietà d’interesse; la regola d’induzionestabilisce che, se vale ψ(0) e, se, supponendo che valga ψ(x), vale ψ(x + 1),allora ψ vale per ogni x ∈ ω.

La regola di coinduzione permette di costruire oggetti che ereditino proprietàda ω∪Ω. Se G é un insieme contenente 0 e chiuso rispetto al successore, alloraG ⊆ ω ∪Ω, quindi se ψ vale per ogni x ∈ ω ∪Ω, allora ψ vale per ogni x ∈ G.

2.5 Bisimulazione

Come abbiamo visto nell’introduzione, uno dei concetti chiave per avere unateoria della circolarità soddisfacente, é quello di bisimulazione.

Tuttavia il concetto di bisimulazione introdotto a proposito dell’Algebra deiProcessi sembra essere molto più generale e flessibile degli analoghi visti nel-l’impianto di ZFA.

Tutti i concetti di bisimulazione visti hanno due punti in comune:

• la struttura formale;• il fatto che sono introdotti per definire un concetto di uguaglianza.

Lo scopo di questa sezione consiste nel mostrare una formulazione alternati-va [BM96,BM91], in apparenza più generale, ma equivalente, dell’Assioma diAntifondazione , sfruttando appieno le bisimulazioni tra insiemi.

Con questo strumento saremo in grado di definire su un modello di ZFA,ogni forma di bisimulazione, mostrando come il concetto di bisimulazione trainsiemi sia, in effetti, il più generale possibile.

21

Definizione 25 Un sistema (generale) di equazioni é una tripla ε = 〈X,A; e〉in cui X é un Insieme di incognite, A é un Insieme di atomi ed e : X −→VA[X].

Per definire cosa é la soluzione di un tale sistema, occorre definire il concettodi sostituzione.

Definizione 26 Una sostituzione é una funzione s il cui dominio sia unInsieme di incognite. Una operazione di sostituzione é una operazione subil cui dominio sia una classe di coppie 〈s, b〉 dove s é una sostituzione eb ∈ U ∪ V [U ] 5 tale che soddisfi le seguenti condizioni:

• se x ∈ dom(s), allora sub(s, x) = sx• se x ∈ U \ dom(s), allora sub(s, x) = x• per ogni insieme b, sub(s, b) = {sub(s, p) | p ∈ b}.

Teorema 27 (Esistenza ed Unicità di sub) Esiste una unica operazionesub che sia una operazione di sostituzione e che sia definita per ogni coppia〈s, b〉 in cui s sia una sostituzione e b ∈ U ∪ V [U ].

Dimostrazione.

(1) EsistenzaDefiniamo sub(s, b) = c se s é una funzione con dominio un Insieme di

incognite per cui valga una delle seguenti condizioni:• b ∈ dom(s) e c = sb;• b ∈ U \ dom(s) e c = b;• b ∈ V [U ] e, detti

X = ({b} ∪ range(s))+ \ A ,

A = ({b} ∪ range(s))+ ∩ A ,

ε′ = 〈X,A; e′〉

con

e′z = {sx | x ∈ z ∩ dom(s)} ∪ {x | x ∈ z ∩ (A \ dom(s))} ∪ (z ∩X) ,

e c = solb dove sol é la soluzione di ε′.

5 Indichiamo con U la classe unione di tutte le incognite e di tutti gli atomi e conA la classe di tutti gli atomi.

22

Per definizione, sub soddisfa le prime due condizioni per essere una sos-tituzione. Per quanto riguarda la terza, sia b un insieme, e siano εb e solbi corrispondenti insieme di equazioni e soluzione come dalla definizionedi sub.

Notiamo che, se b′ ∈ b\A, εb′ é un sottosistema di εb per cui solb′(b′) =

solb(b′) ∈ solb(b).

Quindi sub(s, b) = solb(b) = {sx | x ∈ b ∩ dom(s)} ∪ {x | x ∈ b ∩ (A \dom(s))} ∪ {sub(s, b′) | b′ ∈ b \ A}.

Se x ∈ b∩dom(s), sub(s, x) = sx, e, se x ∈ b∩(A\dom(s)) ⊆ U\dom(s),allora sub(s, x) = x.

Quindi sub(s, b) = {sub(s, p) | p ∈ b}. Ovvero sub é una operazione disostituzione.

(2) UnicitàSia sub′ una operazione di sostituzione definita per ogni coppia 〈s, b〉.Fissando s, si definisce

R = {〈sub(s, b), sub′(s, b)〉 | b ∈ U ∪ V [U ]} .

La relazione R é una bisimulazione tra insiemi:• sia z ∈ U ∩sub(s, b), ma, essendo b un insieme, z é della forma sub(s, x)

per un qualche x ∈ U ∩ b; e z = sub(s, x) = sx = sub′(s, x) ∈ sub′(s, b).

In modo simmetrico si verifica l’altra proprietà per gli atomi.• sia c ∈ sub(s, b) un insieme; se b ∈ A allora c ∈ sb = sub

′(s, b).Se b é un insieme, allora c = sub(s, p) per un qualche p ∈ b, e〈sub(s, p), sub′(s, p)〉 ∈ R.Quindi, per ogni insieme b, sub(s, b) = sub′(s, b), e, per il Teorema di

Estensionalità Forte, sub = sub′.

2

Per comodità di notazione scriviamo b[s] invece di sub(s, b).

La nozione di sostituzione consente di definire cosa sia la soluzione di unsistema generale di equazioni.

Definizione 28 Sia ε = 〈X,A; e〉 un sistema generale di equazioni; unasoluzione di ε é una funzione s con dominio X tale che, per ogni x ∈ X.sx = ex[s].

Il risultato principale riguardante i sistemi generali di equazioni é noto in let-teratura come General Solution Lemma [BM96,BM91]. La sua dimostrazioneé una conseguenza del lemma seguente.

Lemma 29 Sia ε = 〈X,A; e〉 un sistema generale di equazioni; esiste unsistema semplice di equazioni εb = 〈Y,A; e′〉 con X ⊆ Y tale che:

23

• se s é una soluzione di ε allora s si estende alla soluzione s′ per εb.• se s′ é la soluzione di εb ed s = s′ � X (la restrizione di s′ ad X) allora s é

soluzione di ε.

Dimostrazione. Sia

Y = (X ∪⋃

x∈X

(ex)+)) \ A .

Se x ∈ X, definiamo e′x = ex, notando che e′x ⊆ Y ∪ A.

Se x ∈ Y \X, definiamo e′x = x, notando che e′x ⊆ Y ∪ A.

In questo modo abbiamo determinato εb.

(1) s soluzione di ε ⇒ s si estende ad s′, soluzione di εb.Definiamo s′ come s′y = y[s]. Evidentemente s

′ estende s poichè, perogni x ∈ X, s′x = x[s] = sx.

Occorre provare che s′ é soluzione di εb.Poichè a ∩X = ∅, per ogni a ∈ A, a[s] = a = a[s′].La definizione di sostituzione e la transitività 6 di Y implicano che, per

ogni y ∈ Y \X,

s′y = y[s] = {z[s] | z ∈ y} ∪ {y ∩ A} = {s′z | z ∈ y} ∪ {y ∩ A} = e

′y[s

′] .

Per x ∈ X, s′x = sx = ex[s], quindi

s′x = {z[s] | z ∈ ex} =

= {z[s] | z ∈ ex ∩ (Y \X)} ∪ {sz | z ∈ ex ∩X} ∪ (ex ∩ A) =

= {s′z | z ∈ ex ∩ (Y \X} ∪ {s′z | z ∈ ex ∩X} ∪ (e

′x ∩ A) = e

′x[s

′] .

Da cui segue, per definizione, che s′ é (l’unica) soluzione di εb.(2) s′ soluzione di εb ed s = s′ � X ⇒ s soluzione di ε.

Vogliamo innanzitutto provare che, per ogni y ∈ Y , s′y = y[s].Sia R = {〈s′y, y[s]〉 | y ∈ Y }; questa relazione é una bisimulazione tra

insiemi.Supponiamo che 〈s′y, y[s]〉 ∈ R. Sia z ∈ U ∩ s

′y, per definizione di

soluzione di un sistema semplice di equazioni, z ∈ ey ∩ A = y ∩ A. MaX ∩ A = ∅, implica che z = z[s] ∈ y[s].

Nell’altro verso, supponiamo che z ∈ y[s]∩ U . Poichè s prende insiemicome valori, p[s] ∈ U é possibile solamente quando p 6∈ dom(s). Ma, datoche z = z[s], z 6∈ dom(s), quindi z ∈ A, ovvero z ∈ s′y.

6 Un insieme A si dice transitivo se x ∈ y ∈ A implica x ∈ A.

24

Supponiamo che c ∈ s′y e che c sia un insieme. Questo implica chec = s′v per un qualche v ∈ Y . Ma 〈c, v[s]〉 ∈ R quindi ancora una voltariusciamo a soddisfare le condizioni sulla bisimulazione tra insiemi.

Infine supponiamo che c ∈ y[s] e che c sia un insieme. Per le condizioninella definizione di sostituzione, c = v[s] con v ∈ y. Essendo v un insieme,ed essendo Y transitivo, v ∈ Y , quindi 〈s′v, v[s]〉 ∈ R.

Ovvero R é una bisimulazione tra insiemi, e per estensionalità forte,s′y = y[s] per ogni y ∈ Y .

Questo fatto ci consente di provare che s é soluzione di ε: poichè sx =s′x = e

′x[s

′] = ex[s′], per ogni x ∈ X,

sx = {s′z | z ∈ ex \ A} ∪ (ex ∩ A) =

= {s′z | z ∈ ex ∩ (Y \X)} ∪ {s′z | z ∈ ex ∩X} ∪ (ex ∩ A) =

= {z[s] | z ∈ ex ∩ (Y \X)} ∪ {z[s] | z ∈ ex ∩ (X ∪ A)} =

= ex[s] .

2

Teorema 30 (General Solution Lemma) Ogni sistema generale di equa-zioni ε ammette un’unica soluzione s. Inoltre l’insieme soluzione di ε é unsottoinsieme di V [A], dove A é l’insieme degli atomi di ε.

Dimostrazione. Conseguenza immediata del lemma precedente e del FlatSolution Lemma. 2

Il risultato che avevamo preannunciato all’inizio di questa sezione, é il seguen-te:

Teorema 31 AFA (l’Assioma di Antifondazione) é equivalente all’asserzio-ne che ogni sistema generale di equazioni ammette un’unica soluzione.

Dimostrazione. Conseguenza immediata del General Solution Lemma e del-la prova del lemma 29. 2

Come ultimo risultato della nostra analisi teorica di ZFA, presentiamo unaproposizione che utilizzeremo per mostrare come si possa risolvere il paradossodell’ipergioco, ma che riveste un significato autonomo.

Definizione 32 Un insieme a é detto riflessivo se a ∈ a.

25

Proposizione 33 (Difference Lemma) Sia V un insieme transitivo e siab = V \ {v}, allora b 6∈ V .

Dimostrazione. Se V non é riflessivo, allora b = V e, per definizione di nonriflessivo, b 6∈ V .

Supponiamo che V sia riflessivo: se b ∈ V (ipotesi d’assurdo), allora b ∈V \ {V } = b poichè V 6∈ b, e quindi V 6= b.

Quindi anche b é riflessivo.

Sia R = {〈V, b〉} ∪ {〈a, a〉 | a ∈ b}. Proviamo che R é una bisimulazione trainsiemi:

• per ogni a ∈ V esiste c ∈ b tale che 〈a, c〉 ∈ R; se a = V allora c = b,altrimenti c = a.• per ogni a ∈ b esiste c ∈ V tale che 〈a, c〉 ∈ R; poichè V é transitivo, c = a.• per definizione di b, b e V hanno lo stesso insieme di atomi.

Per il Teorema di Estensionalità Forte, b = V .

Ma V ∈ V per ipotesi e V 6∈ b per ipotesi d’assurdo, quindi b 6= V . Abbiamopertanto una contraddizione, quindi b 6∈ V . 2

26

3 Applicazioni

Nell’introduzione di questo lavoro, abbiamo presentato alcuni esempi ed alcuniparadossi inerenti il concetto di circolarità.

Avendo sviluppato l’apparato teorico, é tempo di presentare una formaliz-zazione degli esempi, mostrando come la teoria ZFA sia sufficentemente po-tente per modellarli tutti, ed in modo naturale.

Inoltre intendiamo mostrare il modo in cui ZFA renda i paradossi, ovvero comeessi siano costruzioni impossibili, o con un significato diverso, talora più in-teressante, della semplice inconsistenza che, in apparenza, essi presuppongononell’idea di circolarità.

Infine mostreremo una costruzione particolarmente notevole in quanto presen-ta applicazioni in logica, che illustra come alcune nozioni che coincidono inZF diano luogo a strutture molto differenti in ZFA: parleremo degli insiemiereditariamente finiti.

3.1 Esempi Introduttivi

3.1.1 Sequenze

Nell’introduzione abbiamo presentato, intuitivamente, il concetto di lista edi sequenza, evidenziando come una teoria della circolarità accettabile debbaessere in grado di rappresentare appropriatamente entrambe le strutture dati.

In ZFA, ciò é possibile, e gli strumenti sviluppati nella parte teorica con-sentono di dare un modello naturale per queste strutture dati.

Sia A un insieme; vogliamo costruire due nuovi insiemi L ed S, che rappre-sentino le liste e le sequenze sull’alfabeto A.

A tal fine, definiamo l’operatore Γ(c) = A×c; esso é evidentemente, monotono.

Notando che Γ(∅) = ∅, il minimo punto fisso per Γ é l’insieme vuoto. TuttaviaΓ∗ (il massimo punto fisso per Γ) é non banale:

Γ∗ =⋃

{a | a ⊆ Γ(a)} =⋃

{a ⊆ A× a} .

Consideriamo la mappa ψ : Sequenze −→ Γ∗:

ψ(Nil) = ∅ e ψ(Cons α x) = 〈α, ψ(x)〉 .

27

Essa é totale e biiettiva, infatti

• se σ é una sequenza allora σ = Nil oppure σ = Cons α τ con α ∈ A e τsequenza, quindi ψ é totale.• se σ = τ allora σ = τ = Nil e ψ(σ) = ψ(τ), oppure σ = Cons α σ ′

e τ = Cons α τ ′; per ipotesi ψ(σ′) = ψ(τ ′), quindi anche ψ(σ) = ψ(τ).Ovvero ψ é iniettiva.• se 〈α, β〉 ∈ Γ∗ allora, per ipotesi, esiste σ tale che ψ(σ) = β e quindiψ(Cons α σ) = 〈α, β〉; inoltre ∅ ∈ Γ∗ e ψ(Nil) = ∅, provando la suriettivitàdi ψ.

Quindi Γ∗ é un modello in ZFA per le sequenze.

Consideriamo l’equazione ψ(x) = ψ(Cons α x): essa ammette soluzione, in-fatti x = 〈α, x〉 é un sistema generale di equazioni e pertanto ammette una eduna sola soluzione; la sequenza costituita da elementi α.

Banalmente otteniamo un Principio di Coinduzione ed uno di Coricorsione:

Principio 34 (Coinduzione) Z ⊆ Γ∗ se Z ⊆ A× Z.

Principio 35 (Coricorsione) Sia C un insieme e siano G : C −→ A edH : C −→ C due funzioni, allora esiste una unica funzione F : C −→ Γ∗ taleche, per ogni c ∈ C,

F (c) = 〈G(c), F (H(c))〉 .

Dimostrazione. Sia X un insieme di incognite in corrispondenza biunivocacon C. Sia ε = 〈X,A; e〉 un sistema generale di equazioni con

exc = 〈G(c), xH(c)〉 .

Questo sistema ammette una unica soluzione s. Definiamo F (c) = sxc. Ma

sxc = 〈G(c), xH(c)〉[s] = 〈G(c), F (H(c))〉 ,

ovvero F (c) = 〈G(c), F (H(c))〉. 2

In questo modo abbiamo uno strumento per definire funzioni su sequenze: adesempio, map(f, s) = 〈f(head(s)),map(f, tail(s))〉 risulta ben definita per ilPrincipio di Coricorsione.

Come risultato, possiamo dire che la nostra teoria permette di codificare ilconcetto di sequenza in modo naturale.

28

Consideriamo l’operatore Γ′ tale che Γ′(c) = (A× (c ∪ {∅})) ∪ {∅}.

É immediato verificare che il minimo punto fisso di Γ′ esiste (per monotonicità)ed é non banale, cos̀i come il massimo punto fisso.

Definendo ψ : Liste −→ Γ′∗ come

ψ(Nil) = ∅ e ψ(Cons α x) = 〈α, ψ(x)〉

e ripetendo il ragionamento fatto in precedenza riguardo l’interpretazione perle sequenze, otteniamo una caratterizzazione per le liste sull’alfabeto A. Inmodo analogo a quanto visto per le sequenze, possiamo introdurre un Principiodi Induzione ed un Principio di Ricorsione.

Più interessante é analizzare Γ′∗: infatti esso coincide con Γ∗, se A 6= ∅.

Proposizione 36 Γ′∗ = Γ∗.

Dimostrazione.

(1) Γ∗ ⊆ Γ′∗ infatti, usando il Principio di Coinduzione per Γ′, abbiamo che

Γ∗ ⊆ Γ′(Γ∗) = (A× (Γ∗ ∪ {∅})) ∪ {∅}

= (A× Γ∗) ∪ {∅}

= Γ∗ ∪ {∅}

= Γ∗

poichè ∅ ∈ Γ∗.(2) Γ

′∗ ⊆ Γ∗, infatti Γ′∗ é Γ-corretto. Per provare questo mostriamo che

Γ′∗ = A× Γ

′∗.Sia

R = {〈α, 〈β, α〉〉 | β ∈ A, α ∈ Γ′∗} .

Questa é una bisimulazione tra Γ′∗ e A× Γ

′∗:• ∀α ∈ Γ

′∗. ∃β ∈ A× Γ′∗. α R β, basta prendere β = 〈a, α〉 con a ∈ A.

• ∀α ∈ A × Γ′∗. ∃β ∈ Γ

′∗. β R α, basta prendere β = γ, dove α = 〈a, γ〉con a ∈ A.• Gli atomi in Γ

′∗ sono in A cos̀i come in A× Γ′∗.

Sapendo che A×Γ′∗ = Γ

′∗, per il Principio di Coinduzione su Γ, notandoche Γ

′∗ ⊆ A× Γ′∗ = Γ(Γ

′∗), deduciamo che Γ′∗ ⊆ Γ∗.

2

29

Quindi esiste modo di caratterizzare le liste e le sequenze come minimo emassimo punto fisso del medesimo operatore, che attraverso le opportune in-terpretazioni, codifica esattamente la usuale dichiarazione di queste strutturedati.

In modo analogo possono essere modellate tutte le strutture dati definite perinduzione, generando parallelamente le costrutture come massimi punti fissidella medesima trasformazione.

3.1.2 Chiusure

Nell’introduzione abbiamo visto come il concetto algebrico di chiusura sia inrelazione con la circolarità. Come esempio abbiamo usato la chiusura riflessivae transitiva di una relazione.

Tale esempio é formalizzabile in maniera semplice all’interno della nostrateoria. Sia R una relazione, consideriamo l’operatore Γ definito come:

Γ(c) = {〈a, a〉 | ∃b. 〈a, b〉 ∈ c ∨ 〈b, a〉 ∈ c} ∪

{〈a, b〉 | ∃d. 〈a, d〉 ∈ c ∧ 〈d, b〉 ∈ R} ∪R .

É immediato verificare la monotonia di Γ.

Consideriamo Γ∗, il minimo punto fisso di Γ:

• Γ∗ é una relazione poichè ogni suo elemento é una coppia; inoltre R ⊆ Γ∗poichè Γ(∅) ⊆ Γ∗, per la caratterizzazione di quest’ultimo e Γ(∅) = R.• Γ∗ é una relazione riflessiva poichè Γ(Γ∗) = Γ∗ e, in particolare questo

significa che

∀a. (∃b. 〈a, b〉 ∈ Γ∗ ∨ 〈b, a〉 ∈ Γ∗)→ 〈a, a〉 ∈ Γ∗ ,

per definizione di Γ.• per gli stessi motivi, Γ∗ é una relazione transitiva.• Sia Q una relazione riflessiva, transitiva, che contenga R: Γ(Q) = Q∪Q′∪R,

con Q′ ⊆ R, per definizione di Γ, ovvero Γ(Q) = Q; ma Γ∗ é il minimoinsieme che sia un punto fisso per Γ, quindi Γ∗ ⊆ Q.

Tutto ciò comporta che Γ∗ é la chiusura riflessiva e transitiva di R.

Notiamo come il fenomeno dell’impredicatività venga a coincidere, nella strut-tura della nostra teoria, con il concetto di insieme non ben fondato, e che,mediante una trattazione appropriata di questi insiemi, sia possibile utilizzare

30

e circoscrivere opportunamente il fenomeno in virtù dei risultati che abbiamosviluppato.

Un’altra richiesta che abbiamo introdotto quando abbiamo parlato di chiusure,é stato il concetto di costruzione duale. Vediamo come tale costruzione sia ilnaturale sviluppo della nostra teoria applicata all’esempio della cochiusurariflessivo-transitiva; sia ∆ l’operatore definito come:

∆(c) = {〈a, a〉 | 〈a, a〉 ∈ R} ∪

{〈a, b〉 | 〈a, b〉 ∈ R ∧ ∃d ∈ c. 〈a, d〉 ∈ c ∧ 〈d, b〉 ∈ c} .

Anche in questo caso, la monotonia di ∆ é evidente.

Consideriamo ∆∗, il massimo punto fisso di ∆:

• poichè ∀c. ∆(c) ⊆ R, ∆∗ ⊆ R.• per definizione di ∆, ed essendo ∆∗ = ∆(∆∗), ∆∗ é una relazione riflessiva

e transitiva.• per massimalità di ∆∗, ogni altra relazione riflessiva e transitiva che sia

contenuta in R, é contenuta in ∆∗.

Quindi ∆∗ é, secondo la nostra definizione, la cochiusura riflessivo-transitivadi R.

L’operazione di cochiusura può essere efficacemente usata per definire nuovioggetti. Sia R una relazione, Γ un operatore monotono, Γ∗ la cochiusura diR rispetto a Γ, e Q un sottoinsieme di Γ∗. Un modo naturale per definire unnuovo oggetto, é considerare il minimo insieme Q∗ che contenga Q e che siaΓ-corretto.

La naturalità di questa operazione deriva da alcune costruzioni similari chevengono usate in Topologia [Csá78], specialmente quando si parla di compat-tificazione.

Per garantire l’esistenza e l’unicità di tale Q∗ é necessario richiedere qualchecondizione aggiuntiva sull’operatore Γ.

Il seguente sviluppo teorico consente di identificare una condizione sufficente,di vasta applicabilità, per garantire una buona definizione di un tale Q∗.

Definizione 37 Un operatore monotono Γ commuta con intersezioni binariese, per ogni insieme a e b, Γ(a ∩ b) ⊆ Γ(a) ∩ Γ(b).

Un operatore monotono Γ commuta con tutte le intersezioni se, per ogni b,Γ(

⋂

b) =⋂

c∈b Γ(c).

31

Proposizione 38 Esistono operatori monotoni che non commutano con in-tersezioni binarie.

Dimostrazione. Sia Γ definito come

Γ(b) =

∅ se b ⊆ {∅}

b altrimenti.

Banalmente si verifica che Γ é monotono.

Siano a = {∅, 1} e b = {∅, 2}:

Γ(a ∩ b) = Γ({∅}) = ∅ ,

ma

Γ(a) ∩ Γ(b) = {∅, 1} ∩ {∅, 2} = {∅} .

2

Corollario 39 Esistono operatori monotoni che non commutano con tutte leintersezioni.

Notiamo, per inciso, che tutti gli operatori presentati come esempio di mono-tonia quando si é introdotto il concetto di punto fisso, commutano con tuttele intersezioni.

Proposizione 40 Se Γ commuta con tutte le intersezioni allora l’intersezionedi una famiglia di insiemi Γ-corretti, é Γ-corretta.

Dimostrazione. Sia c una famiglia di insiemi Γ-corretti:

⋂

b∈c

b ⊆⋂

b∈c

Γ(b) = Γ(⋂

b∈c

b) .

2

Lemma 41 Se Γ commuta con tutte le intersezioni e a ⊆ Γ∗, allora esiste uninsieme b minimalmente Γ-corretto tale che a ⊆ b.

Dimostrazione. Sia a ⊆ Γ∗, allora, dal Teorema di Massimo Punto Fisso,sappiamo che esiste un insieme b Γ-corretto tale che a ⊆ b.

Sia c =⋂

{b′ ⊆ b | b′ é Γ-corretto e a ⊆ b′}.

32

Ovviamente, a ⊆ c; per la proposizione precedente, c é Γ-corretto. Sia d uninsieme Γ-corretto con a ⊆ d. Ma questo significa che d∩ c é Γ-corretto, e, perdefinizione di c, c ⊆ d ∩ c, ovvero c ⊆ d. 2

Definizione 42 Sia Γ un operatore che commuti con tutte le intersezioni, esia a ⊆ Γ∗; un insieme b é la Γ-chiusura di a se b é Γ-corretto, a ⊆ b ed é ilminimo insieme con queste proprietà.

In virtù del lemma precedente, la definizione di Γ-chiusura é ben data, ovveroidentifica sempre ed in modo univoco un oggetto.

In sintesi, una condizione sufficente per garantire l’esistenza della Γ-chiusuradi un insieme a, é data dal fatto che Γ commuti con tutte le intersezioni.Inoltre tale condizione é vera per molti degli operatori monotoni che ricorrononella pratica.

3.1.3 Auto-Applicazione

Nell’introduzione abbiamo visto come il concetto di auto-applicazione, che,naturalmente, ricade sotto il dominio di una teoria della circolarità, sia model-labile attraverso il λ-Calcolo [Bar84], e la Logica Combinatoria [HS86,CF58].

Per semplificare l’esposizione, ci concentreremo sulla Logica Combinatoria (insigla CL), mostrando come i concetti di convergenza e divergenza di cui ac-cennato nell’introduzione, ed i cui corrispettivi formali sono in relazione alleforme normali per un termine, abbiano una naturale caratterizzazione in ZFA.

In questa sezione mostreremo come sia possibile immergere la Logica Com-binatoria in ZFA, seguendo l’idea intuitiva che un termine denota un valoredato dalla sua forma normale.

Mostreremo che tale immersione fornisce una rappresentazione elementare peril concetto di uguaglianza in CL, per la nozione di forma normale, di terminefortemente normalizzabile e di termine insolubile.

Osservando la rappresentazione fornita, avremo un modello per CL che mostracome codificare in generale i requisiti di cui abbiamo fatto richiesta nella parteintroduttiva di questo lavoro.

L’idea intuitiva che intendiamo perseguire per rappresentare un termine di CLcome un insieme in ZFA é la seguente: un termine che sia in forma normaledenota un valore, mentre un termine che non sia in forma normale, denotal’insieme dei termini a cui può essere ridotto. Formalmente:

33

Definizione 43 Sia t un termine, la rappresentazione di t in ZFA é

rep(t) =

{at} se t é una forma normale

{rep(s) | t+−→ s altrimenti

dove at é un atomo e t 6≡ s implica at 6= as e la relazione+−→ é la chiusura

transitiva di −→, la riduzione in un passo di termini:

S x y z −→ x z (y z) K x y −→ x

x −→ y

x z −→ y z

x −→ y

z x −→ z y

É immediato verificare che, in ZFA, per ogni termine t, rep(t) é un insieme(non necessariamente ben fondato) ed é univocamente determinato.

Per mostrare che l’immagine di rep é un modello per CL, é necessario provare

l’esistenza di una rappresentazione che perCL=.

Proposizione 44 Siano t ed s due termini:

tCL= s

se e solo se

rep(t) ∩ rep(s) 6= ∅ ∨ rep(t) ∈ rep(s) ∨ rep(s) ∈ rep(t) .

Dimostrazione.

• Per il Teorema di Church-Rosser, se tCL= s, allora esiste u tale che t

∗−→ u

e s∗−→ u.

Se t ≡ u e s ≡ u allora t ≡ s e rep(t)∩rep(s) = rep(t), ma, per definizione,per ogni t, rep(t) 6= ∅.

Se t ≡ u e s 6≡ u allora s+−→ t ed s non é una forma normale, quindi

rep(t) ∈ rep(s).

Se t 6≡ u e s ≡ u allora t+−→ s e t non é una forma normale, quindi

rep(s) ∈ rep(t).

Se t 6≡ u e s 6≡ u allora t+−→ u, s

+−→ u e t ed s non sono forme normali,

quindi rep(u) ∈ rep(t) e rep(u) ∈ rep(s), ovvero rep(u) ∈ rep(t) ∩ rep(s).• Se vale rep(t) ∈ rep(s) allora, per definizione di rep, s non é una forma

normale, avendo un insieme come elemento, quindi s+−→ t , ovvero s

CL= t.

Analogamente, se rep(s) ∈ rep(t), si vede che tCL= s.

34

Sia perciò rep(t) ∩ rep(s) 6= ∅ e rep(t) 6∈ rep(s) e rep(s) 6∈ rep(t); poichèrep(t) ∩ rep(s) 6= ∅, esiste x ∈ rep(t) e x ∈ rep(s).

Se x é un insieme allora nè t, nè s sono forme normali, per cui x ≡ rep(u)

per un certo u e t+−→ u e s

+−→ u, quindi, per definizione segue che t

CL= s.

Se x non è un insieme allora é un atomo, e, per definizione di rep, é dellaforma au per un certo termine u in forma normale.

Ma questo vuol dire che t ed s devono necessariamente essere in formanormale, poichè un atomo é elemento di rep(x) se e solo se rep(x) = {ax}.In altre parole au ∈ {at} e au ∈ {as}, ovvero at = as. Quindi t ≡ s, cioé

tCL= s.

2

La proposizione appena provata mostra cheCL= é rappresentata fedelmente

dalla relazione

{〈x, y〉 | {x, y} ⊆ range(rep) ∧ (x ∩ y 6= ∅ ∨ x ∈ y ∨ y ∈ x)} .

La rappresentazione prescelta cattura in maniera naturale i concetti di terminefortemente normalizzabile, di termine normalizzabile e di termine insolubile.

Lemma 45 Il termine t é fortemente normalizzabile se e solo se rep(t) é benfondato.

Dimostrazione.

• Se t é fortemente normalizzabile allora ogni possibile riduzione di t é finita.

Formalmente, non esiste s tale che t∗−→ s ed s

+−→ s.

Quindi, per definizione di insieme ben fondato, rep(t) é ben fondato.

• Se t non é fortemente normalizzabile, esiste s tale che t∗−→ s ed s

+−→ s.

Quindi rep(s) non é ben fondato, essendo un insieme riflessivo. Ma rep(s) ∈rep(t) per definizione, quindi rep(t) non é ben fondato.

2

Definizione 46 Sia t un termine, indichiamo con Base(t) l’insieme degliatomi presenti in rep(t) ad un qualsiasi livello di innestamento.

Lemma 47 Il termine t non ammette forma normale se e solo se Base(t) = ∅.

Dimostrazione. Per costruzione Base(t) ⊆ {au | u é una forma normale}.

35

Quindi Base(t) = ∅ implica che t non é una forma normale e {au} 6∈ rep(t) per

ogni u, ovvero t+−→ u, con u forma normale, non vale. Quindi t non ammette

forma normale.

Viceversa se t non ammette forma normale, rep(t) = {rep(s) | t+−→ s} e

nessun s é una forma normale, quindi per nessun s, rep(s) = {as}.

Notando che Base(t) =⋃

rep(s)∈rep(t) Base(s), per ∈-induzione, Base(t) = ∅. 2

Corollario 48 Per ogni termine t, |Base(t)| ≤ 1.

Dimostrazione. Se t non ammette forma normale, Base(t) = ∅ e quindi|Base(t)| = 0.

Se t ammette forma normale s, ma t non é una forma normale, allora rep(s) ={as} ∈ rep(t).

Per assurdo, se |Base(t)| > 1 allora esiste u 6≡ s tale che au ∈ Base(t). Maquesto implica che esiste un v tale che {au} ∈ rep(v) e rep(v) ∈ rep(t); quindi,

per definizione di rep, {au} ∈ rep(t) e t+−→ u. Ma t

+−→ s, quindi per il

Teorema di Church-Rosser e sapendo che s ed u sono forme normali, s ≡ u,assurdo.

Ovviamente, se t é una forma normale |Base(t)| = 1. 2

La conclusione che possiamo trarre dallo sviluppo presentato é che, ancora unavolta, i concetti base di ZFA (insieme ben fondato, insieme riflessivo, . . . )caratterizzano in modo diretto i criteri di convergenza (divergenza) che sorgonoda teorie come la Logica Combinatoria o il λ-Calcolo e che costituiscono unmodo per definire concetti circolari.

É interessante rilevare come la costruzione da noi presentata, seppur moltosintattica, sia simile ad alcuni dei modelli semantici proposti (ad esempio iGraph Models [Plo72,Sco74] o i Böhm Trees [Böh68]) ma manchi delle diffi-coltà in esse intrinseche per via di un ambiente di definizione (la teoria degliinsiemi ZF) che non permtte di trattare direttamente nozioni circolari.

3.1.4 Concorrenza

Al fine di mostrare come si possa codificare la nozione di bisimulazione traprocessi all’interno di ZFA, fornendo di un sistema fondazionale tale concetto,é necessario rappresentare i processi medesimi come insiemi.

36

Informalmente, un processo é identificato con l’insieme dei comportamenti cheé in grado di esibire. Se vogliamo quindi rappresentare i processi CCS, e siamointeressati a cogliere il loro comportamento rispetto ad ogni azione che sonoin grado di compiere, verrà naturale identificare la bisimulazione tra processicon la bisimulazione tra gli insiemi che li rappresentano.

Formalmente un processo CCS é definito per induzione a partire dai costruttoridel linguaggio; in modo analogo noi possiamo costruire un sistema generale diequazioni in cui, ad ogni variabile, verrà associato un unico insieme, in virtùdel General Solution Lemma, che é la rappresentazione del processo medesimo.

A tal punto é sufficente provare che la nozione di bisimulazione tra insiemicoincide con la nozione di bisimulazione tra processi.

Definizione 49 Un processo CCS P é rappresentato dalla soluzione sxP asso-ciata al sistema generale di equazioni εP costruito per induzione sulla strutturadi P , come segue:

• P ≡ nil

εP = 〈{xP}, ∅; e〉

con exP = ∅.• P ≡ α . Q

εP = 〈{xP} ∪XQ, {α} ∪ AQ; e〉

dove εQ = 〈XQ, AQ; eQ〉 é il sistema associato a Q e

e � XQ = eQ, exP = 〈α, xQ〉 .

• P ≡ α . Q

εP = 〈{xP} ∪XQ, {α} ∪ AQ; e〉

dove εQ = 〈XQ, AQ; eQ〉 é il sistema associato a Q e

e � XQ = eQ, exP = 〈α, xQ〉 .

• P ≡∑

∆

εP = 〈{xP} ∪⋃

Q∈∆

XQ,⋃

Q∈∆

AQ; e〉

dove, per ogni Q ∈ ∆, εQ = 〈XQ, AQ; eQ〉 é il sistema associato a Q e

e � XQ = eQ, exP =

⋃

Q∈∆

{xQ} .

37

• P ≡ Q |R

εP = 〈{xP} ∪XQ ×XR, AQ ∪ AR; e〉

dove εQ = 〈XQ, AQ; eQ〉 e εR = 〈XR, AR; e

R〉 sono i sistemi associati a Qed R, rispettivamente ed e é definita come

exP = exQ|R , exα|β = {〈γ, xα′|β′〉 | α | βγ−→ α′ | β ′ ∨ α | β

γ−→ α′ | β ′} .

• P ≡ Q \ Γ

εP = 〈{xP} ∪XQ, AQ \ Γ; e〉

dove εQ = 〈XQ, AQ; eQ〉 é il sistema associato a Q e

e � XQ = eQ ristretta ad AQ \ Γ, exP = xQ .

• P ≡ Q[Φ]

εP = 〈{xP} ∪XQ,Φ(AQ); e〉

dove εQ = 〈XQ, AQ; eQ〉 é il sistema associato a Q, Φ(AQ) = {Φ(α) | α ∈

AQ} e

e � XQ = Φ ◦ eQ, exP = xQ .

• P ≡ rec x. Q

εP = 〈{xP} ∪XQ, AQ; e〉

dove εQ = 〈XQ, AQ; eQ〉 é il sistema associato a Q (in cui comparirà una

variabile, x solo nel lato destro delle equazioni), e

e � (XQ \ {x}) = eQ, exP = x, ex = xP .

Per induzione sulla struttura di un processo P é facile convincersi che

Proposizione 50 Se Pα−→ Q, allora 〈α, xQ〉 ∈ exP in εP = 〈XP , AP ; e〉 il

sistema associato a P .

Analogamente si può verificare che, in base alla definizione del nostro sistemaεP ed alla definizione della relazione di transizione:

Proposizione 51 Se 〈α, xQ〉 ∈ exP nel sistema εP = 〈XP , AP ; e〉 associato aP , allora esiste un processo Q tale che

(1) Pα−→ Q;

(2) Il sistema associato a Q é la restrizione di εP a cui sia stato sottratto lavariabile xP , modulo una bisimulazione tra sistemi.

38

Le due proposizioni appena enunciate (di cui omettiamo la dimostrazione,essendo totalmente standard) garantiscono che la nostra rappresentazione deiprocessi sia completa e fedele rispetto alla relazione di transizione.

Il concetto di bisimulazione tra processi coincide con la bisimulazione trainsiemi.

Teorema 52 Siano P e Q due processi, e siano P ′ e Q′ i corrispondentiinsiemi nella rappresentazione in ZFA; P ≈ Q se e solo se P ′ = Q′.

Dimostrazione.

(1) P ≈ Q implica P ′ = Q′.Per definizione di bisimulazione tra processi, P ≈ Q se e solo se

∀α, P . Pα−→ P → ∃Q. Q

α−→ Q ∧ P ≈ Q

e

∀α,Q. Qα−→ Q→ ∃P . P

α−→ P ∧ P ≈ Q .

Sia R la relazione tra insiemi che siano rappresentazione di processidefinita come: a R b se e solo se

∀α, a′. 〈α, a′〉 ∈ a→ ∃b′. 〈α, b′〉 ∈ b ∧ 〈a′, b′〉 ∈ R

e

∀α, b′. 〈α, b′〉 ∈ b→ ∃a′. 〈α, a′〉 ∈ a ∧ 〈a′, b′〉 ∈ R

Questa é una bisimulazione tra insiemi come si prova immediatamente.Ma, se P ≈ Q, allora P ′ R Q′, infatti

∀α, P . Pα−→ P → ∃Q. Q

α−→ Q ∧ P ≈ Q

equivale, per le proposizioni precedenti, a

∀α, P . 〈α, P 〉 ∈ P ′ → ∃Q. 〈α,Q〉 ∈ Q′ ∧ P ≈ Q

ovvero, secondo l’ipotesi che P ≈ Q → P′R Q

′, questo si riduce a

P ′ R Q′. Quindi P ′ = Q′ essendo R una bisimulazione.(2) É immediato provare che P ≈ Q sapendo che P ′ = Q′: infatti, sfruttando

la bisimulazione R introdotta nel punto precedente, risulta immediatoverificare la tesi.

2

39

In un certo senso la prova é costruttiva, esibendo effettivamente una bisimu-lazione tra insiemi che agisca come ≈ sulle rappresentazioni dei processi.

In generale é possibile cambiare la codifica dei processi per effettuare osser-vazioni differenti su di essi, e la naturale nozione di bisimulazione che vienegenerata da una osservazione risulta coincidente con la bisimulazione tra gliinsiemi rappresentazione dei processi.

Le dimostrazioni dei relativi risultati, ad esempio, riguardo l’uguaglianza os-servazionale, sono del tutto simili a quelle presentate.

3.2 Soluzione ai Paradossi

3.2.1 Russell

Come é noto, la soluzione al paradosso di Russell che viene fornita nella teoriaZF consiste nel bandire tale collezione, mostrando l’impossibilità di costruireun insieme che soddisfi la condizione.

Definiamo Rb = {x ∈ b | x 6∈ x}. É facile mostrare che, in ZF, questo é uninsieme. Il paradosso di Russell afferma che Rb 6∈ b, e questo fatto non inducealcuna inconsistenza nella teoria.

La soluzione fornita da ZFA é identica: poichè il solo modo per costruire uninsieme che soddisfi l’enunciato di Russell implica l’uso dell’Assioma di Com-prensione, e questo stabilisce che l’insieme costruito debba essere sottoinsiemedi un insieme dato, segue che, se esistesse R = {x | x 6∈ x}, R deve esseresottoinsieme dell’insieme di tutti gli insiemi.

In ZF ciò é impossibile poichè non esiste un oggetto identificabile con l’insiemedi tutti gli insiemi, per l’Assioma di Fondazione.

In ZFA l’oggetto identificable come l’insieme di tutti gli insiemi non puòessere costruito 7 , ma se fosse possibile esso sarebbe il massimo punto fissodell’operatore potenza insiemistica.

Per quanto visto nella parte relativa ai punti fissi, tale punto fisso esiste, a pattodi prendere una opportuna base di atomi. Tale base deve formare una classepropria, quindi il massimo punto fisso di P é una classe propria, esattamentecome in ZF.

Tirando le somme, il paradosso di Russell non inficia ZFA, ma é utile per

7 Per via del Teorema di Cantor, che afferma che la cardinalità della potenza di Xé maggiore della cardinalità di X, per ogni insieme X.

40

mostrare che alcuni insiemi non sono costruibili, come, ad esempio, un insiemeRb che appartenga a b.

3.2.2 Mentitore

Il paradosso del mentitore[Mar84] deriva dall’autoriferimento contenuto nellafrase questa frase é falsa. Vediamo di analizzare formalmente la nozione dicircolarità soggiacente.

Una sentenza del mentitore ha la seguente struttura

¬Trueh(this) .

Teorema 53 (Mentitore) Sia α una sentenza del mentitore:

α ≡ ¬Trueh(this) .

SeM é un modello (parziale) per cui sia possbile esprimere α, allora una delleseguenti condizioni é falsa:

(1) this denota α in M.(2) h denota M in M.(3) M |= α ∨ ¬α.

Dimostrazione. Assumiamo le tre condizioni e deriviamone una contrad-dizione: poichèM |= α ∨ ¬α, alloraM |= α oppure M |= ¬α.

Se M |= α allora M |= ¬Trueh(this), ma this denota α ed h denota M, e,per definizione del predicato di verità, M |= ¬α, assurdo.

SeM |= ¬α, alloraM |= Trueh(this) e, analogamente, M |= α, assurdo. 2

Apparentemente quindi, una qualsiasi soluzione del paradosso del mentitoredeve rendere falsa una condizione del teorema.

In realtà, seppur questo é vero, la situazione é più complessa, soprattutto sevista in relazione al concetto circolarità.

L’esempio più interessante riguarda la possibilità di costruire un modello incui si abbia autoriferimento, che sia totale e che permetta di esprimere unasentenza del mentitore.

Per formalizzare l’esempio, faremo uso della teoria dei modelli per la logica atre valori di Kleene [Res69]. Rimandiamo alla letteratura la presentazione ditale teoria [BM96] in quanto esula dagli scopi del nostro lavoro.

41

Sia α ≡ ¬Trueh(this); il modelloM = 〈D,L,E,A, d, c〉 é definito come:

• D = {α,M} l’universo del discorso, il dominio del modello.• L = {m,True} le costanti extralogiche, il linguaggio.• E = {〈True, ∅〉} l’estensione, ovvero i predicati che vengono interpretati

come veri.• A = {〈True, D×D〉} l’antiestensione, ovvero i predicati che hanno valore

logico falso.• d = {〈m,M〉, 〈this, α〉} la denotazione, o l’interpretazione dei simboli per

costante.• c = ∅ l’interpretazione delle varabili.

Poichè h non é denotato in M, ed M é un modello per la logica di Kleene atre valori,M 6|= α eM 6|= ¬α, ovvero α é indefinito su M.

TuttaviaM é totale poichè ogni predicato atomico non é indefinito.

Occorre notare cheM |= ¬Truem(this), ma questo non genera alcun parados-so, poichè this denota α e α 6≡ ¬Truem(this).

Quindi un qualsiasi modello per una logica con indefiniti, che ammetta au-toriferimento può essere bisimulato entro ZFA da un insieme riflessivo.

Inoltre, a seconda della particolare soluzione al paradosso, tali modelli in ZFAsaranno costruibili secondo le linee guida negli esempi citati.

3.2.3 Ipergioco

Come abbiamo già detto nell’introduzione, la natura dell’ipergioco é differentedagli altri paradossi. Nelle sezioni precedenti abbiamo visto come il paradossod Russell non possa occorrere in ZFA, e come il paradosso del mentitore siamodellabile per mostrare che certi insiemi non possano essere costruiti.

Il paradosso dell’ipergioco coinvolge direttamente l’idea di circolarità e quindimerita un’analisi formale dettagliata.

Definizione 54 Sia S un insieme di giochi, il supergioco su S, denotato conS+ é definito informalmente come segue: il giocatore I sceglie un gioco G ∈ S,poi il giocatore II inizia G, ed il resto del gioco é G. Il vincitore di S+ é ilvincitore di G.

É chiaro che, per ogni S, esiste il supergioco S+.

Proposizione 55 Sia S un insieme di giochi

(1) Se S é un insieme ben fondato allora S+ é ben fondato.

42

(2) Se S é un insieme ben fondato allora S+ 6∈ S.

Dimostrazione.

(1) Un gioco viene modellato come l’insieme delle sequenze di mosse pos-sibili. Essendo S ben fondato, per ipotesi, ogni G ∈ S é ben fondato.Formalmente S+ = {〈x, σ〉 | x ∈ S ∧ σ ∈ x}, ovvero la prima mossa (x) éla scelta di un gioco in S ed il resto della partita (σ) é uno svolgimentodi x.

Se S+ fosse non ben fondato, esso conterrebbe una sequenza discen-dente infinita, ma ciò é possibile solo se esiste σ ∈ x per un certo x ∈ Stale che σ sia infinita, contro ipotesi.

Da cui segue che S+ é ben fondato.(2) Per assurdo, se S+ ∈ S allora in S deve esistere la sequenza

〈S+, 〈S+, 〈S+, . . . 〉〉〉

che ha lunghezza transfinita, per cui S+ non é ben fondato, contraddi-cendo il punto (1).

2

Corollario 56 Non esiste un insieme i cui elementi siano precisamente tuttii giochi ben fondati.

Dimostrazione. Per assurdo, sia S tale insieme, allora esiste S+ ed é benfondato per la proposizione precedente, quindi S+ ∈ S, assurdo. 2

Definizione 57 Sia S un insieme di giochi, l’ipergioco su S, indicato conS∗, é definito informalmente come segue: il giocatore I sceglie un gioco G ∈S ∪ {S∗}, poi il giocatore II inizia G, ed il resto del gioco é G. Il vincitore diS∗ é il vincitore di G.

In questo caso, é necessario provare che il gioco S∗ é ben definito in ZFA,ovvero che l’insieme delle sequenze di mosse che individua esista e sia unico.

Proposizione 58 Per ogni insieme di giochi S ben fondato, l’ipergioco S∗ éun gioco ben definito.

Dimostrazione. Ogni gioco é modellabile come una quadrupla

〈M,R,WI,WII〉

43

dove l’insieme M é costituito da tutte le possibili sequenze di mosse; R é unarelazione tra sequenze di mosse che afferma che, se σ R τ , allora τ corrispondead una possibile prosecuzione di σ;WI, WII sono sottoinsiemi di R che debbonoessere ben fondati, quindi i cui elementi siano sequenze finite, contenenti,rispettivamente, le sequenze che assegnano la vittoria al giocatore I ed algiocatore II.

Se G ∈ S indichiamo G = 〈MG, RG,WIG ,WIIG〉.

Consideriamo il seguente sistema di equazioni:

x = 〈y, z, w, v〉

y = M

z = R

v = WI

w = WII

(4)

con

M = {〈α, τ〉 | (α ∈ S ∧ τ ∈Mα) ∨ (α = x ∧ τ ∈ y)}

R é definita come: per ogni ρ ∈ M , se ρ = 〈x, . . . , x, τ〉 allora ρ R τ , τ ∈ M ,con un numero finito di x nel prefisso; se esiste un gioco G ∈ S ed un q taleche q ∈ MG, con ρ = 〈G, q〉 o ρ = 〈x, . . . , x, G, q〉, allora ρ R q; in ogni altrocaso R non vale.

Inoltre

WI = {ρ | ρ = 〈x, . . . , x, G, q〉 dove ρ ha lunghezza dispari e ρ ∈M〉}

WII = {ρ | ρ = 〈x, . . . , x, G, q〉 dove ρ ha lunghezza pari e ρ ∈M〉} .

É ovvio che il sistema (4) codifica S∗ per come abbiamo definito M , R e WI,WII.

Tuttavia (4) é un sistema generale di equazioni in ZFA, per cui ammette unaed una sola soluzione s. Ovviamente S∗ = sx.

In effetti é immediato provare che sx soddisfa la descrizione informale del-l’ipergioco; in conclusione la definizione di ipergioco é ben data. 2

Proposizione 59 Sia S un insieme di giochi ben fondati, allora S∗ non é benfondato, da cui S∗ 6∈ S.

44

Dimostrazione. Notiamo che, dalla costruzione formale di S∗, la sequenza〈S∗, S∗, . . . 〉 é una mossa lecita (ovvero é in MS∗), e nessun prefisso di essacostituisce una vittoria per alcun giocatore. Quindi S∗ non é ben fondato. 2

La lettura che questi risultati ci danno rispetto al paradosso dell’ipergioco éche, in realtà, la descrizione informale dell’ipergioco é ambigua: il paradossonasce dal fatto che, implicitamente, in tale descrizione, identifichiamo S+ conS∗.

Avendo provato che non esiste un insieme di tutti i giochi ben fondati, ab-biamo analizzato come formalizzare il paradosso preso un insieme di giochiben fondati (regolari). Il risultato é che, rifacendo la costruzione del paradosso,assumendo l’ipergioco irregolare, otteniamo un gioco regolare, il supergioco,che non appartiene all’insieme iniziale; invece facendo la costruzione inversa, incui, nel paradosso, si supponeva l’ipergioco regolare, ma che, in ZFA, possiamoeffettuare senza tale ipotesi, otteniamo l’ipergioco, e, come il paradosso deduce,esso risulta irregolare.

Una lettura alternativa dell’analisi condotta porta al seguente risultato:

Lemma 60 Sia s un insieme, allora non esiste alcun insieme a che sia solu-zione dell’equazione:

a = {b ∈ s ∪ {a} | b é ben fondato} .

Dimostrazione. Supponiamo che tale a esista. Per definizione, per ogni b ∈a, b é ben fondato, per cui a é ben fondato.

Ma allora a ∈ {b ∈ s ∪ {a} | b é ben fondato} = a, ovvero a é riflessivo equindi non ben fondato. 2

In conclusione possiamo leggere il paradosso dell’ipergioco come una lezioneche insegna che alcune classi di sistemi di equazioni tra insiemi di ZFA, han-no una unica soluzione, ma un sistema qualsiasi non ricade sotto il dominiodei risultati ottenuti sulla teoria di ZFA, e quindi nulla si può dire riguardoall’esistenza e/o unicità delle sue soluzioni.

3.3 Insiemi Ereditariamente Finiti

Spesso, in molte branche della Matematica [Bar77,MB65,Mac71,Csá78], si haa che fare con insiemi finiti, insiemi di insiemi finiti, . . .

45

Vi sono diversi modi di formalizzare una tale costruzione, e, in ZF, essisono equivalenti. In ZFA ciò non avviene e questo fatto illustra bene comel’intuizione nella teoria degli insiemi non ben fondati, sia differente.

Oltre a costituire un ottimo esempio per rimarcare le differenze tra ZFA e lateoria degli insiemi standard, specialmente in rapporto all’idea di circolarità,gli insiemi ereditariamente finiti forniscono anche una concreta applicazione,di per se interessante, di ZFA; il loro punto di forza é costituito dalle numeroseproprietà di cui godono e dal fatto che essi, seppur non cos̀i semplicementecome in ZFA, trovano formalizzazione anche nella teoria degli insiemi usuale.

Vi sono tre modi di formalizzare l’intuizione che sottende alla costruzione degliinsiemi ereditariamente finiti:

Definizione 61 Sia A un insieme; l’operatore ∆ é definito come:

∆(b) = Pfin(b ∪ A) = {c | c ⊆ b ∪ A ∧ |c| ∈ N}

Evidentemente ∆ é un operatore monotono.

Definiamo HF0[A] come il minimo punto fisso ∆∗; definiamo HF1[A] = ∆∗, il

massimo punto fisso di ∆. Infine definiamo HF1/2[A] come l’insieme costituitoda tutti gli elementi in HF1[A], la cui chiusura transitiva sia finita.

Al solito scriveremo HF0, HF1, HF1/2 al posto di HF0[∅], HF1[∅], HF1/2[∅].

Le relazioni tra questi insiemi sono descritte dalla seguente proposizione:

Proposizione 62 Sia A un insieme

(1) Se A é transitivo allora HF0[A], HF1/2[A], HF1[A] sono transitivi.(2) HF0[A] ⊆ HF1/2[A] ⊆ HF1[A].(3) HF0[A] = {b | b ∈ HF1[A] ∧ b é ben fondato}.(4) N ⊆ HF0[A].(5) Ω ∈ HF1/2[A].(6) 〈0, 〈1, 〈2, . . . 〉〉〉 ∈ HF1[A].(7) HF0[A] 6= HF1/2[A] e HF1/2[A] 6= HF1[A].

Dimostrazione.

(1) Osservando che, in generale, se A é transitivo e B é un punto fisso di ∆,allora B é transitivo, segue che HF0[A] e HF1[A] sono transitivi.

Per HF1/2[A], se a ∈ b, allora a+ ⊆ b+, dove x+ é la chiusura transitivadi x. Per cui se la chiusura transitiva di un insieme é finita, cos̀i é lachiusura transitiva di tutti i suoi elementi.

46

(2) In generale, per ogni operatore Γ monotono, Γ∗ ⊆ Γ∗, quindi HF0[A] ⊆

HF1[A].Usando il principio di induzione per HF0[A], si prova che HF0[A] ⊆

HF1/2[A]: sia b un sottoinsieme finito di A ∪ (HF1/2[A] ∩ HF0[A]); allorab+ = b ∪

⋃

a∈b a+ é una unione finita di insiemi finiti, ovvero B+ é finito.

In altre parole

Pfin(A ∪ (HF1/2[A] ∩ HF0[A])) = ∆(HF1/2[A] ∩ HF0[A]) ⊆ HF1/2[A] .

Per il principio di induzione segue che HF0[A] ⊆ HF1/2[A].Per provare che HF1/2[A] ⊆ HF1[A], notiamo che HF1/2[A] é un punto

fisso di ∆: questa é una conseguenza immediata del fatto che

b+ =⋃

{c+ | c ∈ b é un insieme} ∪ {x | x ∈ b é un atomo} .

(3) Sia WF la classe (propria) di tutti gli insiemi ben fondati:

Pfin(A ∪ (WF ∩ HF0[A])) ⊆ WF

poichè ogni insieme i cui elementi siano atomi o insiemi ben fondati é, asua volta, ben fondato. Quindi, per il principio di induzione su HF0[A],HF0[A] ⊆ WF , ovvero tutti gli elementi di HF0[A] sono ben fondati.Questo prova che

HF0[A] ⊆ {b | b ∈ HF1[A] ∧ b ∈ WF} .

Sia b ∈ WF ∩ HF1[A], assumiamo che ogni elemento c ∈ b con c ∈WF ∩ HF1[A], appartenga a HF0[A], allora b ⊆ A ∪ HF1[A] e b é finito.Ma WF e HF1[A] sono entrambe collezioni transitive e b ⊆ω HF

0[A] ∪Aper ipotesi, quindi, per ∈-induzione su WF , b ∈ HF0[A]. Ovvero WF ∩HF1[A] ⊆ HF0[A].

(4) Per induzione su N: si supponga che ogni m < n appartenga a HF0[A];poichè n é un insieme finito, n ⊆ω HF

0, quindi n ⊆ω HF0[A], ma questo

implica, per definizione di ∆, che n ∈ HF0[A].(5) Notando che Ω+ contiene un solo elemento, segue che Ω ∈ HF1/2[A].(6) La sequenza σ = 〈0, 1, . . . 〉 é un elemento di HF1[A], poichè ogni prefisso

proprio di σ é un insieme finito, per cui σ ∈ ∆∗ = HF1[A] per definizionedi massimo punto fisso.

(7) Poiché Ω ∈ HF1/2[A] e Ω non é ben fondato, Ω 6∈ HF0[A], quindi HF0[A] 6=HF1/2[A] e HF0[A] 6= HF1[A].

Inoltre la chiusura transitiva di σ =