TECNOLOGIA DELLA DIMOSTRAZIONE - CleverCoder.net - Gil...

Università degli Studi di Trieste

Facoltà di Scienze Matematiche, Fisiche e Naturali

Tesi di laurea in

MATEMATICA

TECNOLOGIA DELLA

DIMOSTRAZIONE

SVILUPPO DI UNO SCENARIO DI VERIFICA

AUTOMATICA

Relatore:

Laureando:

Prof. Eugenio Omodeo

Gil Vegliach

Correlatore:

Prof. Sergio Invernizzi

Anno accademico 2009-2010

[ 18 settembre 2010 at 15:34 ]

[ 18 settembre 2010 at 15:34 ]

I N D I C E

1 Introduzione 5

2 Perché verificare le dimostrazioni? 7

3 Cos’è un proof assistant? 13

4 Il verificatore Referee 17

5 Dimostrare in Ref 19

6 Verso il teorema di Stone... 25

7 Algebre booleane in Ref 27

8 La dimostrazione classica del teorema di Stone 31

9 La parte topologica:caratterizziamo la compattezza 339.1 Le leggi di De Morgan 37

10 Risultati finali e sviluppi futuri ... 39

bibliografia 40

3

[ 18 settembre 2010 at 15:34 ]

[ 18 settembre 2010 at 15:34 ]

1I N T R O D U Z I O N E

Nel corso della storia le dimostrazioni si sono fatte via via piùlunghe e complesse. La prima proposizione degli Elementi diEuclide, la costruzione di un triangolo equilatero dato un lato,riempiva poche righe (Euclide [2010]). Le dimostrazioni delleproposizioni non occupavano in generale più di una pagina. Iteoremi di oggi invece si estendono su svariati articoli tecnici,ognuno lungo decine di pagine. Si prenda ad esempio il teoremadell’indice di Atiyah-Singer1 oppure la più recente classificazionedei gruppi semplici finiti2. Come possiamo essere sicuri che que-ste dimostrazioni siano corrette? Come può aiutarci la tecnologiain questo compito?

Nel presente lavoro parleremo di proof-checking, cioè il pro-cesso di usare del software per controllare le dimostrazioni. Unadimostrazione scritta in un linguaggio formale viene data in pa-sto a un verificatore automatico, il quale la controlla e ci dice setutto è filato liscio oppure se qualcosa non va. In quest’ultimocaso viene generato un diagnostico con gli errori commessi, erroriche potranno venir corretti prima di una nuova esecuzione delverificatore.

Come particolare verificatore automatico useremo Ref, unsoftware sviluppato da Jacob T. Schwartz e E.Omodeo. Refè un verificatore automatico basato sulla teoria degli insiemi.

In Ref svilupperemo uno scenario che caratterizza la com-pattezza di uno spazio topologico attraverso le intersezioni diinsiemi chiusi.

Per quanto semplice, questo risultato è un primo passo versol’integrazione di un preesistente scenario sul teorema di Sto-ne sulla rappresentazione delle algebre di Boole con tutte leinformazioni topologiche del caso (Stone [1936]).

1 la dimostrazione del celeberrimo teorema dell’indice Atiyah-Singer compiutanegli anni ’60 era divisa in quattro lunghi articoli negli Annals of Mathematicse usava un sacco di strumenti da altre fonti

2 il teorema di classificazione dei gruppi semplici finiti è talmente lungo da esserechiamato teorema enorme

5

[ 18 settembre 2010 at 15:34 ]

[ 18 settembre 2010 at 15:34 ]

2P E R C H É V E R I F I C A R E L E D I M O S T R A Z I O N I ?

La prima volta che una persona è introdotta al concetto didimostrazione questo viene spiegato più o meno così

ragionamento deduttivo che partendo da certe ipotesi ve-rifica una tesi, la cui validità è dovuta alla coerenza delragionamento

In pratica una dimostrazione è un certificato di garanzia, unaprova inconfutabile della validità della nostra tesi. Perché con-trollare il certificato allora? Nessuno si preoccupa degli errorid’ortografia nella garanzia di un cellulare, ma la matematica èuna cosa diversa. La matematica parla di certezza, una certezzaderivata dal fatto di costruire i propri concetti tramite un rigo-roso procedimento logico-deduttivo, partendo da pochi assiomiritenuti veri.

In teoria uno potrebbe scommettere la casa sulla correttezzadella classificazione dei gruppi finiti semplici. In teoria funziona.In pratica nessuno lo farebbe mai: noi matematici commettiamospesso degli errori. Basta un segno invertito, una lettera scrittamale o qualche piccola svista ed ecco partire una serie di deduzio-ni errate. Su queste deduzioni costruiamo intere teorie, magari lepubblichiamo, finché ci accorgiamo del nostro errore. Il nostrocastello concettuale distrutto dalla rimozione di un solo mattone.

Gli errori possono infiltrarsi anche in ciò che non vediamo.Spesso un passaggio ci sembra ovvio e sicuramente non vale lapena verificare tutte le parti, perciò non le scriviamo. E abbiamoi nostri buoni motivi per questo comportamento: quando AlfredNorth Whitehead e Bertrand Russel provarono a scrivere tutti ipassaggi anche solo di una parte elementare della matematica,produssero un libro di 2000 pagine (Whitehead e Russell [2009]).Lo stesso Russell ammise ad un amico

non credo che alcun essere umano lo leggerà mai per intero

Tra piccole sviste e passaggi dimenticati la nostra sicurezzacomincia a vacillare. Come possiamo essere sicuri che il nostrolavoro sia corretto?

La soluzione di oggi si basa sul peer-review, la revisione deipari. Un articolo, prima di esser pubblicato, viene inviato ano-nimamente ai referee, anonimi arbitri che lavorano nel nostrostesso campo. I referee credono che il materiale sia corretto eche contenga della sostanza? Sì, allora il giornale si occupa dipubblicare l’articolo. La correttezza viene dunque ad essere unprocesso sociale, un processo che soffre degli stessi svantaggidel fattore umano visti sopra: piccoli errori possono sfuggire, epiccoli errori portano a grandi disastri.

Per fortuna i nostri punti deboli sembrano essere coperti dallatecnologia. Il computer, benché sprovvisto di alcuna intelligenzapropria, è molto veloce nel controllare una miriade di passi

7

[ 18 settembre 2010 at 15:34 ]

2 Perché verificare le dimostrazioni?

semplici. Se una dimostrazione potesse essere scritta nei suoipassi più elementari, un computer potrebbe facilmente verificarnela correttezza.

Questa è l’idea del proof-checking: scrivere una dimostrazionein tutti i suoi dettagli e poi farla controllare a un computer. Intutti i suoi dettagli significa ridurre una dimostrazione a livello dilogica proposizionale, in cui le regole di inferenza sono semplicie indiscutibili: la validità è garantita. Controllarla a computersignifica meccanizzare quello che è il peer-review di oggi: ilfattore umano può esser impiegato nel discutere il senso e l’utilitàdelle dimostrazioni invece che perder tempo sulla parte logica.

Per capire come il computer possa aiutarci in questo compitovedremo alcuni esempi di errori storici e come la tecnologia ci siavenuta in aiuto.il teorema dei 4

colori,il teorema piùverificato della storia

Nel 1852 Francis W. Guthrie, laureato al University Collegedi Londra, propose il seguente problema al fratello Frederick(Krantz [2007]):

Immagina una mappa sulla superficie della terra, una map-pa suddivisa in regioni. Non ci sono fiumi o laghi a divi-dere le regioni, né altre zone d’acqua. L’unica regola èche ogni regione sia un’unica massa contigua senza bu-chi. In qualità di cartografi, vorremmo colorare la mappain modo che nessuna regione adiacente abbia lo stesso co-lore. Quanti colori dobbiamo comprare? Quanti coloridobbiamo comprare per colorare una qualsiasi mappa?

Il problema passò di man in mano a molti matematici illu-stri: primo tra tutti Augustus De Morgan, 1 un professore diGuthrie, poi W. R. Hamilton 2 e infine A. Cayley 3 ne parlò inuna pubblicazione del 1878. Le voci arrivarono fino a Göttingendove Felix Klein4 dichiarò che l’unica ragione per cui il problemaera irrisolto era che nessun matematico capace ci aveva ancoralavorato. Lui ci provò e fallì. Ma la storia non finisce qui: nel 1879A. Kempe5 pubblicò una soluzione. La dimostrazione resistetteper undici anni quando P.Heawood6 trovò un errore. Purtroppol’errore di Kempe non era eliminabile anche se Heawood riuscìa tirare fuori molti concetti carini, come ad esempio il numerocromatico di una superficie. Un altro tentativo fallito fu a operadel matematico Tait: dimostrazione presentata nel 1880, erroretrovato nel 1891 da Peterson.

Dopo tutti questi tentativi falliti il teorema dei quattro colori di-ventava celebre: contributi parziali furono dati da Birkhoff, Frank-lin, Heesch e Stromquist ma nessuna dimostrazione completa eraancora conosciuta.

Così quando nel 1974 Kenneth Appel7 e Wolfgang Haken8

annunciarono di avere una dimostrazione la notizia si scontrò

1 Augustus De Morgan, 1806–1871. È l’autore delle famose leggi di De Morgan2 William Rowan Hamilton, 1805-1865. È l’autore del teorema di Cayley-Hamilton3 Arthur Cayley, 1821-18954 Felix Klein, 1849-19255 Alfred Bray Kempe, 1845-19226 Percy John Heawood,1861-19557 Kenneth Ira Appel, 1932–8 Wolfgang Haken, 1928–

8

[ 18 settembre 2010 at 15:34 ]

con un pubblico incerto e dubbioso. Era forse questa la voltabuona? La tecnica di Appel e Haken era di ridurre la casistica dimappe a 1936 configurazioni fondamentali, dimostrando indivi-dualmente il teorema per ogni configurazione. Fin qui niente dieccezionale, tranne per il fatto che le 1936 configurazione eranostate dimostrate dai supercomputer dell’università dell’Illinois,in circa 1200 ore di computer-time. Nessun essere umano sa-rebbe mai riuscito a controllare una dimostrazione così lunga ecomplicata e molto si dibattè se questa fosse una dimostrazionefilosoficamente accettabile. Finora per quanto una dimostrazionefosse stata una lunga e intricata sequenza di passaggi logici erasempre stato possibile che un altro essere umano la controlli.

I piccoli errori trovati nel programma

4-colorazione

negli anni a venire – sempre prontamen-te corretti – contribuirono ad aumentare isospetti.

Nel 1994 Paul Seymour e il suo grup-po all’università di Princeton trovarono unnuovo algoritmo più stabile per dimostrareil teorema. L’approccio soffriva dei stessiproblemi di quello di Appel e Haken manel 2004 Gonthier, uno scienziato alla Mi-crosoft Research a Cambridge, usò un proofassistant per controllare la dimostrazione

(Gonthier [2008]). La dimostrazione non era stata controllata daun essere umano ma almeno era stata controllata 9.

Una domanda però sorse spontanea: Se il verificatore avessedei bug la verifica non sarebbe stata valida. La correttezza delladimostrazione sarebbe nuovamente incerta. Come possiamoescludere questa eventualità?

Enunciato delteorema dei 4-coloriscritto da Gonthierin Coq v7.3.1

Variable R : real_model.Theorem four_color : (m : (map R))(simple_map m) -> (map_colorable (4) m). Proof.Exact (compactness_extension four_color_finite). Qed.

La risposta di Gonthier fu servirsi di un verificatore con unkernel il più corto possibile, con il minor numero possibile diassiomi e di regole d’inferenza. Anche se il software non sarà maiin grado di garantire la certezza assoluta la dimostrazione delteorema dei quattro colori diventò così una delle dimostrazionipiù scrupolosamente verificate della storia, citazione di Hales.

Hales è un professore di Pittsburgh che fu direttamente coinvol-to nel proof-checking quando dimostrò la congettura di Kepleronel ’98. la congettura di

KepleroLa congettura di Keplero nasce ingenuamente da una domandadi Sir Walter Releigh 10, al matematico inglese Thomas Harriot:

9 In cosa differisce l’uso del computer di A.& H. da quello di Gonthier? Usiamouna metafora, supponiamo di dover mostrare 1 + 1 = 2 usando un computer.A.&H. avrebbero lanciato l’applicazione Calcolatrice ed eseguito il conto. Gon-thier avrebbe assiomatizzato l’aritmetica, dimostrato che il successore di 1 sia 2e controllato il tutto con un software ad hoc

10 Sir Walter Releigh, 1552-1618. Navigatore, corsaro e poeta inglese

9

[ 18 settembre 2010 at 15:34 ]


”qual è il modo più efficiente per disporre le palle di cannone sulponte della mia nave” La domanda risultò di notevole interessematematico e fu passata da Harriot a Johannes Kepler 11 chela pubblicò nel 1611 in un libricino intitolato Strena seu de nivesexangula (Sul fiocco di neve e sei angoli)

Messa in uno stile più matematico la domanda non riguardaval’artiglieria ma suonava più o meno così: qual è il modo piùefficiente possibile di impacchettare sfere uguali nello spazio?

Può sembrare più astratto ma il problema è in pratica quelloche si trova ad affrontare un fruttivendolo ogni giorno: disporreil maggior numero di arance nel minor spazio possibile.

Facile da enunciare, ma non altrettanto da risolvere questoproblema ha una lunga storia: i primi contributi furono dati nelcaso bidimensionale da Carl Friedrich Gauss e Axel Thue.

Gauss provò che la disposizione regolare che garantisce ladensità più alta è il reticolo esagonale. Thue provò che il reticoloesagonale garantisce la densità più alta sia tra le disposizioniregolari, sia tra quelle irregolari (1890).

Il passo successivo verso una soluzione fu fatto dal matematicoungherese László Fejes Tóth 12. Nel 1953 Fejes Tóth mostrò cheil problema di determinare la massima densità di tutte le dispo-sizioni di sfere, regolari ed irregolari, poteva essere ridotto a unnumero finito, anche se molto grande, di calcoli. Questo signifi-cava che era possibile, almeno in linea di principio, trovare unadimostrazione per esaustione. Un computer sufficientemente po-tente avrebbe potuto fornire un approccio pratico alla risoluzionedel problema.

Nel frattempo vennero fatti tentativi per trovare un estremosuperiore per la massima densità di un qualunque impacchetta-mento di sfere. Il matematico inglese Claude Ambrose Rogersstabilì un limite superiore di circa 78% nel 1958, e tentativi succes-sivi fatti da altri matematici ridussero leggermente questo valore,che era comunque di molto superiore alla densità dell’impacchet-tamento cubico, cioè 74%. Furono anche prodotte dimostrazionierrate. L’architetto e geometra statunitense Buckminster Fulleraffermò di essere in possesso di una dimostrazione nel 1975, masi scoprì poco dopo che non era corretta. Nel 1993 Wu-Yi-Hsiang,all’University of California, Berkeley pubblicò un articolo in cuiaffermava di aver dimostrato la congettura di Keplero usandometodi geometrici. Alcuni esperti affermarono di non aver tro-vato motivazioni sufficienti per alcune delle sue affermazioni.Sebbene non fosse stato trovato nulla di scorretto nel lavoro diHsiang, la maggioranza del mondo matematico si trovò d’accor-do nell’affermare che la dimostrazione di Hsiang era incompleta.Uno dei critici più attivi fu proprio il nostro Thomas Hales, cheall’epoca stava lavorando a una sua dimostrazione.

Seguendo l’approccio suggerito da Fejes Tóth, Thomas Hales,all’epoca all’University of Michigan, determinò che la massi-ma densità di tutti gli impacchettamenti poteva essere trovataminimizzando una funzione di 150 variabili. Nel 1992, assisti-to dal suo allievo laureato Samuel Ferguson, diede inizio a un

11 Johannes Kepler (Giovanni Keplero), 1571-163012 László Fejes Tóth, 1915-2005

10

[ 18 settembre 2010 at 15:34 ]

programma di ricerca per applicare sistematicamente i metodidella programmazione lineare alla ricerca di un limite inferioreper il valore di questa funzione relativo a un insieme di più di5000 differenti configurazioni di sfere. Se, per ognuna di questeconfigurazioni, fosse riuscito a trovare un limite inferiore chesuperasse il valore relativo all’impacchettamento cubico, allorala congettura di Keplero sarebbe stata dimostrata. La ricerca ditutte queste limitazioni inferiori avrebbe richiesto la soluzionidi circa 100.000 problemi di programmazione lineare. Quandopresentò i progressi del suo progetto nel 1996, Hales affermò diessere in vista della fine, ma che avrebbe avuto ancora bisogno diun anno o due. Nell’agosto del 1998 Hales annunciò che la dimo-strazione era completa: 250 pagine di annotazioni e 3 gigabyte diprogrammi per computer, dati e risultati.

Hales non mandò la sua dimostrazione a una rivista qualsiasi,mandò la sua dimostrazione agli Annals of Mathematics. GliAnnals of Mathematics (Annali della matematica) è la rivistamatematica più prestigiosa al mondo e, come ci si aspetterebbe,è quella con le regole di pubblicazione più rigide. Non consideraarticoli troppo lunghi, cerca solo problemi di effettivo interessee pubblica solamente scritti in forma tradizionale. In breve, ladimostrazione di Hales non rispettava nessun standard dellarivista. Ciononostante Robert MacPherson, il Managing Editordella rivista, era interessato alle dimostrazioni fatte a computer.Credeva che il computer potesse risolvere i soliti vecchi problemi.E così considerò lo scritto. Fu istituita una commissione di dodicireferee e nel 2003, dopo quattro anni di lavoro, il capo della com-missione Gábor Fejes Tóth (figlio di László Fejes Tóth) annunciòche la commissione era certa al 99% che la dimostrazione eracorretta, ma che non poteva garantire la correttezza di tutti icalcoli fatti al computer.

Hales decise che certa al 99% non era abbastanza. Così ini-ziò il progetto FlysPecK, dove le lettere F, P e K sono le inizialidelle parole che compongono la frase Formal Proof of Kepler. Lasua stima è che ci vorranno 20 anni-persona di lavoro, cioè unlavoro di 20 anni per una singola persona, oppure 10 anni perdue persone. Ora progetto sembra essere a metà strada. L’im-portanza di questo anedotto riesiede nel fatto che nonostante ladimostrazione sia considerata sufficientemente corretta da unarivista prestigiosa come gli Annals of Mathematics lo stesso Halesnon è soddisfatto. Se possiamo citare con disinvoltura i teoremicontenuti negli Elementi di Euclide è perché la matematica sibasa su certezze assolute. E così, per ottenere la certezza assoluta,Hales si rivolse al mondo dei verificatori automatici.

Un altro esempio in cui i proof-assistant giocarono un ruolodecisivo fu quando il professore del Lynchburg College, ThomasNicely, scoprì un bug nell’istruzione di divisione del primo pen-tium della Intel nel ’94. Questa volta non si trattava di astrattiteoremi matematici ma di migliaia di computer nel mondo cheogni giorno sbagliavano di fare le divisioni. L’errore compariva il bug nei Pentiumsoltanto dopo svariate cifre decimali ed era sfuggito agli ingegne-ri della Intel. Nessun problema, dunque, per dividere il contodi una pizza, ma da un computer non ci si può aspettare questa

11

[ 18 settembre 2010 at 15:34 ]


superficialità.E la Intel l’aveva capito: quando Nicely mandò il suo report

nell’ottobre del ’94, l’azienda già si era accorta da qualche mesedel problema, ma aveva segretamente taciuto fino ad allora. Cosasarebbe successo se il grande pubblico si fosse accorto che iloro processori sbagliavano? Il danno economico sarebbe statoenorme.

Nicely aveva bisogno del computer nelle sue ricerche sui nu-meri primi: stava enumerando tabelle di numeri primi, coppiee triplette di primi quando notò delle discrepanze nei risultati.Le discrepanze erano cominciate quando era stato introdotto ilprimo Pentium nell’arsenale computazionale. Nicely continuòad inviare mail i suoi colleghi e amici chiedendo se anche lororisconstrassero lo stesso problema.

E così pian piano la storia si diffuse: comparsa in un articolodel Electronic Engineering Times il 7 novembre 1994, fu successi-vamente mandata in onda dalla cnn il 21 novembre dello stessoanno. La notizia ormai era giunta al grande pubblico tanto cheil bug si conquistò addirittura un nome–laddove di solito i bugsono catalogati con un banale numero di identificazione: Pentiumfdiv bug, dove fdiv è l’istruzione per la Floating-point Divisionnel linguaggio assembly x86.

Un duro colpo per la Intel, un danno eco-nomico e d’immagine. Molti utenti recla-marono la sostituzione del loro processori.

Intel rispose con un colpo d’ingegno: do-po aver ritirato i processori difettosi li tra-sformò in graziosi portachiavi con sopraincisa una citazione di Andy Grove, unodei fondatori della stessa Intel:

Bad companies are destroyed by crisesgood companies survive themgreat companies are improved by them

E così da quel giorno, un po’ per tenere fede alla frase ad effetto,un po’ per il colpo subito costato 475.000.000$, Intel migliorò sulserio: si affidò a software di verifica automatica per gli algoritmidei suoi processori. (La intel usa Hol light, lo stesso verificatoredel teorema dei quattro colori di Hales, vedi articolo di Geuvers[2009])

12

[ 18 settembre 2010 at 15:34 ]

3C O S ’ È U N P R O O F A S S I S TA N T ?

Un proof assistant è un programma che serve per formalizzareteorie matematiche. Formalizzare una teoria matematica significaesprimerla in un linguaggio logico-formale elaborabile da uncomputer, includendo tutti i teoremi, dimostrazioni e definizionidi cui la teoria stessa ha bisogno. Ogni dettaglio deve essereincluso: vietato etichettare un passaggio come ovvio o lasciarloal lettore.

Nella pratica un proof assistant legge un lungo file di testo,comprendente migliaia di righe di enunciati e definizioni e dicese il contenuto è corretto. Il file di input si chiama proof script, ela modalità di lavoro si dice batch. Il proof assistant fa il lavoro diun diligente ragioniere, ma invece che verificare pian piano unamiriade di conti, verifica per noi una lunga catena di inferenzelogiche.

Ogni proof assistant è distinto dalla sue caratteristiche, tra lepiù importanti c’è la sintassi. La sintassi determina il modo incui l’utente scriverà le dimostrazioni e può essere procedurale odichiarativa.

Una dimostrazione in stile dichiarativo è strutturata in blocchi.Ogni blocco dichiara una serie di affermazioni ognuna derivantedalle precedenti. Il sistema è responsabile di riempire i dettaglidi basso livello tra i vari passaggi. In sostanza, l’utente dice alverificatore dove vuole arrivare. Questo sistema, usato ad esempioda Mizar e Isabelle, è il modo naturale di pensare dei matematici,ma è poco efficiente e produce dimostrazioni molto prolisse.

Una dimostrazione in stile procedurale contiene invece tutti ipassaggi. Ogni passaggio è come un comando di basso livelloal proof assistant. In sostanza, l’utente dice al proof assistantcosa vuole fare. Questo è lo stile adottato da Gonthier quandoformalizzò la dimostrazione del teorema dei quattro colori inCoq (Wiedijk [2007]).

Quale sia il miglior approccio è in fase di discussione: laddoveuno stile dichiarativo e classico assomiglia molto al modo natu-rale di pensare di un matematico, produce dimostrazioni moltolunghe e tediose. Uno stile procedurale è meno naturale, mapermette di scrivere meno, fattore chiave in dimostrazioni lunghecome quella del teorema dei quattro colori. Per una discussionesi veda l’articolo di F. Wiedijk (Wiedijk [2007])

La prima volta che si utilizza un proof assistant, subito ci sirende conto del livello di dettaglio necessario: leggi insiemisticheconsiderate ovvie come la distributività dell’intersezione rispettol’unione oppure le leggi di De Morgan vanno dimostrate passo apasso (vedi appendice), e in generale ogni dimostrazione è cinquevolte più lunga della sua controparte informale. Per questo è difondamentale importanza la costruzione di una libreria standardcon i risultati più comuni della matematica: ciò permetterebbe dinon dover riscrivere ogni volta i risultati più comuni.

13

[ 18 settembre 2010 at 15:34 ]

3 Cos’è un proof assistant?

Un progetto in questa direzione si può trovare al sito (Wiedijk[2010]). È una specie di top 100 della matematica, una lista di100 teoremi ben noti di cui ogni matematico riconoscerebbe ilvalore. I teoremi spaziano in complessità e difficoltà: si partedall’irrazionalità di radice di 2 al teorema fondamentale dell’alge-bra, passando per il teorema del punto fisso di Brouwer e per ladisuguaglianza media geometrica vs media aritmetica. Lo scopoè creare una lista standard di teoremi da formalizzare, un fermopunto di partenza su cui poi costruire altri teoremi. La statoattuale del progetto (settembre 2010) copre l’84% dei teoremi,nello specifico abbiamo i seguenti risultati:

Verificatore % th. formalizzatiHol Light 75Mizar 51Coq 49C-CoRN 10Isabelle 46ProofPower 42PVS 15nqthm/ACL2 12NuPRL/MetaPRL 8

Nella lista, notiamo che la maggior parte del lavoro è stata fattaper i primi tre verificatori. Non è un caso, infatti questi sono iproof assistant più diffusi: Hol light, Mizar e Coq. Ne faremoun rapido confronto, in cui emergeranno altre funzionalità chepuò avere un verificatore.Hol light

Hol light (High Order Logic) è un dimostratore interattivodiscendente dal progetto lcf (Logic for Computable Functions),un altro dimostratore automatico sviluppato da Robert Milner nel1972. Hol è interattivo, cioè i comandi possono essere immessiuno alla volta, senza ricorrere alla modalità batch. La sintassi èdichiarativa, usa la logica classica e quindi ben si presta per chi èalle prime armi.

Il punto forte di Hol Light è la leggerezza: solo dieci rego-le d’inferenza e un kernel da meno di 500 righe di codice. Isostenitori sono così soddisfatti di questa caratteristica che stam-parono delle magliette con il codice sorgente in toto in segno dipropaganda.Mizar

Mizar è un sistema sviluppato da Trybulec a partire dal 1973all’università di Bialystock. Il linguaggio di Mizar ricalca quellodella matematica informale: è dichiarativo come Hol, ed è basatosu una teoria degli insiemi tipo Zermelo Fraenkel.

Lo progetto Mizar prevede non solo lo sviluppo del software,ma anche lo sviluppo di una libreria di articoli matematici formali,chiamata Mizar Mathematics Library (mml). Attualmente (omeglio al tempo della pubblicazione dell’articolo Mizar: Animpression, di Freek Wiedijk) la libreria contiene 587 articoli,occupanti uno spazio totale di 41 megabyte.Coq

Coq non solo fa il verificatore ma può anche descrivere spe-cifiche formali per lo sviluppo software o essere usato comelinguaggio funzionale di programmazione. È stato sviluppato

14

[ 18 settembre 2010 at 15:34 ]

in Francia, nel progetto TypiCal (ex progetto LogiCal) in siner-gia dalla inria, dalla École Polytechnique, dalla Paris-Sud 11University e dalla cnrs.

Coq implementa un linguaggio d’ordine superiore chiamatoGallina. Gallina è un linguaggio funzionale tipato basato sulcalcolo delle costruzioni induttive, cioè una variante d’ordinesuperiore del lambda calcolo tipizzato sviluppata da ThierryCoquand. Coq è stato utilizzato da Gonthier nella dimostrazionedel teorema dei quattro colori, la dimostrazione formale piùlunga fino ad oggi.

Dopo questa carrellata sui maggiori verificatori, vediamo comefunziona il nostro verificatore Ref. In Ref svilupperemo i proof-script che ci porteranno verso il teorema di Stone.

Tre pionieri. . .1954 M.Davis implementa l’algoritmo di Pre-

sburger per l’addizione aritmetica nelcomputer “Johniac” all’Institute for Ad-vanced Study. Johniac dimostrò chela somma di due numeri pari è pa-ri iniziando l’era della dimostrazione acomputer

1956 Inizia la formalizzazione dei PrincipiaMathematica di Russel e White. Entro lafine del 1959, la procedura di Wang avevagenerato dimostrazioni per ogni teoremadel calcolo predicativo contenuta nel libro

1968 N.G de Bruijn progetta il primo program-ma per verificare dimostrazioni matema-tiche. Il programma di nome Automa-th controllò ogni proposizione di un te-sto che Landau scrisse per la figlia sul-la costruzione dei numeri con i tagli diDedekind

1

1 tabella presa da Hales [2008]

15

[ 18 settembre 2010 at 15:34 ]

[ 18 settembre 2010 at 15:34 ]

4I L V E R I F I C AT O R E R E F E R E E

Ætnanova, Refeeree o più semplicemente Ref, è un verificatoreautomatico basato sulla teoria degli insiemi sviluppato da JacobT. Schwartz (Omodeo et al. [2006]). Funziona nel seguente modo:l’utente scrive la propria dimostrazione su un file, la carica sulweb e lancia il verificatore. Il verificatore si preoccuperà di pro-cessare l’intero file–lavora in modalità batch–e ritornerà la paginadei tempi di verifica e degli eventuali errori.

Un errore sintattico fermerà immediatamente il verificatore: ilparser non riconoscerebbe più gli altri comandi. Un errore logicopermetterà comunque al verificatore di terminare l’esecuzione,generando una lista diagnostica con i problemi da correggere. Inquesta ottica Ref è più vicino a un compilatore di un linguaggiodi programmazione che ad un interprete: possiamo dargli inpasto molte righe alla volta piuttosto che doverlo lanciare dopoogni comando.

Un tipico scenario in Ref contiene un mix delle seguenti cose:teoremi più dimostrazioni, definizioni, teorie. Ogni dimostra-zione può citare solamente teoremi già verificati, che precedanol’attuale teorema in fase di verifica. Stessa sorte per le definizioni:gli oggetti da usare devono essere stati definiti precedentemente.

Quando abbiamo un sostanziale numero di teoremi e definizio-ni possiamo riunirli in una teoria, cioè in una struttura di livellopiù alto che serve a modularizzare il lavoro. Le teorie conferi-scono un tocco del secondo ordine su un sistema che altrimentisi baserebbe su una logica del primo. Esempi di teorie possonoessere la teoria sugli spazi topologici (topologicalSpace) o quellasul principio d’induzione finita (finiteInduction).

Illustriamo ora le caratteristiche di Ref tramite una dimostra-zione esemplificativa.

17

[ 18 settembre 2010 at 15:34 ]

[ 18 settembre 2010 at 15:34 ]

5D I M O S T R A R E I N R E F

Prendiamo il seguente semplice teorema

Teorema 1:�{Y ∩ X : X ∈ C} = Y ∩

�{X : X ∈ C}

Il teorema dice che l’intersezione binaria d’insiemi distribuiscesull’unione arbitraria di insiemi. Niente di difficile. Il nostrocompito è tradurre la dimostrazione standard in una formaledigeribile da Ref.

Il primo passo è scrivere l’enunciato in modo formale. Nell’e-nunciato compare l’unione di una collezione d’insiemi e poichéRef non ha un simbolo built-in per tale scopo, la nostra primamissione è fornire questa definizione. Questo può essere fattosemplicemente con le seguenti righe

Def unionset: [unionset di una famiglia d’insiemi]Un(C) := { w: Y in C, w in Y }

La sintassi è molto naturale e ricalca la definizione che si puòtrovare in un libro di matematica. Le specifiche dell’istruzioneDef, come si può leggere nel manuale, sono

Def definitionName: symbolName(params): definisce il simbolo sym-bolName: può essere una costante, una funzione o un predicato

Ora possiamo scrivere l’enunciato del teorema

Theorem 1: [distrib. dell’intersezione sull’unione]Un({ Y * X : X in C }) = (Y * Un(C)). Proof:Suppose_not(Y0,C0) ==> AUTO

Tsomehow ==> falseDischarge ==> QED

Qui notiamo le prime caratteristiche vere e proprie di Ref: i teo-remi vengono annunciati dalla parola Theorem, segue un numeroo un nome identificativo e un facoltativo commento tra parentesiquadre. Scritto l’enunciato si mette un punto “.” e quindi laparola chiave Proof:. Dopodiché si inizia la dimostrazione vera epropria.

Le dimostrazioni si dividono in passi. Ogni passo ha la seguen-te struttura: Hint ⇒ Expr. Hint indica il meccanismo inferenzialeusato, Expr è la conclusione parziale che abbiamo raggiunto.

Il primo passo in una dimostrazione è sempre la negazionedella tesi, cioè la dimostrazione è “per assurdo”. L’Hint che ser-ve allo scopo è la Suppose_not. Questa istruzione, come la sua

19

[ 18 settembre 2010 at 15:34 ]

5 Dimostrare in Ref

cugina Suppose, apre una sottodimostrazione (in questo caso ladimostrazione principale) e svolge lo stesso ruolo che le espres-sioni supponiamo che non. . . e supponiamo che. . . svolgerebbero inun ordinario testo matematico.

La dicitura seguente, AUTO, svolge il compito più naturale cheviene suggerito dall’Hint prima della freccia (⇒). In questo casonega automaticamente la tesi.

Ogni sottodimostrazione deve essere chiusa da una Dischargeche scarica le ipotesi temporanee e mostra le conclusioni rag-giunte. Nel caso si chiuda la Suppose_not della dimostrazioneprincipale, la conclusione raggiunta sarà la fine della dimostra-zione, segnalata con la parola chiave QED. Da questo momento ilteorema sarà utilizzabile nella dimostrazione di altri teoremi.

Capita spesso di dover scrivere degli enunciati e di dimostrarlisolo in seguito: in questa situazione la prassi è scrivere una rigadel tipo

Tsomehow ==> false

Questa riga cita un inesistente teorema somehow che dovrebbeportare a una contraddizione. In questo modo possiamo concen-trarci sui teoremi più importanti lasciando in sospeso i lemmiaccessori.

Prima di vedere la dimostrazione matematica e trasformarlain una di Ref, riportiamo le specifiche delle istruzioni fin quiutilizzate

• Suppose: introduce un’ipotesi e relativa sottodimostrazione

• Discharge: chiude una sottodimostrazione

• Suppose_not: versione particolare della suppose per le di-mostrazioni per assurdo. È sempre il primo passo in unadimostrazione

• AUTO: introduce della assunzioni in modo implicito chevengono ricavate automaticamente dall’Hint utilizzata

• QED: chiude una dimostrazione e rende citabile il teorema

Faremo un parallelo tra dimostrazione usuale e formale. Que-sto aiuterà il lettore sia a capire come funziona Ref partendo daun punto di vista a lui noto, sia a sviluppare le dimostrazioni perconto proprio. La dimostrazione usuale suonerebbe più o menocosì

Dimostrazione. “⊆”: Sia z ∈ �{Y ∩ X : X ∈ C}, per definizionedi unione abbiamo ∃X0 ∈ X : z ∈ Y ∩ X0.

Dato che Y ∩ X0 ⊆ Y ∩�{X : X ∈ C} otteniamo z ∈ Y ∩�{X :X ∈ C}.

20

[ 18 settembre 2010 at 15:34 ]

“⊇”: Sia z ∈ Y ∩ �{X : X ∈ C}, per definizione di intersezioneed unione abbiamo: z ∈ Y ∧ ∃X0 ∈ X : z ∈ X0.

Quindi z ∈ Y ∩ X0 e dato che Y ∩ X0 ⊆�{X ∩ Y : X ∈ C}

otteniamo z ∈ �{X ∩Y : X ∈ C}

Tuttavia Ref accetta solo dimostrazioni per assurdo e quindidovremmo modificare leggermente la nostra dimostrazione. Lalunghezza non varia di molto.

Dimostrazione. “ �⊆”: Dato che vale “ �⊆” abbiamo che ∃z : z ∈�{Y ∩ X : X ∈ C} ∧ z �∈ Y ∩�{X : X ∈ C}.Per definizione di unione abbiamo ∃X0 ∈ X : z ∈ Y ∩ X0.

Assurdo perché Y ∩ X0 ⊆�{X : X ∈ C}

“ �⊇”: Dato che vale “ �⊇” abbiamo che ∃z : z ∈ Y ∩ �{X : X ∈C} ∧ z �∈ �{Y ∩ X : X ∈ C}

Per definizione di intersezione ed unione abbiamo z ∈ Y ∧∃X0 ∈ C : z ∈ X0, dunque z ∈ Y ∩ X0. Assurdo perché Y ∩ X0 ⊆�{Y ∩ X : X ∈ C}

Ora possiamo finalmente arrivare alla dimostrazione formale.Riportiamo lo scenario completo, per provarlo basta copiarlo neldimostratore.

--BEGIN HEREDef unionset: [unionset di una famiglia d’insiemi]Un(C) := { w: Y in C, w in Y }

Theorem 1: [distrib. dell’intersezione sull’unione]Un({ Y * X : X in C }) = (Y * Un(C)). Proof:Suppose_not(Y0,C0) ==> Stat0: AUTO

z-->Stat0 ==> AUTOUse_def(Un({ Y0 * X : X in C0 })) ==> AUTO

SIMPLF ==> Un({ Y0 * X : X in C0 })= { w: X in C0, w in (Y0 * X) }

Use_def(Un(C0)) ==> AUTO

Suppose ==> (z notin (Y0 * Un(C0)))& Stat1: (z in { w: X in C0, w in (Y0 * X) })

(X0,w)-->Stat1 ==> (z in (Y0 * X0)) & (X0 in C0)& Stat3: (z notin { w: X in C0, w in X })

(X0,z)-->Stat3 ==> falseDischarge ==> (z in Y0)

& (z notin Un({Y0 * X : X in C0 }))& Stat4: (z in { w: X in C0, w in X })

(X1,w1)-->Stat4 ==> (z in X1) & (X1 in C0)& Stat5: (z notin { w: X in C0, w in (Y0 * X)})

(X1,z)-->Stat5 ==> falseDischarge ==> QED--END HERE

21

[ 18 settembre 2010 at 15:34 ]

5 Dimostrare in Ref

La prima riga è una novità: ogni scenario completo inizia conla riga

--BEGIN HERE

Questo comando fa partire il verificatore. Un’istruzione simileper fermarlo compare alla fine

--END HERE

L’istruzione per metterlo in stand-by sarebbe

--PAUSE HERE

ma non ne avevamo bisogno in uno scenario così corto.Le righe seguenti, come abbiamo già visto, sono la definizione

di unione e l’enunciato del teorema. Un’altra novità comparedopo la Suppose_not: prima della parola AUTO figura un’etichet-ta. Un’etichetta battezza un passo della dimostrazione con unnome, nome che si potrà usare per sostituire variabili all’internodel passo stesso. Infatti, nella riga successiva, introduciamo unelemento z nello Stat0, con

z --> Stat0 ==> AUTO

Lo Stat0 negava la tesi, cioè diceva che i due insiemi erano diversi.Inserire un elemento z in questo Stat significa trovare un z chedifferenzia i due insiemi.

Un uso più avanzato delle etichette è la restrizione del conte-sto in cui operano le regole d’inferenza. Ad esempio, quandooperiamo con una ELEM (inferenza insiemistica elementare), l’i-struzione tenta di derivare la conclusione voluta prendendo aipotesi tutti i passaggi precedentemente dimostrati. Con un’op-portuna restrizione del contesto suggeriamo alla ELEM le ipotesispecifiche che le servono. È facile dare questo tipi di suggeri-menti: basta scrivere (Statx), dove Statx è lo statment che indical’ipotesi cercata. Così facendo acceleriamo parecchio la verifica,ma lo sforzo vale la fatica solamente se lo scenario è di una cer-ta consistenza: per questo motivo non abbiamo incluso questatecnica in questa dimostrazione.

L’istruzione Use_def che troviamo subito sotto espande la defi-nizione di unione. L’espansione delle definizioni è necessaria perdire al verificatore come sono fatti gli oggetti che stiamo usando:per dire che un elemento sta nell’unionset bisogna prima saperecom’è fatto l’unionset.

Ref non può indovinare il simbolo da espandere tra l’enormenumero di possibilità disponibili, ma con dati sufficienti puòespandere la definizione di un simbolo dato senza doverla riscri-verla esplicitamente. Questo è il senso della parola chiave AUTO:diamo un simbolo e dei parametri su cui lavora il simbolo a unaUse_def e Ref espande per noi la definizione

22

[ 18 settembre 2010 at 15:34 ]

Da qui in poi la dimostrazione formale ricalcalca quella stan-dard. La prima Suppose tratta il caso “ �⊆” : a destra della frecciaabbiamo la nostra ipotesi con le definizione espanse.

Riprendiamo in mano le sostituzioni, vedremo come le gestisceRef. Quando affermiamo un’appartenenza come

Stat1: z in { w: X in C0, w in (Y0 * X) }

Ref traduce l’espressione in una formula con quantificatoreesistenziale:

Stat1: (EXISTS X,w|(z=w) & (X in C0) & (w in (Y0 * X)))

Ora il senso di

(X0,w) -->Stat1 ==> (z in (Y0 * X0)) & (X0 in C0)

dovrebbe essere chiaro: al posto della variabili quantificate creia-mo due costanti (X0, w) che hanno le proprietà a destra dellabarra, i.e. z = w ∧ X0 ∈ C0 ∧ w ∈ Y0 ∩ X0. Eseguendo un ra-gionamento basato sulla teoria degli insiemi, come se avessimorichiamato una ELEM, otteniamo la conclusione a destra dellafreccia, i.e. z ∈ Y0 ∩ X0 ∧ X0 ∈ C

La seconda sostituzione è essenzialmente diversa. Quandoaffermiamo la non-appartenenza

Stat3: (z notin { w: X in C0, w in X })

Ref traduce l’espressione in una formula con quantificatoreuniversale:

(FORALL X,w | (z /= w) or (X notin C0) or (w notin X))

La sostituzione

(X0,z) --> Stat3 ==> false

dunque non crea dei nuovi nomi di costante come sopra, ma inse-risce quelli già esistenti nella formula a destra della barra. Il falsedopo la freccia indica che siamo arrivati a una contraddizione.

La seconda parte della dimostrazione è analoga, tranne perun’unica cosa ancora da notare: Ref non può riutilizzare i nomidelle costanti definite in sottodimostrazioni. Dunque non pos-siamo più usare X0 e w come nomi, ma dobbiamo inventarne dinuovi, X1 e w1.

A conclusione del capitolo riportiamo la descrizione delleultime istruzioni più importanti.

In particolare la ELEM è di fondamentale importanza: esegueragionamenti insiemistici elementari e viene automaticamenterichiamata dopo ogni istruzione. Per questo motivo non comparenella nostra dimostrazione: viene tacitamente adoperata dopo lesostituzioni.

23

[ 18 settembre 2010 at 15:34 ]

5 Dimostrare in Ref

THEORY e ENTER_THEORY sono le direttive per creare edaccedere alle teorie. Senza creare inutili teorie giocattolo qui, lespiegheremo più avanti quando parleremo di algebre booleane edel teorema di Stone.

• ELEM : dimostrazione usando ragionamenti elementari su-gli insiemi

• EQUAL : dimostrazione usando sostituzioni di uguali-per-uguali

• (e1, . . . , en) → Statn: introduce espressioni e/o costanti nel-l’etichetta Statn

• (e1, . . . , en) → Ttheorem: introduce espressioni e/o costantinel teorema theorem

• Use_def(symbol): espande la definizione di un simbolo

• Loc_def symbolName(params): simile a Use_def, ma la defi-nizione dura soltanto una dimostrazione

• THEORY theoryName : introduce una nuova teoria, pre-sentando i nuovi simboli di funzione e i nuovi simboli dicostante assunti dalla teoria e gli eventuali presupposti chegli argomenti della teoria devono soddisfare

• ENTER_THEORY theoryName : definisce l’inizio del con-testo di una teoria, dove vengono date le definizioni e ledimostrazioni interne alla teoria stessa

• APPLY : deriva delle conclusioni da teoremi precentementeprovati in una teoria. Svolge anche compiti di meccanismodefinitorio di alto livello

24

[ 18 settembre 2010 at 15:34 ]

6V E R S O I L T E O R E M A D I S T O N E . . .

Lo scopo del mio lavoro era trovare un modo per unire i risultatiprecedenti sulle algebre booleane ai risultati elementari di topolo-gia, in vista della dimostrazione del teorema di Stone. Il teoremadi Stone dice

Teorema 2: Ogni algebra booleana B è isomorfa all’algebra dei sot-toinsiemi chiusaperti del suo spazio di Stone S(B). Per ogni alge-bra booleana B il suo spazio di Stone S(B) è uno spazio di Hausdorffcompatto e totalmente sconnesso.

Il teorema di Stone si può dividere in due grosse parti: la primadice che ogni algebra booleana è isomorfa ad un campo d’insiemi,la seconda che questo campo d’insiemi è un particolare spaziotopologico. Un preesistente scenario conteneva già la dimostra-zione della prima parte ma mancava della seconda. Occorrevasviluppare una teoria degli spazi topologici che contenesse glienunciati utili per il nostro scopo. Ma la topologia è vasta, svi-luppare la teoria nella sua interezza sarebbe lungo e senza scopo:cosa ci serve per la dimostrazione formale del teorema di Stone?

Per capirlo dobbiamo fare tre cose:

• capire cosa abbiamo già in mano, i.e. vedere la teoria dellealgebre booleane in Ref

• studiare la dimostrazione classica e vedere dove entra ingioco la topologia

• implementare in Ref la parte topologica

Prima di iniziare però, riportiamo velocemente qualche defini-zione sulle algebre booleane, sugli spazi topologici e sugli spazidi Stone. Il lettore che le ricorda può tranquillamente saltarle.

Definizione 1: Un’algebra booleana è un reticolo completo distribu-tivo con unità. Un reticolo è una coppia (L,≤) in cui L è un insieme,≤ è un ordinamento parziale su L e per ogni coppia x, y ∈ L esistonoil sup, denotato con x ∨ y, e l’inf, denotato con x ∧ y. Completo si-gnifica che ogni sottoinsieme di L limitato superiormente deve avere ilsup. Distribuitivo significa che per ogni x, y, z ∈ L vale

x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z)

Avere un’unità 1 significa che 1 ∈ L e per ogni x ∈ L vale x ≤ 1

Definizione 2: Lo spazio di Stone S(B) di un’algebra booleana B èdefinito come l’insieme degli omomorfismi da B in 2, dove 2 è l’algebrabooleana con due elementi. Definiamo ora la base per la topologia delteorema di Stone: sia x ∈ B consideriamo l’insieme Sx(B) degli omo-morfismi che mandano x in 1 ∈ 2. La collezione {Sx(B) : x ∈ B} è lanostra base. Infine uno spazio topologico è di Hausdorff quando ogni

25

[ 18 settembre 2010 at 15:34 ]

6 Verso il teorema di Stone...

sua coppia di punti può esser separata da intorni disgiunti. Uno spaziotopologico è connesso quando ha sconnessioni. Una sconnessione è unacoppia di aperti disgiunti e non vuoti che uniti insieme danno tutto lospazio. Uno spazio topologico è totalmente sconnesso quando le unichecomponenti connesse sono i singoletti e l’insieme vuoto. Uno spaziotopologico è compatto quando da ogni suo ricoprimento aperto si puòestrarre un sottoricoprimento finito.

26

[ 18 settembre 2010 at 15:34 ]

7A L G E B R E B O O L E A N E I N REF

Siamo al primo passo del nostro piano di battaglia: capire lateoria già sviluppata in Ref. Nel farlo spiegheremo velocementecome funzionano le teorie. Riportiamo il codice per la teoria dellealgebre booleane.

Theory booleanAlgebra�bb, U · V, U + V + ee

�

-- assunzioni di non vacuità

ee ∈ bbee �= ee, ee

-- proprietà di chiusura

�∀x, y | {x, y} ⊆ bb → x · y ∈ bb��∀x, y | {x, y} ⊆ bb → x + y ∈ bb�

-- leggi associative

�∀x, y, z | {x, y, z} ⊆ bb → x · (y · z) = (x · y) · z��∀x, y, z | {x, y, z} ⊆ bb → x + (y + z) = (x + y) + z�

-- leggi distributive

�∀x, y, z | {x, y, z} ⊆ bb → (x + y) · z = (z · y) + (z · x)�

-- zero additivo

�∀x, y | {x, y} ⊆ bb → (x + x) = (y + y)�

-- legge di auto-eliminazione

�∀x, y | {x, y} ⊆ bb → x + (y + x) = y�

-- idempotenza della moltiplicazione

�∀x | x ∈ bb → x · x = x�

-- unità moltiplicativa

⇒ (cmpΘ, IdealΘ, BooHomΘ, hhΘ, phiΘ)

[. . . ]

�∀x, y | x, y ∈ bb → phiΘ�x · y = phiΘ�x ∩ phiΘ�y & phiΘ�(x + y) = phiΘ�x�phiΘ�y�phiΘ�ee =

�range(phiΘ) & phiΘ�zzΘ = ∅ & phiΘ�ee �= phiΘ�zzΘ

�∀x | x ∈ bb → phiΘ�cmpΘ(x) = phiΘ�ee\phiΘ�x�One_1_map(phiΘ) & domain(phiΘ) = bbBooHomΘ(phiΘ)

End booleanAlgebra

Le teorie sono dei meccanismi designati per agevolare lo svi-luppo di dimostrazioni su larga scala, cioè proprio quello che ci

27

[ 18 settembre 2010 at 15:34 ]

7 Algebre booleane in Ref

serve per sviluppare il nostro scenario. Una teoria si dichiara conla parola chiave THEORY a cui seguono il nome e i parametrisu cui si basa la teoria stessa. I parametri in questo caso sono ilsupporto (bb), le due operazioni (· e +) e l’unità moltiplicativa(ee). L’unità additiva invece è implicita poiché viene ricavata dalleassunzioni della teoria. Le assunzioni sono le righe che seguonola dichiarazione della teoria fino alla freccia ⇒ e corrispondonoagli assiomi delle algebre booleane.

Enunciata una teoria con i suoi parametri e scritti gli assiomiotteniamo i simboli specifici della teoria (cmpΘ, IdealΘ, BooHomΘ,hhΘ, phiΘ), contraddistinti con un Θ, e una serie di teoremiverificati da tutti gli oggetti istanziati da tale teoria.

I simboli specifici di una teoria devono essere dimostrati dentroil contesto della teoria. Stessa sorte per i teoremi di una teoria.Per entrare nel contesto di una teoria possiamo usare la paro-la chiave ENTER_THEORY (si veda il capitolo 5 per la sintassidell’istruzione): i simboli e i teoremi qui definiti saranno visibilisolamente all’interno di tale ambito. Entrati in un contesto, abbia-mo a disposizione anche tutti gli assunti di una teoria. Gli assuntipossono essere usati come ipotesi aggiuntive richiamandoli conl’istruzione Assump.

Abbiamo abbreviato la lista (lunghissima) dei teoremi sullealgebre booleane per evidenziare unicamente quelli importantiper il teorema di Stone.

Il primo dice che l’immagine di ogni prodotto è intersezionedelle immagini dei fattori e che l’immagine della somma booleanaè la differenza simmetrica delle immagini degli addendi. Sono leproprietà esplicitate caratteristiche di un omomorfismo: servonoper mettere in luce che il codominio sia un campo d’insiemi.

Il secondo dice che l’unità moltiplicativa ee dell’algebra corri-sponde al massimo insieme nel codominio dell’omorfismo e chel’unità additiva zzΘ corrisponde all’insieme vuoto.

Il terzo dice l’operazione di complemento booleano corrispon-de alla complementazione insiemistica.

Il quarto dice che phiΘ è iniettiva e il quindi che phi è unomomorfismo booleano.

Questi quattro teoremi uniti assieme implicano il teorema diStone in cui campo d’insiemi è l’immagine dell’omomorfismophiΘ.

Non ci dilungheremo a commentare altri risultati della teoria,in quanto per usarla ci basta conoscere i suoi assiomi e le sueproprietà. Questo infatti è un altro vantaggio delle teorie: crearescatole chiuse che possono essere usate senza conoscerne il conte-nuto. Il lettore interessato potrà consultare lo scenario completoin appendice.

Una cosa interessante da notare, anche se non è stata esplicita-mente scritta, è il lemma di Zorn. La dimostrazione del teoremail lemma di Zorndi Stone richiede la proprietà d’esistenza di un ideale massimale,teorema che richiede il lemma di Zorn. Ciò è ovviamente statodimostrato nella parte della teoria delle algebre booleane masarebbe prolisso ora mostrarne tutte le dipendenze (da notare inparticolare l’uso dell’induzione transfinita). Si possono trovare i

28

[ 18 settembre 2010 at 15:34 ]

dettagli in appendice e nel libro di Schwartz (Dunford e Schwartz[1958])

Il lemma di Zorn in Ref è enunciato così

Theorem 412: [Zorn’s lemma]�∀x ⊆ T | �∀u ∈ x, v ∈ x | u ⊇ v ∨ v ⊇ u�→ �∃w ∈ T, ∀y ∈ x | w ⊇ y��→ �∃y ∈ T, ∀x ∈ T |¬(x ⊇ y & x �= y)�.

L’uso di questo lemma, equivalente all’assioma della scelta,rende la dimostrazione non costruttiva.

29

[ 18 settembre 2010 at 15:34 ]

[ 18 settembre 2010 at 15:34 ]

8L A D I M O S T R A Z I O N E C L A S S I C A D E LT E O R E M A D I S T O N E

Siamo al secondo passo del nostro piano di battaglia: capire ladimostrazione del teorema di Stone. Per la dimostrazione delteorema ci ispiriamo al testo di Schwartz (Dunford e Schwartz[1958]) che riportiamo brevemente

Dimostrazione della parte topologica. [. . . ] Ci rimane da mostra-re che S(B) può essere topologizzato in maniera che gli insie-mi Sx(B) al variare di x ∈ B siano esattamente i sottoinsiemichiusaperti di S(B). ecco cosa ci serve

↓Prendiamo un omomorfismo h ∈ S(B): per le proprietà dell’al-gebra booleana 2 abbiamo che h(xy) = 1 se e solo se h(x) = 1e h(y) = 1. Da questo, usando la definizione di Sxy(B) ottenia-mo la proprietà Sxy(B) = Sx(B) ∩ Sy(B). Inoltre per definizionedi omomorfismo è facile verificare che vale anche la proprietàS1(B) = S(B). Queste due proprietà messe insieme permettonofacilmente di verificare la definizione di base per la collezione{Sx(B) : x ∈ B}.

Mostriamo che ogni insieme della base è un chiusaperto: daciò segue che S(B) è totalmente sconnesso. Dato che ogni tale totale sconnessioneinsieme è aperto per definizione basta mostrare che è anchechiuso, i.e. che è il complementare di un aperto. Questo segueda S(B)− Sx(B) = Sx+1(B), visto che un omomorfismo h fa 1 sux se e solo se fa 0 su x + 1. Dunque S(B) è totalmente sconnesso.

Mostriamo che S(B) è compatto: per farlo useremo la caratte-rizzazione con la proprietà delle intersezioni finite (vedi Munkres[2000], p.169). Dato che ogni chiuso in S(B) è intersezione di caratterizzazione

della compattezzainsiemi in {Sx(B) : x ∈ B} è sufficiente mostrare che:se A1 ⊆ B tale che per ogni {x1, . . . , xn} ⊆ B valga

�ni=1 Sxi(B) �=

∅ allora deve valere�

x∈A1 Sx(B) �= ∅. Per un lemma precedente1

esiste h1 ∈ S(B) con h1(x) = 1, x ∈ A1 tale che h1 appartiene aogni Sx(B), x ∈ A1. Dunque S(B) è compatto.

Mostriamo che ogni G ⊆ S(B) chiusaperto è della forma Sx(B)per qualche x ∈ B. Dato che G è aperto è unione arbitraria dielementi della base. Dato che G è anche chiuso in uno spaziocompatto, G è compatto e dunque basta un numero finito dielementi della base. Abbiamo ottenuto G = Sx1(B) ∪ . . . ∪ Sxn(B)Ora basta dimostrare che ogni unione binaria di elementi dellabase può esser scritta come un unico elemento della base. Perquesto ci serve la seguente proprietà di S(B): denotato il comple-mentare in S(B) con una barra verticale, vale Sx(B) = Sx+1(B).Grazie alle leggi di De Morgan vale leggi di De Morgan

1 Più che un lemma era un’affermazione presente nella prima parte della dimo-strazione. Si può trovare nel libro di Schwart a pagina 42. L’affermazione dice:se B1 ⊆ B tale che 0 /∈ B1 e x, y ∈ B1 ⇒ xy ∈ B1 allora esiste un omomorfismoh1 : B → 2 tale che ∀x ∈ B1 . h1(x) = 1

31

[ 18 settembre 2010 at 15:34 ]

8 La dimostrazione classica del teorema di Stone

Sx(B) ∪ Sy(B) = Sx(B) ∩ Sy(B)

= Sx+1(B) ∩ Sy+1(B)

= S(x+1)(y+1)(B)= S(x+1)(y+1)+1(B)

da cui segue che G è della forma Sx(B) per qualche x ∈ B.

Nei graffiti a lato notiamo i prerequisiti del teorema di Stone:l’uso dei concetti di totale sconnessione, e di una teoria suglispazi topologici in generale, il teorema sulla caratterizzazionedella compattezza e le leggi di De Morgan.

Per iniziare ho caratterizzato la compattezza. Non è statosemplicissimo, mi ha impegnato parecchi giorni ed è emersauna forte dipendenza dalle leggi di De Morgan. Le leggi diDe Morgan sono state implementate strada facendo. Per motividi tempo non sono riuscito a gestire la parte sulla connessione,che ultimerebbe la parte topologica verso il teorema di Stone.Vediamo come ho proceduto.

32

[ 18 settembre 2010 at 15:34 ]

9L A PA RT E T O P O L O G I C A :CARATTERIZZIAMO LA COMPATTEZZA

Tradizionalmente uno spazio topologico X si dice compatto seda ogni suo ricoprimento aperto si riesce ad estrarre un sottori-coprimento finito. Nella dimostrazione di Stone si usa però unacaratterizzazione sulle intersezioni. Riprendiamo un attimo ledefinizioni dal Munkres (Munkres [2000])

Definizione 3: Una collezione C di sottoinsiemi di X è detta averela proprietà delle intersezioni finite (fip dall’inglese Finite Intersec-tion Property) sse per ogni sottocollezione finita {C1, . . . , Cn} di Cl’intersezione C1 ∩ . . . ∩ Cn è non vuota.

Questa definizione porta al seguente teorema

Teorema 3: Sia X una spazio topologico. Allora X è compatto see solo se per ogni collezione C di chiusi in X che hanno la fip vale�

C∈C C �= ∅ fip

Dimostrazione. Data una collezione A di sottoinsiemi di X defi-niamo C = {X− A : A ∈ A}.

Valgono le seguenti affermazioni

• A è una collezione di aperti se e solo se C è una collezionedi chiusi

• la sottocollezione {Ai} di A ricopre A se e solo se l’interse-zione dei corrispettivi elementi Ci = X− Ai è vuota

leggi di De MorganLa prima affermazione segue dalle definizioni, la seconda dallalegge di De Morgan: X− (

�α∈J Aα) =

�α∈J(X− Aα).

Prendendo il contrapositivo della definizione di compattezzaabbiamo: ”X è compatto sse data A collezione di aperti, senessuna sua sottocollezione finita ricopre X allora neanche Aricopre X.

Usando le due affermazioni su quest’ultimo enunciato ottenia-mo la tesi.

Come notiamo immediatamente abbiamo bisogno di un predi-cato che definisca la fip e della definizione di ricoprimento. InRef si traduce così

Def : [Ricoprimento] Covers(C, X) ↔Def

�C = X

Def : [Proprietà intersezioni finite]HasFip(C) ↔Def {D ⊆ C | Finite(D) & D �= ∅ & inters(D) = ∅} = ∅

È interessante notare come abbiamo definito la fip: Ref èbasato sulla teoria degli insiemi per cui gestisce con naturalezzale sostituizioni nei set-former. Riscrivendo la fip come insieme

33

[ 18 settembre 2010 at 15:34 ]

9 La parte topologica: caratterizziamo la compattezza

vuoto aiuteremo il dimostratore quando farà delle sostituzioni divariabili alla ricerca di una contraddizione.

def. tradizionale: ∀D. D ⊆ C finita ⇒ �D �= ∅↓

doppia negazione: ¬(∃D. D ⊆ C ∧D finita∧�D = ∅)↓

def. per insiemi: { D ⊆ C|D finita∧�D = ∅ } = ∅

La definizione di compattezza ricalca invece quella classica

Def : [compattezza] IsCompactΘ(supportΘ) ↔Def

�∀u ⊆ open | Covers(u, supportΘ) → �∃d ⊆ u | Finite(d) & Covers(d, supportΘ)��

Anche un predicato può far parte di una teoria: infatti ilpredicato IsCompactΘ possiede un curioso pedice Θ.

Riportiamo la dimostrazione formale

Theorem topologicalSpace20: [caratterizz. della compattezza]IsCompactΘ(supportΘ)

↔�∀c ⊆ closedΘ | c �= ∅ & HasFip(c) → inters(c) �= ∅�. Proof:Suppose_not ⇒ Auto

Suppose ⇒ IsCompactΘ(supportΘ) &Stat0 : ¬�∀c ⊆ closedΘ | c �= ∅ & HasFip(c) → inters(c) �= ∅�

�c0��→Stat0 ⇒ c0 ⊆ closedΘ & c0 �= ∅ & HasFip(c0) & inters(c0) = ∅Use_def(HasFip) ⇒ Stat1 : {x ⊆ c0 | Finite(x) & x �= ∅ & inters(x) = ∅} = ∅

Use_def(IsCompactΘ) ⇒ Stat2 : �∀u ⊆ open |Covers(u, supportΘ) →�∃d ⊆ u | Finite(d) & Covers(d, supportΘ)��

Loc_def ⇒ Stat22 : u0 = {supportΘ\k : k ∈ c0}

-- c0 = ∅

Suppose ⇒ u0 = ∅�z0��→Stat22 ⇒ false; Discharge ⇒ u0 �= ∅

�c0��→TtopologicalSpace13 ⇒ u0 ⊆ open�u0��→Stat2 ⇒ Covers(u0, supportΘ)→�∃d ⊆ u0 |Finite(d) & Covers(d, supportΘ)�

�c0��→TtopologicalSpace14 ⇒ Covers({supportΘ\k : k ∈ c0} , supportΘ)EQUAL ⇒ Covers(u0, supportΘ)ELEM ⇒ Stat3 : �∃d ⊆ u0 | Finite(d) & Covers(d, supportΘ)�

�d0��→Stat3 ⇒ d0 ⊆ u0 & Finite(d0) & Covers(d0, supportΘ)�d0��→TtopologicalSpace16 ⇒ inters({supportΘ\k : k ∈ d0}) = ∅�d0��→TtopologicalSpace15 ⇒ d0 �= ∅

Loc_def ⇒ Stat4 : k0 = {supportΘ\k : k ∈ d0}EQUAL ⇒ inters(k0) = ∅

Suppose ⇒ k0 = ∅

34

[ 18 settembre 2010 at 15:34 ]

�b0��→Stat4 ⇒ false; Discharge ⇒ k0 �= ∅

-- d0 ⊆ u0 ed u0 ⊆ open

�d0��→TtopologicalSpace11 ⇒ �∀w ∈ d0 | w ⊆ supportΘ��d0��→TtopologicalSpace18 ⇒ Finite({supportΘ\k : k ∈ d0})EQUAL ⇒ Finite(k0)

�d0, u0��→TtopologicalSpace19 ⇒ {supportΘ\k : k ∈ d0} ⊆ {supportΘ\k : k ∈ u0}EQUAL ⇒ k0 ⊆ {supportΘ\k : k ∈ u0}EQUAL ⇒ k0 ⊆ {supportΘ\k : k ∈ {supportΘ\k : k ∈ c0}}SIMPLF ⇒ k0 ⊆ {supportΘ\(supportΘ\k) : k ∈ c0}

-- c0 ⊆ closedΘ

�c0��→TtopologicalSpace11 ⇒ �∀w ∈ c0 | w ⊆ supportΘ��c0��→TtopologicalSpace17 ⇒ k0 ⊆ c0

�k0��→Stat1 ⇒ false;

Discharge ⇒ ¬IsCompactΘ(supportΘ) &Stat5 : �∀c ⊆ closedΘ | c �= ∅ & HasFip(c) → inters(c) �= ∅�

Use_def(IsCompactΘ) ⇒Stat6 : ¬�∀u ⊆ open | Covers(u, supportΘ) → �∃d ⊆ u | Finite(d) & Covers(d, supportΘ)��

�u1��→Stat6 ⇒u1 ⊆ open & Covers(u1, supportΘ) & ¬�∃d ⊆ u1 | Finite(d) & Covers(d, supportΘ)�

Loc_def ⇒ Stat7 : c1 = {supportΘ\k : k ∈ u1}�u1��→TtopologicalSpace12 ⇒ {supportΘ\k : k ∈ u1} ⊆ closedΘEQUAL ⇒ c1 ⊆ closedΘ

�u1��→TtopologicalSpace15 ⇒ u1 �= ∅Suppose ⇒ c1 = ∅�b1��→Stat7 ⇒ false; Discharge ⇒ c1 �= ∅

�c1��→Stat5 ⇒ HasFip(c1)→ inters(c1) �= ∅ELEM ⇒ inters(c1) = ∅→¬HasFip(c1)�u1��→TtopologicalSpace16 ⇒ inters({supportΘ\k : k ∈ u1}) = ∅EQUAL ⇒ ¬HasFip(c1)

Use_def(HasFip) ⇒ Stat8 : {x ⊆ c1 | Finite(x) & x �= ∅ & inters(x) = ∅} �= ∅ELEM ⇒ Stat9 : ¬�∃d ⊆ u1 |Finite(d) & Covers(d, supportΘ)��x1��→Stat8 ⇒ x1 ⊆ c1 & Finite(x1) & x1 �= ∅ & inters(x1) = ∅

Loc_def ⇒ Stat10 : d1 = {supportΘ\k : k ∈ x1}

ELEM ⇒ x1 ⊆ c1�x1, c1��→TtopologicalSpace19 ⇒ {supportΘ\k : k ∈ x1} ⊆ {supportΘ\k : k ∈ c1}EQUAL ⇒ d1 ⊆ {supportΘ\k : k ∈ {supportΘ\k : k ∈ u1}}SIMPLF ⇒ {supportΘ\k : k ∈ {supportΘ\k : k ∈ u1}} = {supportΘ\(supportΘ\k) : k ∈ u1}

-- u1 ⊆ open

�u1��→TtopologicalSpace11 ⇒ �∀w ∈ u1 | w ⊆ supportΘ��u1��→TtopologicalSpace17 ⇒ {supportΘ\k : k ∈ {supportΘ\k : k ∈ u1}} = u1

35

[ 18 settembre 2010 at 15:34 ]


EQUAL ⇒ d1 ⊆ u1

-- c1 ⊆ closedΘ x1 ⊆ c1

�x1��→TtopologicalSpace11 ⇒ �∀w ∈ x1 | w ⊆ supportΘ��x1��→TtopologicalSpace18 ⇒ Finite({supportΘ\k : k ∈ x1})EQUAL ⇒ Finite(d1)

�x1��→TtopologicalSpace14 ⇒ Covers({supportΘ\k : k ∈ x1} , supportΘ)EQUAL ⇒ Covers(d1, supportΘ)

�d1��→Stat9 ⇒ false;

Discharge ⇒ Qed

La dimostrazione formale a differenza di quella classica dividel’implicazione in due parti. Questa scelta è dovuta a leggereasimmetrie.

Ad esempio una collezione vuota U non può ricoprire il sup-porto (teorema topologicalSpace15) ma cosa si può dire dell’inter-sezione di una collezione vuota C?il problema di

�∅

Nella dimostrazione vista sopra la collezione C era formataprendendo i complementari degli insiemi di U , dunque se U eravuota anche C lo era. Ma mentre l’unionset di una collezionevuota è facile da definire (se andiamo a vedere la definizione diUn data in precedenza si vede che è vuoto), l’intersezione è piùproblematica.

Nella topologia generale l’intersezione vuota viene posta perdefinizione uguale al supporto. Questo prevede che ci sia un in-sieme “grande” dal quale partire, una specie di insieme universo.Un insieme universo funziona bene in un ambito ristretto qualela topologia, ma Ref si occupa di tutta la teoria degli insiemi enella teoria degli insiemi un insieme universo è un problema.

Il problema nasce dal paradosso del barbiere, enunciato daRussel nel 1918. Sia U l’insieme universo e R = {X ∈ U : X �∈ X},vale R ∈ R? In un linguaggio più pittoresco ci si chiede: ”In unvillaggio c’è un unico barbiere. Il barbiere rade tutti (e solo) gliuomini che non si radono da sé. Chi rade il barbiere?” Questafrase porta inevitabilmente a una contraddizione che escludel’esistenza dell’insieme universo.

Per la nostra dimostrazione è un problema. Vediamo comepossiamo risolverlo. L’intersezione arbitraria l’abbiamo definitacosì, non essendo un operatore built-in di Ref

Def : [Intersezione unaria]inters(C) ↔Def

�z ∈ arb(C) | �∀y ∈ C | z ∈ y�

�

Con questa definizione l’intersezione di una collezione vuotaè vuota. Infatti arb è una funzione predefinita che sceglie unelemento di un insieme, ma se l’insieme di partenza è vuototorna vuoto. Partendo da una C = ∅ otteniamo che non ci sonoz ∈ arb(C) e anche l’intersezione risulta vuota. Ora, se entrambeU e C sono vuote, la prima non ricopre X ma la seconda ha

36

[ 18 settembre 2010 at 15:34 ]

9.1 Le leggi di De Morgan

intersezione vuota. Ma questo va contro la prima affermazionedella dimostrazione del teorema della compattezza!

Come possiamo dimostrare l’enunciato formalmente allora?Gestendo con dei condizionali il caso dell’intersezione vuota. Iltutto si traduce nell’aggiungere una serie di ipotesi nel lemmiprecedenti e in un condizionale if. . .then. . .else nelle leggi di DeMorgan.

Per la parte restante la dimostrazione ricalca quella standard,solamente è specificato ogni dettaglio. Per questioni di stileho diviso la dimostrazione in blocchi: l’ultima riga mostra laconclusione a cui si voleva arrivare, di solito per citare un lemmao un teorema.

9.1 le leggi di de morgan

La caratterizzazione della compattezza che abbiamo visto usainevitabilmente la seconda legge di De Morgan. Ci si potrebbestupire che Ref non includa dei teoremi così basilari, ma pen-sandoci un attimo ci si rende conto che non è poi così stranodato che non erano definite nemmeno le unioni e le intersezioniarbitrarie d’insiemi.

La maggior difficoltà con le leggi di De Morgan è gestire l’in-tersezione vuota. Abbiamo già parlato del problema quindi cilimiteremo a riportare la dimostrazione formale. Come si vedeabbiamo usato un condizionale if. . . then. . . else.

Theorem 23a: [seconda legge di De Morgan]X\�

Y = if Y = ∅ then X else�

({X\z : z ∈ Y}) fi. Proof:Suppose_not(x0, y0) ⇒ Auto

-- Ragionando per assurdo, cominciamo semplificandoil lato destro della disuguaglianza e con l’escludere lapossibilità che il controesempio x0, y0 possa avere y0 = ∅.Da ciò segue subito che {x0\z : z ∈ y0} �= ∅.

�y0��→T3 f ⇒ y0 �= ∅ & Stat1 : x0\�

y0 �=�

({x0\z : z ∈ y0})Suppose ⇒ Stat2 : {x0\z : z ∈ y0} = ∅�arb(y0) ��→Stat2 ⇒ false; Discharge ⇒ Auto

-- Richiamando la prima legge di De Morgan, troviamoche x0 ∩

�({x0\z : z ∈ y0}) = x0\

� {x0 ∩ z : z ∈ y0}.

�x0, {x0\z : z ∈ y0} ��→T23 ⇒ x0 ∩�

({x0\z : z ∈ y0}) =x0\

� {x0\z : z ∈ {x0\z : z ∈ y0}}SIMPLF ⇒ {x0\z : z ∈ {x0\z : z ∈ y0}} = {x0\(x0\z) : z ∈ y0}Suppose ⇒ Stat3 : {x0\(x0\z) : z ∈ y0} �= {x0 ∩ z : z ∈ y0}�c0��→Stat3(Stat3�) ⇒ false;Discharge ⇒ {x0\(x0\z) : z ∈ y0} = {x0 ∩ z : z ∈ y0}�x0, y0��→T3h ⇒ x0\

� {x0 ∩ z : z ∈ y0} = x0\�

y0EQUAL ⇒ x0 ∩

�({x0\z : z ∈ y0}) = x0\

�y0

-- Il lato sinistro di quest‘ultima uguaglianza si sempli-fica in inters ({x0-z: z in y0}), il che contraddice il passoStat1.

37

[ 18 settembre 2010 at 15:34 ]


Suppose ⇒ Stat4 :�

({x0\z : z ∈ y0}) �⊆ x0 ∩�

({x0\z : z ∈ y0})�c1��→Stat4(Stat4�) ⇒

Stat5 : c1 ∈�

({x0\z : z ∈ y0}) & c1 /∈ x0Use_def (

�) ⇒Stat6 : c1 ∈

�z ∈ arb({x0\z : z ∈ y0}) | �∀y ∈ {x0\z : z ∈ y0} | z ∈ y�

�

Loc_def ⇒ a = arb({x0\z : z ∈ y0})� ��→Stat6(Stat6) ⇒ Stat7 : a ∈ {x0\z : z ∈ y0} & c1 ∈ a�z0��→Stat7(Stat5, Stat7�) ⇒ false; Discharge ⇒ falseDischarge ⇒ Qed

La dimostrazione cita due teoremi: il 3f e il3h. I teoremi sonodelle leggi di distribitutività dell’unione arbitraria, prima rispettola differenza e poi rispetto all’intersezione.

Theorem 3 f : (Y ⊆ {∅} ↔ �Y = ∅) &

�Y ∈ Z → �

Z = Y ∪�

(Z\ {Y})�.

Theorem 3h:� {X ∩ z : z ∈ Y} = X ∩

�Y.

38

[ 18 settembre 2010 at 15:34 ]

10R I S U LTAT I F I N A L I E S V I L U P P I F U T U R I . . .

Siamo in conclusione del lavoro: cosa abbiamo ottenuto e cosaresta da fare? cosa abbiamo

ottenuto. . .L’obiettivo finale era creare uno scenario indipendente in Refche includesse un risultato non banale. Il risultato che abbiamoscelto è il teorema di rappresentazione di Stone. Questo teoremaha il pregio di essere un risultato non puramente insiemistico,cioè mostra come Ref possa essere usato in contesti al di fuoridalla teoria degli insiemi, ma allo stesso tempo non richiedegrandi prerequisiti, come la costruzione dei reali in un teoremad’analisi.

In questa ottica abbiamo ripreso in mano le teorie delle al-gebre booleane sviluppate precedentemente e abbiamo inizia-to a sviluppare il primo concetto topologico che ci serviva: lacompattezza.

In particolare, riprendendo la dimostrazione di Schwartz, èrisultato fondamentale darne una caratterizzazione alternativa.Questa caratterizzazione utilizza insiemi chiusi invece che apertiperché la base dello spazio Stone si comporta bene rispetto alleintersezioni, cioè vale Sxy(B) = Sx(B) ∩ Sy(B).

Per dimostrare questa caratterizzazioni abbiamo definito deglioperatori su unioni e intersezioni arbitrarie e quindi dimostratole leggi di De Morgan e di altri lemmi insiemistici. . . . cosa resta da fare

Cosa manca ora? Come accennato nel capitolo apposito bi-sogna integrare la teoria degli spazi topologici con i concetti diconnessione e di spazio di Hausdorff. L’integrazione dovrebbeessere fatta modellando i concetti di connessione e spazio diHausdorff su predicati come IsCompactΘ. Ottenuti questi duepredicati avremo bisogno di alcuni lemmi, come il fatto che unospazio di Hausdorff compatto con una base di chiusaperti siaautomaticamente totalmente sconnesso.

Dimostrati tutti i lemmi che ci servono e integrati nella teoriatopologicalSpace potremmo finalmente finire la dimostrazionedel teorema di Stone.

39

[ 18 settembre 2010 at 15:34 ]

[ 18 settembre 2010 at 15:34 ]

B I B L I O G R A F I A

Dunford, N. e Schwartz, J. T. (1958), Linear Operators, Part IGeneral Theory, Interscience Publishers. (Citato alle pagine 29e 31.)

Euclide (2010), «Gli elementi di Euclide, Libro I», URLhttp://aleph0.clarku.edu/~djoyce/java/elements/bookI/propI1.html, online, controllata in settembre 2010. (Citato apagina 5.)

Geuvers, H. (2009), «Proof assistants: History, ideas and future»,Sadhana Journal, vol. 34. (Citato a pagina 12.)

Gonthier, G. (2008), «Formal Proof—The Four-Color Theorem»,Notices of the AMS, vol. 55 (11). (Citato a pagina 9.)

Hales, T. C. (2008), «Formal Proof», Notices of the AMS,vol. 55 (11). (Citato a pagina 15.)

Krantz, S. G. (2007), The Proof is in the Pudding. The ChangingNature of Mathematical Proof, Springer. (Citato a pagina 8.)

Munkres, J. (2000), Topology (2nd edition), Prentice Hall. (Citatoalle pagine 31 e 33.)

Omodeo, E. G., Cantone, D., Policriti, A. e Schwartz, J. T.(2006), «A Computerized Referee», in Stock, O. e Schaerf, M.,curatori, «Reasoning, Action and Interaction in AI Theoriesand Systems — Essays Dedicated to Luigia Carlucci Aiello»,vol. 4155, p. 117–139, Springer. (Citato a pagina 17.)

Stone, M. H. (1936), «The Theory of Representations of BooleanAlgebras», Transactions of the American Mathematical Society,(40), p. 37–111. (Citato a pagina 5.)

Whitehead, A. N. e Russell, B. (2009), Principia Matematica, vol.1–3, Merchant Books. (Citato a pagina 7.)

Wiedijk, F. (2007), «The QED Manifesto Revisisted», STUDIESIN LOGIC, GRAMMAR AND RHETORIC 10 (23). (Citato apagina 13.)

Wiedijk, F. (2010), «Formalizing 100 Theorems», URL http://www.cs.ru.nl/~freek/100/. (Citato a pagina 14.)

41

[ 18 settembre 2010 at 15:34 ]

http://aleph0.clarku.edu/~djoyce/java/elements/bookI/propI1.html

http://aleph0.clarku.edu/~djoyce/java/elements/bookI/propI1.html

http://www.cs.ru.nl/~freek/100/

http://www.cs.ru.nl/~freek/100/

Theorem 1a. S ⊇ X → PX ∪ {∅,X} ⊆ PS. Proof:Suppose not(s0, x0) ⇒ AutoSet monot ⇒ {x : x ⊆ x0} ⊆ {x : x ⊆ s0}Use def (P) ⇒ Stat1 : ∅ /∈ {x : x ⊆ s0} ∨ x0 /∈ {x : x ⊆ s0}�∅, x0��→Stat1 ⇒ false; Discharge ⇒ Qed

Theorem 1b. P∅= {∅} & P {X} = {∅, {X}} . Proof:Suppose not(x0) ⇒ AutoSuppose ⇒ P∅ �= {∅}�∅, ∅��→T1a ⇒ Stat0 : P∅ �⊆ {∅}�y0��→Stat0(Stat0�) ⇒ Stat1 : y0 ∈ P∅ & y0 /∈ {∅}�∅, y0��→T1 (Stat1�) ⇒ false; Discharge ⇒ P {x0} �= {∅, {x0}}� {x0} , {x0} ��→T1a ⇒ Stat2 : P {x0} �⊆ {∅, {x0}}�y1��→Stat2 ⇒ Stat3 : y1 ∈ P {x0} & y1 /∈ {∅, {x0}}� {x0} , y1��→T1 (Stat3�) ⇒ false; Discharge ⇒ Qed

Theorem 3a. Z = {X,Y}→�

Z = X ∪ Y &�

{Y} = Y. Proof:Suppose not(z0, x0, y0) ⇒ Auto

-- La seconda parte dell’enunciato di questo teorema discende direttamente dalla prima epotremmo posporne la dimostrazione; preferiamo invece trattare per primo questo casospeciale per illustrare una linea dimostrativa lievemente diversa e piu semplice.

Suppose ⇒�

{y0} �= y0

Use def (S

) ⇒ {z : y ∈ {y0} , z ∈ y} �= y0

SIMPLF ⇒ {z : z ∈ y0} �= y0

ELEM ⇒ false; Discharge ⇒ Stat0 : z0 = {x0, y0} &�

z0 �= x0 ∪ y0

-- Nell’altro caso, cioe sotto l’assurda ipotesi che z0 = {x0, y0} &�

z0 �= x0 ∪ y0, duecitazioni del Theorem 3 ci pemettono di ricavare da z0 = {x0, y0} che x0 ⊆

�z0 ed

y0 ⊆�

z0

�x0, z0��→T3 ⇒ Auto�y0, z0��→T3 ⇒ Auto

-- Una terza citazione dello stesso Theorem 3 ci permette di ricavare da�

z0 �= x0 ∪ y0 chequalche elemento di z0 = {x0, y0} non e incluso in x0 ∪ y0, il che e palesemente assurdo.

�x0 ∪ y0, z0��→T3 (Stat0�) ⇒ Stat1 : ¬�∀y ∈ z0 | y ⊆ x0 ∪ y0��v��→Stat1(Stat0,Stat0�) ⇒ v ∈ {x0, y0} & v �⊆ x0 ∪ y0

(Stat1�)Discharge ⇒ Qed

Theory imageOfDoubleton�f(X), x0, x1

�

End imageOfDoubleton

Enter theory imageOfDoubleton

-- the image of a doubleton is a doubleton or singletonTheorem imageOfDoubleton. {f(v) : v ∈ ∅} = ∅ & {f(v) : v ∈ {x0}} = {f} (x0) & {f(v) : v ∈ {x0, x1}} = {f(x0), f(x1)} . Proof:

Suppose not() ⇒ AutoSIMPLF ⇒ Stat1 : {f(v) : v ∈ {x0, x1}} �= {f(x0), f(x1)}�c��→Stat1(Stat1�) ⇒ c ∈ {f(v) : v ∈ {x0, x1}} �= c ∈ {f(x0), f(x1)}Suppose ⇒ Stat2 : c /∈ {f(v) : v ∈ {x0, x1}}�x0��→Stat2(Stat1�) ⇒ c = f(x1)�x1��→Stat2(Stat1�) ⇒ false; Discharge ⇒ Stat3 : c ∈ {f(v) : v ∈ {x0, x1}} & c /∈ {f(x0), f(x1)}�x��→Stat3 ⇒ x� ∈ {x0, x1} & f(x�) /∈ {f(x0), f(x1)}Suppose ⇒ x� = x0

EQUAL ⇒ f(x0) /∈ {f(x0), f(x1)}(Stat3�)Discharge ⇒ x� = x1

EQUAL ⇒ Stat4 : f(x1) /∈ {f(x0), f(x1)}(Stat4�)Discharge ⇒ Qed

Enter theory Set theory

-- unione di unioneTheorem 3b.

�(�

X) =�

{�

y : y ∈ X} . Proof:Suppose not(x0) ⇒ AutoUse def (

S) ⇒ {z : y ∈ {u : v ∈ x0, u ∈ v} , z ∈ y} �= {s : r ∈ {

�y : y ∈ x0} , s ∈ r}

SIMPLF ⇒ Stat1 : {z : v ∈ x0, u ∈ v, z ∈ u} �= {s : y ∈ x0, s ∈�

y}�z0��→Stat1 ⇒ Stat2 : z0 ∈ {z : v ∈ x0, u ∈ v, z ∈ u} �= z0 ∈ {s : y ∈ x0, s ∈

�y}

Suppose ⇒ Stat3 : z0 ∈ {z : v ∈ x0, u ∈ v, z ∈ u} & z0 /∈ {s : y ∈ x0, s ∈�

y}Use def (

Sv0) ⇒ Auto

�v0, u0, z, v0, z0��→Stat3(Stat2�) ⇒ Stat4 :z0 /∈ {z : u ∈ v0, z ∈ u} & v0 ∈ x0 & u0 ∈ v0 & z0 ∈ u0

�u0, z0��→Stat4(Stat4�) ⇒ false; Discharge ⇒ Stat5 : z0 ∈ {s : y ∈ x0, s ∈�

y}Use def (

Sy0) ⇒ Auto

�y0, s0��→Stat5(Stat5�) ⇒ Stat6 : z0 ∈ {s : u ∈ y0, s ∈ u} & y0 ∈ x0

�u1, s1��→Stat6(Stat5,Stat2�) ⇒ Stat7 : z0 /∈ {z : v ∈ x0, u ∈ v, z ∈ u} & z0 ∈ u1 & u1 ∈ y0

�y0, u1, z0��→Stat7(Stat6�) ⇒ false; Discharge ⇒ Qed

-- additivita e monotonicita dell’unione monadicaTheorem 3c.

�(X ∪ Y) =

�X ∪

�Y & (Y ⊇ X →

�Y ⊇

�X). Proof:

Suppose not(x0, y0) ⇒ AutoSuppose ⇒

�(x0 ∪ y0) �=

�x0 ∪

�y0

� {x0, y0} ��→T3b ⇒�

(�

{x0, y0}) =�

{�

v : v ∈ {x0, y0}}APPLY � � imageOfDoubleton

`f(X) �→

SX, x0 �→ x0, x1 �→ y0

´⇒

{�

v : v ∈ {x0, y0}} = {�

x0,�

y0}� {x0, y0} , x0, y0��→T3a ⇒

�{x0, y0} = x0 ∪ y0

� {Sx0,

Sy0} ,

Sx0,

Sy0��→T3a ⇒

�{�

x0,�

y0} =�

x0 ∪�

y0

EQUAL ⇒ false; Discharge ⇒�

(x0 ∪ y0) =�

x0 ∪�

y0 & y0 = x0 ∪ y0 &�

y0 �⊇�

x0

EQUAL ⇒�

y0 =�

x0 ∪�

y0

Discharge ⇒ Qed

-- Anche se puo apparire inutilmente contorto, l’enunciato del teorema che segue ha ilpregio della versatilita ; visto che, per semplice citazione, puo essere utilmente declinatoin almeno tre modi: �

(X ∪ {Y}) = Y ∪�

X ,

Y ∈ Z →�

Z = Y ∪�

(Z\ {Y}) ,

Z �= ∅ →�

Z = arb(Z) ∪�

(Z\ {arb(Z)}) .

-- unione di unione, 2Theorem 3d. Y ∈ Z & X ∈ {Z,Z\ {Y}}→

�Z = Y ∪

�X. Proof:

Suppose not(y0, z0, x0) ⇒ AutoELEM ⇒ z0 = x0 ∪ {y0}EQUAL ⇒

�(x0 ∪ {y0}) �= y0 ∪

�x0

�∅, ∅, y0��→T3a ⇒ Auto�x0, {y0} ��→T3c ⇒ false; Discharge ⇒ Qed

Theorem 3e.�

(X ∪ {Y}) = Y ∪�

X. Proof:Suppose not(x0, y0) ⇒ Auto�y0, x0 ∪ {y0} , x0��→T3d (�) ⇒ false; Discharge ⇒ Qed

Theorem 3f. (Y ⊆ {∅} ↔�

Y = ∅) &�Y ∈ Z →

�Z = Y ∪

�(Z\ {Y})

�. Proof:

Suppose not(x0, z0) ⇒ AutoSuppose ⇒ x0 ⊆ {∅} �=

�x0 = ∅

Use def (S

x0) ⇒ AutoSuppose ⇒ x0 ⊆ {∅}ELEM ⇒ Stat1 : {z : y ∈ x0, z ∈ y} �= ∅�y0, z1��→Stat1 ⇒ false; Discharge ⇒ Stat2 : x0 �⊆ {∅} & {z : y ∈ x0, z ∈ y} = ∅

�y1, y1,arb(y1) ��→Stat2 ⇒ false; Discharge ⇒ x0 ∈ z0 &�

z0 �= x0 ∪�

(z0\ {x0})�x0, z0, z0\ {x0} ��→T3d (�) ⇒ false; Discharge ⇒ Qed

Theorem 3g. Z �= ∅→�

Z = arb(Z) ∪�

(Z\ {arb(Z)}). Proof:Suppose not(z0) ⇒ Auto�arb(z0) , z0, z0\ {arb(z0)} ��→T3d ⇒ false; Discharge ⇒ Qed

Theory doubleUnion�f(X), x0

�

End doubleUnion

Enter theory doubleUnion

-- double union of a setformerTheorem doubleUnion.

��{f(w) : w ∈ x0}

�=

�{�

f(w) : w ∈ x0} . Proof:Suppose not() ⇒ Auto� {f(w) : w ∈ x0} ��→T3b ⇒

�{�

v : v ∈ {f(w) : w ∈ x0}} �=�

{�

f(w) : w ∈ x0}SIMPLF ⇒ false; Discharge ⇒ Qed


-- distributivita dell’intersezione sull’unioneTheorem 3h.

�{X ∩ z : z ∈ Y} = X ∩

�Y. Proof:

Suppose not(x0, y0) ⇒ Stat0 : Auto�c1��→Stat0 ⇒ c1 ∈

�{x0 ∩ z : z ∈ y0} �= c1 ∈ x0 ∩

�y0

Use def (S

{x0 ∩ z : z ∈ y0}) ⇒ AutoSIMPLF ⇒

�{x0 ∩ z : z ∈ y0} = {w : z ∈ y0,w ∈ x0 ∩ z}

Use def (S

y0) ⇒ AutoSuppose ⇒ Stat1 : c1 ∈ {w : z ∈ y0,w ∈ x0 ∩ z} & c1 /∈ x0 ∩

�y0

�z1, w��→Stat1 ⇒ c1 ∈ x0 ∩ z1 & z1 ∈ y0 & Stat3 : c1 /∈ {w : y ∈ y0,w ∈ y}�z1, c1��→Stat3 ⇒ false; Discharge ⇒ Stat5 : c1 ∈ {w : y ∈ y0,w ∈ y} & c1 ∈ x0 & c1 /∈

�{x0 ∩ z : z ∈ y0}

�y2, c��→Stat5 ⇒ c1 ∈ x0 & c1 ∈ y2 & y2 ∈ y0 & Stat6 : c1 /∈ {w : z ∈ y0,w ∈ x0 ∩ z}�y2, c1��→Stat6 ⇒ false; Discharge ⇒ Qed

-- intersezione monadicaDef intersection.

�(X) =Def

�z ∈ arb(X) | �∀y ∈ X | z ∈ y��

-- prima legge di De MorganTheorem 23. X\if Y = ∅ then X else

�(Y) fi =

�{X\z : z ∈ Y} . Proof:

Suppose not(x0, y0) ⇒ Auto

-- Ragionando per assurdo, cominciamo semplificando il lato destro della disuguaglianzae con l’escludere la possibilita che il controesempio x0, y0 possa avere y0 = ∅.

Use def (S

{x0\z : z ∈ y0}) ⇒ AutoSIMPLF ⇒

�{x0\z : z ∈ y0} = {z : w ∈ y0, z ∈ x0\w}

Loc def ⇒ w1 = arb(y0)Suppose ⇒ y0 = ∅� {x0\z : z ∈ y0} ��→T3f ⇒ Stat1 : {x0\z : z ∈ y0} �= ∅�z1��→Stat1 ⇒ false; Discharge ⇒ Stat2 : x0\

�(y0) �= {z : w ∈ y0, z ∈ x0\w} & w1 ∈ y0

-- Escluso quel caso banale, l’assurda ipotesi si e ridotta alla disuguaglianza che leggiamoqui sopra. Sia e0 un elemento che differenzia i due membri della disuguaglianza.

�e0��→Stat2 ⇒ e0 ∈ x0\�

(y0) �= e0 ∈ {z : w ∈ y0, z ∈ x0\w}Use def

`T(y0)

´⇒ Auto

-- Se e0 appartiene al primo membro (e dunque non al secondo), allora e chiaro che deveappartenere a un generico elemento w1 di y0 . . .

Suppose ⇒ e0 ∈ x0\�

(y0)(Stat2�)ELEM ⇒ Stat3 : e0 /∈

�z ∈ arb(y0) | �∀y ∈ y0 | z ∈ y�� & e0 ∈ x0 & Stat4 : e0 /∈ {z : w ∈ y0, z ∈ x0\w}

Suppose ⇒ e0 /∈ w1

�w1, e0��→Stat4(Stat2�) ⇒ false; Discharge ⇒ Auto

-- . . .ma di qui a una contraddizione il passo e breve.

�w1��→Stat3 ⇒ Stat5 : ¬�∀w ∈ y0 | e0 ∈ w��w2��→Stat5 ⇒ w2 ∈ y0 & e0 /∈ w2

�w2, e0��→Stat4 ⇒ false; Discharge ⇒ Stat6 : e0 ∈ {z : w ∈ y0, z ∈ x0\w} & e0 /∈ x0\�

(y0)

-- Consideriamo ora l’altro caso, che e0 appartenga al secondo membro ma non al primo.Di nuovo giungeremo a una contraddizione, col che la dimostrazione sara completa.

�w0, z0��→Stat6 ⇒ Stat7 : e0 ∈�z ∈ arb(y0) | �∀y ∈ y0 | z ∈ y�� & w0 ∈ y0 & e0 ∈ x0\w0

� ��→Stat7 ⇒ Stat8 : �∀y ∈ y0 | e0 ∈ y��w0��→Stat8(Stat7�) ⇒ false; Discharge ⇒ Qed

-- seconda legge di De MorganTheorem 23a. X\

�Y = if Y = ∅ then X else

�({X\z : z ∈ Y}) fi. Proof:


-- Ragionando per assurdo, cominciamo semplificando il lato destro della disuguaglianzae con l’escludere la possibilita che il controesempio x0, y0 possa avere y0 = ∅. Da cio seguesubito che {x0\z : z ∈ y0} �= ∅.

�y0��→T3f ⇒ y0 �= ∅ & Stat1 : x0\�

y0 �=�

({x0\z : z ∈ y0})Suppose ⇒ Stat2 : {x0\z : z ∈ y0} = ∅�arb(y0) ��→Stat2 ⇒ false; Discharge ⇒ Auto

-- Richiamando la prima legge di De Morgan, troviamo chex0 ∩

�({x0\z : z ∈ y0}) = x0\

�{x0 ∩ z : z ∈ y0}.

�x0, {x0\z : z ∈ y0} ��→T23 ⇒ x0 ∩�

({x0\z : z ∈ y0}) =x0\

�{x0\z : z ∈ {x0\z : z ∈ y0}}

SIMPLF ⇒ {x0\z : z ∈ {x0\z : z ∈ y0}} = {x0\(x0\z) : z ∈ y0}Suppose ⇒ Stat3 : {x0\(x0\z) : z ∈ y0} �= {x0 ∩ z : z ∈ y0}�c0��→Stat3(Stat3�) ⇒ false; Discharge ⇒ {x0\(x0\z) : z ∈ y0} = {x0 ∩ z : z ∈ y0}�x0, y0��→T3h ⇒ x0\

�{x0 ∩ z : z ∈ y0} = x0\

�y0

EQUAL ⇒ x0 ∩�

({x0\z : z ∈ y0}) = x0\�

y0

-- Il lato sinistro di quest‘ultima uguaglianza si semplifica in inters ({x0-z: z in y0}), ilche contraddice il passo Stat1.


({x0\z : z ∈ y0}) �⊆ x0 ∩�

({x0\z : z ∈ y0})�c1��→Stat4(Stat4�) ⇒ Stat5 : c1 ∈

�({x0\z : z ∈ y0}) & c1 /∈ x0

Use def (T

) ⇒ Stat6 : c1 ∈�z ∈ arb({x0\z : z ∈ y0}) | �∀y ∈ {x0\z : z ∈ y0} | z ∈ y��

Loc def ⇒ a = arb({x0\z : z ∈ y0})� ��→Stat6(Stat6) ⇒ Stat7 : a ∈ {x0\z : z ∈ y0} & c1 ∈ a�z0��→Stat7(Stat5,Stat7�) ⇒ false; Discharge ⇒ falseDischarge ⇒ Qed

Theorem 23b.�

(X) = if X ⊆ {arb(X)} then arb(X) else arb(X) ∩�

(X\ {arb(X)}) fi. Proof:Suppose not(x0) ⇒ AutoUse def

`T(x0)

´⇒ Auto

Suppose ⇒ x0 = ∅ELEM ⇒ arb(x0) = ∅ &

�z ∈ ∅ | �∀y ∈ x0 | z ∈ y�� = ∅ &

�(x0) �= ∅

EQUAL ⇒ false; Discharge ⇒ AutoSuppose ⇒ Stat1 : x0 = {arb(x0)}ELEM ⇒ Stat2 :

�z : z ∈ arb(x0) | �∀y ∈ x0 | z ∈ y�� = {z : z ∈ arb(x0)}

�e��→Stat2(Stat2�) ⇒ �∀y ∈ x0 | e ∈ y� �= e ∈ arb(x0)Suppose ⇒ Stat3 : ¬�∀y ∈ x0 | e ∈ y��y��→Stat3(Stat1�) ⇒ false; Discharge ⇒ Stat4 : �∀y ∈ x0 | e ∈ y� & e /∈ arb(x0)

�arb(x0) ��→Stat4(Stat1�) ⇒ false; Discharge ⇒ Stat0 : arb(x0\ {arb(x0)}) ∈ x0\ {arb(x0)} & arb(x0) ∩�

(x0\ {arb(x0)}) �=�

(x0)Use def

`T(x0\ {arb(x0)})

´⇒ Auto


(x0) �⊆ arb(x0) ∩�

(x0\ {arb(x0)})�z0��→Stat5 ⇒ Stat6 : z0 ∈

�z ∈ arb(x0) | �∀y ∈ x0 | z ∈ y�� & z0 /∈ arb(x0) ∩

�(x0\ {arb(x0)})

� ��→Stat6 ⇒ Stat7 : �∀y ∈ x0 | z0 ∈ y� & z0 /∈�

(x0\ {arb(x0)})�arb(x0\ {arb(x0)}) ��→Stat7(Stat0�) ⇒ Stat8 :

z0 /∈�z ∈ arb(x0\ {arb(x0)}) | �∀y ∈ x0\ {arb(x0)} | z ∈ y�� & z0 ∈ arb(x0\ {arb(x0)})

�z0��→Stat8(Stat8�) ⇒ Stat9 : ¬�∀y ∈ x0\ {arb(x0)} | z0 ∈ y��w2��→Stat9 ⇒ w2 ∈ x0\ {arb(x0)} & z0 /∈ w2

�w2��→Stat7(Stat5�) ⇒ false; Discharge ⇒ Stat10 : arb(x0) ∩�

(x0\ {arb(x0)}) �⊆�

(x0)�z1��→Stat10 ⇒ Stat11 : z1 /∈

�z ∈ arb(x0) | �∀y ∈ x0 | z ∈ y�� & z1 ∈ arb(x0) ∩

�(x0\ {arb(x0)})

�w3��→Stat11(Stat11�) ⇒ Stat12 : ¬�∀y ∈ x0 | z1 ∈ y��y0��→Stat12(Stat12�) ⇒ y0 ∈ x0 & z1 /∈ y0

(Stat0�)ELEM ⇒ Stat13 : z1 ∈�z ∈ arb(x0\ {arb(x0)}) | �∀y ∈ x0\ {arb(x0)} | z ∈ y��

� ��→Stat13 ⇒ Stat14 : �∀y ∈ x0\ {arb(x0)} | z1 ∈ y��y0��→Stat14(Stat0�) ⇒ false; Discharge ⇒ Qed

-- Tradizionalmente, la finitezza viene definita a partire dalla nozione di cardinalita diun insieme: un insieme e finito se la sua cardinalita precede il primo ordinale limite.Come scorciatoia, per poter giungere senza troppo lavoro a un’accettabile elaborazioneformale della finitezza, adottiamo qui la seguente definizione (ispirata dall’articolo “Surles ensembles fini” di Tarski, 1924): un insieme e finito se ogni famiglia non vuota di suoisottoinsiemi possiede un elemento minimale rispetto all’inclusione. Per esprimere questoconcetto succintamente, ci conviene sfruttare l’operatore di ‘insieme potenza’ definitoall’inizio.-- proprieta di finitezza

Def Fin. Finite(X) ↔Def �∀g ∈ P(PX)\ {∅} ,∃m | g ∩ Pm = {m} �

-- monotonicita della finitezzaTheorem 25. Y ⊇ X & Finite(Y)→ Finite(X). Proof:

Suppose not(y0, x0) ⇒ Auto�y0, x0��→T1a (�) ⇒ Py0 ⊇ Px0

Use def (Finite) ⇒ Stat1 : ¬�∀g ∈ P(Px0)\ {∅} ,∃m | g ∩ Pm = {m} � & �∀g� ∈ P(Py0)\ {∅} ,∃m | g� ∩ Pm = {m} ��Py0, Px0��→T1a (�) ⇒ P(Py0) ⊇ P(Px0)�g0, g0��→Stat1(Stat1�) ⇒ ¬�∃m | g0 ∩ Pm = {m} � & �∃m | g0 ∩ Pm = {m} �Discharge ⇒ Qed

-- finitezza dell’unione di due finitiTheorem 25a. Finite(X) & Finite(Y)→ Finite(X ∪ Y). Proof:


-- Ragionando per assurdo, siano x0 ed y0 insiemi finiti la cui unione non e finita. Alloravi sara un insieme non vuoto g0 di sottoinsiemi di x0 ∪ y0 sprovvisto di elemento minimalerispetto all’inclusione.

Use def (Finite) ⇒ Stat1 :¬�∀g ∈ P

�P(x0 ∪ y0)

�\ {∅} ,∃m | g ∩ Pm = {m} � & Stat2 :

�∀g� ∈ P(Px0)\ {∅} ,∃m | g� ∩ Pm = {m} � & Stat3 : �∀gq ∈ P(Py0)\ {∅} ,∃m | gq ∩ Pm = {m} ��g0��→Stat1 ⇒ Stat4 : ¬�∃m | g0 ∩ Pm = {m} � & g0 ∈ P

�P(x0 ∪ y0)

�\ {∅}

-- Indichiamo con g1 l’insieme delle intersezioni x0 ∩ v con v che varia in g0. Poiche g0

non e vuoto, neanche g1 puo esserlo.

Loc def ⇒ Stat5 : g1 = {x0 ∩ v : v ∈ g0}Suppose ⇒ Stat6 : x0 ∩ arb(g0) /∈ {x0 ∩ v : v ∈ g0}�arb(g0) ��→Stat6(Stat4) ⇒ false; Discharge ⇒ Stat7 : x0 ∩ arb(g0) ∈ g1

-- Allora, visto che abbiamo supposto x0 finito e visto che g1 e formato da sottoinsiemidi x0, g1 avra un elemento minimale m1.

Suppose ⇒ g1 /∈ P(Px0)Use def (P) ⇒ Stat8 : g1 /∈ {y : y ⊆ {z : z ⊆ x0}}�g1��→Stat8(Stat8�) ⇒ Stat9 : g1 �⊆ {z : z ⊆ x0}�x1��→Stat9(Stat5,Stat9�) ⇒ Stat10 : x1 ∈ {x0 ∩ v : v ∈ g0} & x1 /∈ {z : z ⊆ x0}�v1, x0 ∩ v1��→Stat10(Stat10�) ⇒ false; Discharge ⇒ Auto�g1��→Stat2(Stat7�) ⇒ Stat11 : �∃m | g1 ∩ Pm = {m} ��m1��→Stat11(Stat11) ⇒ g1 ∩ Pm1 = {m1}

-- Indichiamo con g2 l’insieme delle intersezioni y0 ∩ v con v che varia sugli elementi dig0 la cui intersezione con x0 e m1. Poiche almeno un tale v in g0 ci dev’essere, anche g2

non puo essere vuoto.

Loc def ⇒ Stat12 : g2 = {y0 ∩ v : v ∈ g0 | x0 ∩ v = m1}Suppose ⇒ Stat13 : {y0 ∩ v : v ∈ g0 | x0 ∩ v = m1} = ∅ELEM ⇒ Stat14 : m1 ∈ {x0 ∩ v : v ∈ g0}�v0��→Stat14 ⇒ Auto�v0��→Stat13(Stat14�) ⇒ false; Discharge ⇒ Auto

-- Pertanto, visto che abbiamo supposto y0 finito e visto che g2 che e formato da sottoin-siemi di y0, g2 avra un elemento minimale m2.

Suppose ⇒ Stat15 : g2 /∈ P(Py0)Use def (P) ⇒ Stat16 : g2 /∈ {y : y ⊆ {z : z ⊆ y0}}�g2��→Stat16(Stat16�) ⇒ Stat17 : g2 �⊆ {z : z ⊆ y0}�x2��→Stat17(Stat12,Stat17�) ⇒ Stat18 : x2 ∈ {y0 ∩ v : v ∈ g0 | x0 ∩ v = m1} & x2 /∈ {z : z ⊆ y0}�v2, y0 ∩ v2��→Stat18(Stat18�) ⇒ false; Discharge ⇒ Auto�g2��→Stat3(Stat11�) ⇒ Stat19 : �∃m | g2 ∩ Pm = {m} ��m2��→Stat19(Stat19�) ⇒ g2 ∩ Pm2 = {m2}

-- Vedremo ora che m1 ∪ m2 e minimale in g0, contro l’assurda ipotesi con cui eravamopartiti. Cominciamo con l’osservare che m1 ∪ m2 appartiene in effetti a g0, dal momentoche coincide con un elemento w0 di g0 che ha con x0 l’intersezione m1 e con y0 l’intersezionem2.

(Stat12�)ELEM ⇒ Stat20 : m2 ∈ {y0 ∩ v : v ∈ g0 | x0 ∩ v = m1}�w0��→Stat20(Stat20,Stat4�) ⇒ m2 = y0 ∩ w0 & w0 ∈ g0 & x0 ∩ w0 = m1 & g0 ∈ P

�P(x0 ∪ y0)

�

Use def (P) ⇒ Stat21 : g0 ∈ {y : y ⊆ {z : z ⊆ x0 ∪ y0}}�y1��→Stat21(Stat20�) ⇒ Stat22 : w0 ∈ {z : z ⊆ x0 ∪ y0}�z1��→Stat22(Stat20�) ⇒ w0 = m1 ∪ m2

-- Poiche w0 non e minimale in g0, indichiamone con w1 un sottoinsieme stretto cheappartenga a g0, per cui risultera che o x0 ∩ w1 e sottoinsieme stretto di x0 ∩ w0 oppurey0 ∩ w1 lo e di y0 ∩ w0.

�w0, w0��→T1a (Stat20�) ⇒ w0 ∈ g0 ∩ Pw0

�w0��→Stat4(Stat22�) ⇒ Stat23 : g0 ∩ Pw0 �⊆ {w0}Use def (Pw0) ⇒ Auto�w1��→Stat23(Stat23�) ⇒ Stat24 : w1 ∈ {y : y ⊆ w0} & w1 �= w0 & w1 ∈ g0

�y2��→Stat24(Stat20�) ⇒ w1 ⊆ w0 & x0 ∩ w1 �= m1 ∨ y0 ∩ w1 �= m2

-- Consideriamo dapprima l’eventualita che x0 ∩ w1 �= x0 ∩ w0. Facile vedere che un sif-fatto elemento, inficiando la minimalita di m1 = x0 ∩ w0 in g1, ci porterebbe a una con-traddizione.

Suppose ⇒ x0 ∩ w1 �= m1

Suppose ⇒ x0 ∩ w1 /∈ g1

EQUAL �Stat5�⇒ Stat25 : x0 ∩ w1 /∈ {x0 ∩ v : v ∈ g0}�w1��→Stat25(Stat24,Stat24�) ⇒ false; Discharge ⇒ AutoUse def (Pm1) ⇒ Auto(Stat11�)ELEM ⇒ Stat26 : x0 ∩ w1 /∈ {z : z ⊆ m1}�x0 ∩ w1��→Stat26(Stat20�) ⇒ false; Discharge ⇒ Stat27 : x0 ∩ w1 = m1 & y0 ∩ w1 �= m2

-- Consideriamo allora l’eventualita che y0 ∩ w1 �= y0 ∩ w0 mentre x0 ∩ w1 = x0 ∩ w0. Inquesto caso verrebbe inficiata la minimalita di m2 = y0 ∩ w0 in g2; in questo caso lacontraddizione non ha vi e d’uscita e ci fornisce la conclusione che stavamo cercandoattraverso l’argomento per assurdo.

Suppose ⇒ y0 ∩ w1 /∈ g2

EQUAL �Stat12�⇒ Stat28 : y0 ∩ w1 /∈ {y0 ∩ v : v ∈ g0 | x0 ∩ v = m1}�w1��→Stat28(Stat24,Stat27�) ⇒ false; Discharge ⇒ AutoUse def (Pm2) ⇒ Auto(Stat19�)ELEM ⇒ Stat29 : y0 ∩ w1 /∈ {z : z ⊆ m2}�y0 ∩ w1��→Stat29(Stat20�) ⇒ false; Discharge ⇒ Qed

-- finitezza dei singolettiTheorem 25b. Finite({X}) & Finite(∅). Proof:

Suppose not(x0) ⇒ Auto� {x0} , ∅��→T25 ⇒ ¬Finite({x0})Use def (Finite) ⇒ Stat1 : ¬�∀g ∈ P(P {x0})\ {∅} ,∃m | g ∩ Pm = {m} ��g0��→Stat1 ⇒ Stat2 : ¬�∃m | g0 ∩ Pm = {m} � & g0 ∈ P(P {x0})\ {∅}Use def (P) ⇒ Stat3 : g0 ∈ {y : y ⊆ P {x0}}�x0��→T1b ⇒ Auto�y0��→Stat3(Stat2�) ⇒ Stat4 : g0 �= ∅ & g0 ⊆ {∅, {x0}}Suppose ⇒ ∅ ∈ g0

�∅��→Stat2(Stat3�) ⇒ false; Discharge ⇒ g0 = {{x0}}� {x0} ��→Stat2(Stat3�) ⇒ false; Discharge ⇒ Qed

-- finitezza delle paiaTheorem 25c. Z = {X,Y}→ Finite(Z). Proof:

Suppose not(z0, x0, y0) ⇒ Auto�x0��→T25b ⇒ Auto�y0��→T25b ⇒ Auto� {x0} , {y0} ��→T25a ⇒ Finite({x0} ∪ {y0}) & {x0} ∪ {y0} = {x0, y0}EQUAL ⇒ false; Discharge ⇒ Qed

Theory finiteInduction�s0,P(S)

�

Finite(s0) & P(s0)End finiteInduction

Enter theory finiteInduction

Theorem finiteInduction1. �∃m | {s ⊆ s0 | P(s)} ∩ Pm = {m} �. Proof:Suppose not() ⇒ Auto

Assump ⇒ Finite(s0) & P(s0)Use def (Finite) ⇒ Stat1 : �∀g ∈ P(Ps0)\ {∅} ,∃m | g ∩ Pm = {m} �� {s ⊆ s0 | P(s)} ��→Stat1 ⇒ {s ⊆ s0 | P(s)} /∈ P(Ps0)\ {∅}Suppose ⇒ Stat2 : s0 /∈ {s ⊆ s0 | P(s)}�s0��→Stat2 ⇒ false; Discharge ⇒ {s ⊆ s0 | P(s)} /∈ P(Ps0)Use def (P) ⇒ Stat3 : {s ⊆ s0 | P(s)} /∈ {y : y ⊆ {z : z ⊆ s0}}� {s ⊆ s0 | P(s)} ��→Stat3 ⇒ Stat4 : {s ⊆ s0 | P(s)} �⊆ {z : z ⊆ s0}�s1��→Stat4 ⇒ Stat5 : s1 ∈ {s : s ⊆ s0 | P(s)} & s1 /∈ {z : z ⊆ s0}�s, s1��→Stat5(Stat5�) ⇒ false; Discharge ⇒ Qed

APPLY �v1Θ : finΘ� Skolem⇒

Theorem finiteInduction0. {s ⊆ s0 | P(s)} ∩ PfinΘ = {finΘ} .

-- insieme finito minimale soddisfacente PTheorem finiteInduction2. S ⊆ finΘ → s0 ⊇ S & Finite(S) &

�P(S) ↔ S = finΘ

�. Proof:

Suppose not(s1) ⇒ AutoTfiniteInduction0 ⇒ {s ⊆ s0 | P(s)} ∩ PfinΘ = {finΘ}ELEM ⇒ Stat1 : finΘ ∈ {s ⊆ s0 | P(s)}� ��→Stat1 ⇒ finΘ ⊆ s0 & P(finΘ)Assump ⇒ Finite(s0)�s0, finΘ��→T25 ⇒ Finite(finΘ)�finΘ, s1��→T25 ⇒ P(s1) �= s1 = finΘ

Suppose ⇒ s1 = finΘ

EQUAL ⇒ false; Discharge ⇒ s1 /∈ {s ⊆ s0 | P(s)} ∩ PfinΘ & P(s1)Suppose ⇒ s1 /∈ PfinΘ

Use def (P) ⇒ Stat2 : s1 /∈ {y : y ⊆ finΘ}�s1��→Stat2 ⇒ false; Discharge ⇒ Stat3 : s1 /∈ {s ⊆ s0 | P(s)}�s1��→Stat3 ⇒ false; Discharge ⇒ Qed


Display finiteInduction

Theory finiteInduction�s0,P(S)

�

Finite(s0) & P(s0)⇒ (finΘ)

�∀S | S ⊆ finΘ → Finite(S) & s0 ⊇ S &�P(S) ↔ S = finΘ

��End finiteInduction

-- Illustriamo l’utilita del principio d’induzione finita or ora introdotto dimostrando chel’unione di una famiglia finita d’insiemi finiti e finita. In modo analogo, ma piu semplice,si dimostrera che gli aperti di uno spazio topologico sono chiusi rispetto all’intersezionemonadica di famiglie finite (visto che sono chiusi rispetto all’intersezione diadica).

-- l’unione di una famiglia finita di insiemi finiti e finitaTheorem 25d. Finite(F)→ Finite

��{v ∈ F | Finite(v)}

�. Proof:

Suppose not(f0) ⇒ Auto

APPLY �finΘ : f1� finiteInduction

“s0 �→ f0, P(S) �→ ¬Finite

`S{v ∈ S | Finite(v)}

´”⇒

Stat1 : �∀S | S ⊆ f1 → f0 ⊇ S & Finite(S) &

�¬Finite

��{v ∈ S | Finite(v)}

�↔ S = f1

��

�f1��→Stat1(Stat1�) ⇒ Finite(f1) & ¬Finite��

{v ∈ f1 | Finite(v)}�

Loc def ⇒ a = arb(f1)Suppose ⇒ f1 = ∅ELEM ⇒ {v ∈ ∅ | Finite(v)} = ∅EQUAL ⇒ {v ∈ f1 | Finite(v)} = ∅� {v ∈ f1 | Finite(v)} ��→T3f ⇒

�{v ∈ f1 | Finite(v)} = ∅

�∅��→T25b ⇒ Finite(∅)EQUAL �Stat1�⇒ false; Discharge ⇒ Auto(Stat1)ELEM ⇒ Stat2 : a ∈ f1

Suppose ⇒ Stat3 : {v ∈ f1 | Finite(v)} �= if Finite(a) then {a} else ∅ fi ∪ {v ∈ f1\ {a} | Finite(v)}�e��→Stat3(Stat3�) ⇒ e ∈ {v ∈ f1 | Finite(v)}↔ e /∈ if Finite(a) then {a} else ∅ fi ∪ {v ∈ f1\ {a} | Finite(v)}Suppose ⇒ Stat4 : e ∈ {v ∈ f1 | Finite(v)}� ��→Stat4(Stat3�) ⇒ Stat5 : e /∈ {v ∈ f1\ {a} | Finite(v)} & e ∈ f1 & Finite(e) & e /∈ if Finite(a) then {a} else ∅ fi�e��→Stat5(Stat5�) ⇒ e = a & ¬Finite(a)EQUAL ⇒ false; Discharge ⇒ AutoSuppose ⇒ e ∈ if Finite(a) then {a} else ∅ fi(Stat3�)ELEM ⇒ Stat6 : e /∈ {v : v ∈ f1 | Finite(v)} & e = a & Finite(a)�a��→Stat6(Stat6,Stat2�) ⇒ false; Discharge ⇒ AutoSet monot ⇒ {v ∈ f1 | Finite(v)} ⊇ {v ∈ f1\ {a} | Finite(v)}(Stat3�)Discharge ⇒ Auto(Stat2�)ELEM ⇒ {v ∈ f1 | Finite(v)} = if Finite(a) then {a} else ∅ fi ∪ {v ∈ f1\ {a} | Finite(v)}�if Finite(a) then {a} else ∅ fi, {v ∈ f1\ {a} | Finite(v)} ��→T3c ⇒ AutoEQUAL ⇒ Stat7 : ¬Finite

��if Finite(a) then {a} else ∅ fi ∪

�{v ∈ f1\ {a} | Finite(v)}

�

�f1\ {a} ��→Stat1(Stat2,Stat2�) ⇒ Finite��

{v ∈ f1\ {a} | Finite(v)}�

�Sif Finite(a) then {a} else ∅ fi,S

{v ∈ f1\ {a} | Finite(v)} ��→T25a (Stat7�) ⇒ Stat8 : ¬Finite

��if Finite(a) then {a} else ∅ fi

�

�a��→T25b ⇒ Finite(∅) & Finite({a})Suppose ⇒ ¬Finite(a)�∅��→T3f (Stat7�) ⇒ if Finite(a) then {a} else ∅ fi = ∅ &

�∅= ∅

EQUAL �Stat8�⇒ false; Discharge ⇒ Auto�∅, ∅, a��→T3a (Stat7�) ⇒ if Finite(a) then {a} else ∅ fi = {a} &

�{a} = a

EQUAL �Stat8�⇒ false; Discharge ⇒ Qed

Theory finiteImage�s0, f(X)

�

Finite(s0)End finiteImage

Enter theory finiteImage

Theorem finiteImage. Finite�{f(x) : x ∈ s0}

�. Proof:

Suppose not() ⇒ Auto

-- Possiamo dimostrare l’enunciato utilizzando l’induzione finita. Supponendo per as-surdo che s0 abbia, tramite la funzione globale f(X), immagine infinita, prendiamo uns1 finito e minimale rispetto all’inclusione che abbia, del pari, immagine {f(x) : x ∈ s1}infinita. Si vede facilmente che s1 �= ∅, per cui togliendo ad s1 un elemento a, troviamoche {f(x) : x ∈ s1\ {a}} e finito per la supposta minimalita di s1. Visto che l’unione didue insiemi finiti e finita, avremo che {f(x) : x ∈ s1\ {a}} ∪ {f} (a) e finita e dunquedifferisce da {f(x) : x ∈ s1}.

Assump ⇒ Finite(s0)APPLY �finΘ : s1� finiteInduction

“s0 �→ s0, P(S) �→ ¬Finite

`{f(x) : x ∈ S}

´”⇒

Stat1 : �∀S | S ⊆ s1 → Finite(S) & s0 ⊇ S &

�¬Finite

�{f(x) : x ∈ S}

�↔ S = s1

��

�s1��→Stat1 ⇒ ¬Finite�{f(x) : x ∈ s1}

�

Loc def ⇒ Stat0 : a = arb(s1)�f(a)��→T25b ⇒ Finite

�{f} (a)

�& Finite(∅)

Suppose ⇒ s1 = ∅ELEM ⇒ {f(x) : x ∈ ∅} = ∅EQUAL ⇒ false; Discharge ⇒ Auto(Stat0)ELEM ⇒ Stat2 : s1\ {a} ⊆ s1 & s1\ {a} �= s1

Suppose ⇒ {f(x) : x ∈ s1} = {f(x) : x ∈ s1\ {a}} ∪ {f} (a)�s1\ {a} ��→Stat1(Stat2�) ⇒ Finite

�{f(x) : x ∈ s1\ {a}}

�

� {f(x) : x ∈ s1\ {a}} , {f} (a)��→T25a (Stat1�) ⇒Finite

�{f(x) : x ∈ s1\ {a}} ∪ {f} (a)

�

EQUAL �Stat1�⇒ false; Discharge ⇒ Auto

-- Ma in realta {f(x) : x ∈ s1\ {a}} ∪ {f} (a) ed {f(x) : x ∈ s1} sono uguali: ineffetti a ∈ s1 e dunque f(a) ∈ {f(x) : x ∈ s1}; inoltre, per monotonicita{f(x) : x ∈ s1\ {a}} ⊆ {f(x) : x ∈ s1} ed infine . . .

Set monot ⇒ {f(x) : x ∈ s1\ {a}} ⊆ {f(x) : x ∈ s1}Suppose ⇒ Stat3 : f(a) /∈ {f(x) : x ∈ s1}�a��→Stat3(Stat2,Stat2�) ⇒ false; Discharge ⇒ Stat4 : {f(x) : x ∈ s1} �⊆ {f(x) : x ∈ s1\ {a}} ∪ {f} (a)

-- . . . e facile vedere che {f(x) : x ∈ s1} ⊆ {f(x) : x ∈ s1\ {a}} ∪ {f} (a), . . .

�b��→Stat4(Stat4�) ⇒ Stat5 : b ∈ {f(x) : x ∈ s1} & b /∈ {f(x) : x ∈ s1\ {a}} ∪ {f} (a)�x0��→Stat5(Stat5�) ⇒ f(x0) /∈ {f(x) : x ∈ s1\ {a}} & x0 ∈ s1 & f(x0) �= f(a)Suppose ⇒ x0 = aEQUAL �Stat5�⇒ false; Discharge ⇒ Stat6 : f(x0) /∈ {f(x) : x ∈ s1\ {a}} & x0 �= a & x0 ∈ s1�x0��→Stat6(Stat6�) ⇒ false; -

-- il che ci porta alla contraddizione cercata.

Discharge ⇒ Qed


-- Per dimostrare l’esistenza di un insieme infinito introduciamo, a partire dall’insiemepredefinito s inf e da una correlata nozione prk di pseudo-rango, l’insieme nats dei numerinaturali intesi alla von Neumann.-- una funzione globale che associa un naturale di von Neumann a qualunque insieme

Def pseudoRank. prk(X) =Def arb({prk(y) ∪ {prk} (y) : y ∈ X | X = {y} & y ∈ s inf})

-- numeri naturaliDef natural numbers. nats =Def {prk(x) : x ∈ s inf}

-- esistenza di un insieme infinitoTheorem 10045. ¬Finite(nats). Proof:

Suppose not() ⇒ AutoUse def (Finite) ⇒ Stat0 : �∀g ∈ P(Pnats)\ {∅} ,∃m | g ∩ Pm = {m} �

-- Se per assurda ipotesi nats fosse un insieme finito, ogni famiglia non vuota di suoisottoinsiemi finiti avrebbe un elemento minimale. Cio sarebbe vero in particolare per lafamiglia

g0 = {nats\n : n ∈ nats} ,

poiche in effetti, come subito verificheremo, a tale famiglia appartiene nats ed e inoltrechiaro che tutti i suoi elementi sono sottoinsiemi di nats.

Loc def ⇒ Stat1 : g0 = {nats\n : n ∈ nats}

-- Richiamiamo che s inf �= ∅, in base all’assioma che riguarda questa costante; perciorisulta prk(arb(s inf )) = ∅ e dunque ∅ ∈ nats e dunque nats ∈ g0.

Suppose ⇒ nats /∈ g0

EQUAL ⇒ Stat2 : nats /∈ {nats\n : n ∈ nats}�∅��→Stat2(Stat2�) ⇒ ∅ /∈ natsUse def (nats) ⇒ Stat3 : ∅ /∈ {prk(x) : x ∈ s inf}Assump ⇒ s inf �= ∅Use def (prk) ⇒ prk(arb(s inf )) = arb({prk(y) ∪ {prk} (y) : y ∈ arb(s inf ) | arb(s inf ) = {y} & y ∈ s inf})�arb(s inf ) ��→Stat3(Stat3) ⇒ Stat4 : {prk(y) ∪ {prk} (y) : y ∈ arb(s inf ) | arb(s inf ) = {y} & y ∈ s inf} �= ∅�y0��→Stat4(Stat4) ⇒ false; Discharge ⇒ AutoSuppose ⇒ g0 /∈ P(Pnats)Use def (P) ⇒ Stat5 : g0 /∈ {x : x ⊆ {y : y ⊆ nats}}�g0��→Stat5(Stat5�) ⇒ Stat6 : g0 �⊆ {y : y ⊆ nats}�s0��→Stat6(Stat1,Stat1�) ⇒ Stat7 : s0 ∈ {nats\n : n ∈ nats} & s0 /∈ {y : y ⊆ nats}�n1, nats\n1��→Stat7(Stat7�) ⇒ false; Discharge ⇒ Auto�g0��→Stat0(Stat1�) ⇒ Stat8 : �∃m | g0 ∩ Pm = {m} ��m0��→Stat8(Stat1,Stat1�) ⇒ {nats\n : n ∈ nats} ∩ Pm0 = {m0}(Stat8�)ELEM ⇒ Stat9 : m0 ∈ {nats\n : n ∈ nats}�n0��→Stat9(Stat9�) ⇒ n0 ∈ nats & m0 = nats\n0

Use def (nats) ⇒ Stat10 : n0 ∈ {prk(x) : x ∈ s inf}�x0��→Stat10(Stat10�) ⇒ n0 = prk(x0) & x0 ∈ s infAssump ⇒ Stat11 : �∀x ∈ s inf | {x} ∈ s inf��x0��→Stat11(Stat10�) ⇒ {x0} ∈ s infSuppose ⇒ prk({x0}) /∈ natsUse def (nats) ⇒ Stat12 : prk({x0}) /∈ {prk(x) : x ∈ s inf}� {x0} ��→Stat12(Stat11�) ⇒ false; Discharge ⇒ AutoSuppose ⇒ Stat13 : prk({x0}) �= prk(x0) ∪ {prk} (x0)Use def (prk) ⇒ prk({x0}) = arb({prk(y) ∪ {prk} (y) : y ∈ {x0} | {x0} = {y} & y ∈ s inf})(Stat13)ELEM ⇒ Stat14 : {prk(x0) ∪ {prk} (x0)} �= {prk(y) ∪ {prk} (y) : y ∈ {x0} | {x0} = {y} & y ∈ s inf}

Suppose ⇒ Stat15 : prk(x0) ∪ {prk} (x0) /∈ {prk(y) ∪ {prk} (y) : y ∈ {x0} | {x0} = {y} & y ∈ s inf}�x0��→Stat15(Stat10�) ⇒ false; Discharge ⇒ Auto

�c0��→Stat14(Stat14�) ⇒ Stat16 : c0 ∈ {prk(y) ∪ {prk} (y) : y ∈ {x0} | {x0} = {y} & y ∈ s inf} & c0 �= prk(x0) ∪ {prk} (x0)�y1��→Stat16(Stat10�) ⇒ x0 = y1 & prk(y1) ∪ {prk} (y1) �= prk(x0) ∪ {prk} (x0)EQUAL �Stat16�⇒ false; Discharge ⇒ Auto(Stat8�)ELEM ⇒ Stat17 : prk({x0}) ∈ nats & {x0} ∈ s inf & nats\prk({x0}) ⊆ m0 & nats\prk({x0}) /∈ {nats\n : n ∈ nats} ∩ Pm0

Suppose ⇒ nats\prk({x0}) /∈ Pm0

Use def (P) ⇒ Stat18 : nats\prk({x0}) /∈ {y : y ⊆ m0}�nats\prk({x0})��→Stat18(Stat17�) ⇒ false; Discharge ⇒ Stat19 : nats\prk({x0}) /∈ {nats\n : n ∈ nats}�prk({x0})��→Stat19(Stat17�) ⇒ false; Discharge ⇒ Qed

-- esistenza di un insieme infinito, 2Theorem 10046. ¬Finite(s inf ). Proof:

Suppose not() ⇒ AutoAPPLY � � finiteImage

`s0 �→ s inf , f(X) �→ prk(X)

´⇒ Finite

�{prk(x) : x ∈ s inf}

�

T10045 ⇒ ¬Finite(nats)Use def (nats) ⇒ nats = {prk(x) : x ∈ s inf}EQUAL ⇒ false; Discharge ⇒ Qed

-- In sede di prima verifica delle precedenti dimostrazioni sulla finitezza era stato imp-iegato il nome di predicato ‘Fin’ del tutto sconosciuto a Ref, onde evitare possibili in-terferenze, nelle dimostrazioni, di meccanismi built-in. Aggirata in questo modo unaquestione metodologica, si poi tornati al nome consueto. Accenniamo un altro concettoimportante correlato a quello di finitezza, la cui definizione e inevitabilmente ricorsiva:Una strada percorribile, per una definizione della finitezza ereditaria e la seguente:

trCl(X) =Def X ∪�

{trCl(y) : y ∈ X} ,

HFinite(H) =Def Finite�trCl(H)

�,

Altra strada percorribile, che qui prescegliamo (senza tuttavia svilupparla), e la seguente:-- finitezza ereditaria

Def HFin. HerFinite(X) ↔Def Finite(X) & �∀x ∈ X | HerFinite(x)�

-- Theory of finite intersection closedness.

Theory fic(ss)�∀x, y | {x, y} ⊆ ss → x ∩ y ∈ ss�

End fic

Enter theory fic

-- We will now derive the finite intersection closedness property from the doubletonintersection closedness property.

-- finite intersection closednessTheorem fic1. F ⊆ ss & Finite(F) & F �= ∅→

�(F) ∈ ss. Proof:

Suppose not(f1) ⇒�f1 ⊆ ss & Finite(f1) & f1 �= ∅

�&

�(f1) /∈ ss

-- Arguing by contradiction, consider an inclusion minimal f0 which violates the claimof this theorem. f0 cannot be singleton, else

�v ∈ arb(f0) | �∀w ∈ f0 | v ∈ w�� = arb(f0)

would belong to ss; but then, since�v ∈ arb(f0) | �∀w ∈ f0 | v ∈ w�� = arb(f0) ∩

�v ∈ arb(f0\ {arb(f0)}) | �∀w ∈ f0\ {arb(f0)} | v ∈ w��

is the intersection of two sets in ss, it must belong to ss by an assumption of the presentTHEORY, which leads to a contradiction.

ELEM ⇒ Finite(f1)

-- Use def (Fin) ⇒ Finite (f1)

ELEM ⇒�

(f1) /∈ ss

APPLY �finΘ : f0� finiteInduction

“s0 �→ f1, P(S) �→

`T(S) /∈ ss & S �= ∅

´”⇒

Stat1 : �∀S | S ⊆ f0 → f1 ⊇ S & Finite(S) &��

(S) /∈ ss & S �= ∅ ↔ S = f0��

�f0��→Stat1 ⇒ f1 ⊇ f0 & Finite(f0) &��

(f0) /∈ ss & f0 �= ∅ ↔ f0 = f0�

ELEM ⇒�

(f0) /∈ ss

Suppose ⇒ f0 = {arb(f0)}Use def (

T) ⇒

�v ∈ arb(f0) | �∀w ∈ f0 | v ∈ w�� /∈ ss

Suppose ⇒ Stat2 :�v ∈ arb(f0) | �∀w ∈ f0 | v ∈ w�� ⊆ arb(f0)

�v0��→Stat2 ⇒ v0 /∈ arb(f0) & Stat3 : v0 ∈�v ∈ arb(f0) | �∀w ∈ f0 | v ∈ w��

� ��→Stat3 ⇒ false; Discharge ⇒ Stat4 : arb(f0) �⊆�v ∈ arb(f0) | �∀w ∈ f0 | v ∈ w��

�v1��→Stat4 ⇒ v1 ∈ arb(f0) & Stat5 : v1 /∈�v ∈ arb(f0) | �∀w ∈ f0 | v ∈ w��

�v1��→Stat5 ⇒ Stat6 : ¬�∀w ∈ f0 | v1 ∈ w��w0��→Stat6 ⇒ w0 ∈ f0 & v1 /∈ w0

ELEM ⇒ w0 = arb(f0)ELEM ⇒ false; -

Discharge ⇒ Stat7 : f0 �= {arb(f0)}

�f0��→T23b ⇒�

(f0) = arb(f0) ∩�

(f0\ {arb(f0)})Assump ⇒ Stat8 : �∀x, y | {x, y} ⊆ ss → x ∩ y ∈ ss�

-- ELEM ⇒ (f0-{arb (f0)}) = f0

�f0\ {arb(f0)} ��→Stat1(Stat7) ⇒�

(f0\ {arb(f0)}) ∈ ss

�f0��→Stat1 ⇒ f1 ⊇ f0ELEM ⇒ {arb(f0) ,

�(f0\ {arb(f0)})} ⊆ ss

�arb(f0) ,T

(f0\ {arb(f0)})��→Stat8 ⇒ arb(f0) ∩�

(f0\ {arb(f0)}) ∈ ssELEM ⇒

�(f0) ∈ ss

ELEM ⇒ false; -Discharge ⇒ Qed

-- weaker formulation of doubleton intersection closednessTheorem fic2. �∀x ∈ ss, y ∈ ss, u ∈ x ∩ y,∃z ∈ ss | u ∈ z & z ⊆ x ∩ y�. Proof:

Suppose not ⇒ Stat1 : ¬�∀x ∈ ss, y ∈ ss, u ∈ x ∩ y,∃z ∈ ss | u ∈ z & z ⊆ x ∩ y��x0, y0, u0��→Stat1 ⇒ Stat2 : ¬�∃z ∈ ss | u0 ∈ z & z ⊆ x0 ∩ y0� & x0, y0 ∈ ss & u0 ∈ x0 ∩ y0

Assump ⇒ Stat3 : �∀x, y | {x, y} ⊆ ss → x ∩ y ∈ ss��x0, y0��→Stat3(Stat2�) ⇒ x0 ∩ y0 ∈ ss�x0 ∩ y0��→Stat2 ⇒ false; Discharge ⇒ Qed


Display fic

Theory fic(ss)�∀x, y | {x, y} ⊆ ss → x ∩ y ∈ ss�

⇒�∀f | f ⊆ ss & Finite(f) & f �= ∅ →

�(f) ∈ ss�

�∀x ∈ ss, y ∈ ss, u ∈ x ∩ y,∃z ∈ ss | u ∈ z & z ⊆ x ∩ y�End fic

-- Specialized variant of the preceding theory on finite intersection closedness, for thecase when the given family of sets is known to be closed under unionset formation.

Theory ficu(open){x ⊆ open |

�x /∈ open} = ∅

�∀x ∈ open, y ∈ open, u ∈ x ∩ y,∃z ∈ open | u ∈ z & z ⊆ x ∩ y�End ficu

Enter theory ficu

-- We will attain the finite intersection closedness property through the doubleton inter-section closedness property.-- doubleton intersection closedness

Theorem ficu1. {X,Y} ⊆ open → X ∩ Y ∈ open. Proof:Suppose not(x0, y0) ⇒ Auto

-- It plainly holds that

x0 ∩ y0 =�

{z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0} ,

because the right-hand side of this equality is the unionset of subsets of the left-hand sideand, on the other hand, for each u0 ∈ x0 ∩ y0, the set {z : z ∈ open | u0 ∈ z & z ⊆ x0 ∩ y0}is included in the right hand side and has u0 as a member.

Suppose ⇒ x0 ∩ y0 �⊇�

{z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0}�x0 ∩ y0, {z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0} ��→T3 (�) ⇒ Stat1 : ¬

�∀x ∈ {z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0} | x ⊆ x0 ∩ y0��x1��→Stat1(Stat1�) ⇒ Stat2 : x1 ∈ {z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0} & x0 ∩ y0 �⊇ x1

�z, u��→Stat2(Stat2�) ⇒ false; Discharge ⇒ AutoSuppose ⇒ Stat3 : x0 ∩ y0 �⊆

�{z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0}

Use def (S

{z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0}) ⇒ Auto�u0��→Stat3(Stat3�) ⇒ Stat4 :

u0 /∈ {u : z� ∈ {z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0} , u ∈ z�} & u0 ∈ x0 ∩ y0

Assump ⇒ Stat5 : �∀x ∈ open, y ∈ open, u ∈ x ∩ y,∃z ∈ open | u ∈ z & z ⊆ x ∩ y��x0, y0, u0��→Stat5 ⇒ Stat6 : �∃z ∈ open | u0 ∈ z & z ⊆ x0 ∩ y0��z0��→Stat6(Stat6�) ⇒ z0 ∈ open & u0 ∈ z0 & z0 ⊆ x0 ∩ y0

�z0, u0��→Stat4(Stat6�) ⇒ Stat7 : z0 /∈ {z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0}�z0, u0��→Stat7(Stat6�) ⇒ false; Discharge ⇒ Stat8 :

�{z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0} /∈ open

Assump ⇒ Stat9 : {x ⊆ open |�

x /∈ open} = ∅� {z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0} ��→Stat9(Stat8�) ⇒ Stat10 :

{z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0} �⊆ open�z1��→Stat10(Stat10�) ⇒ Stat11 : z1 ∈ {z : z ∈ open, u ∈ x0 ∩ y0 | u ∈ z & z ⊆ x0 ∩ y0} & z1 /∈ open�z2, u2��→Stat11(Stat11�) ⇒ false; Discharge ⇒ Qed

-- At this point, finite intersection closedness follows by straightforward application ofthe THEORY fic.

APPLY � � fic(ss �→ open)⇒

-- finite intersection closednessTheorem ficu2. �∀f | f ⊆ open & Finite(f) & f �= ∅ →

�(f) ∈ open�.


Display ficu

Theory ficu(open){x ⊆ open |

�x /∈ open} = ∅

�∀x ∈ open, y ∈ open, u ∈ x ∩ y,∃z ∈ open | u ∈ z & z ⊆ x ∩ y�⇒

�∀x, y | {x, y} ⊆ open → x ∩ y ∈ open��∀f | f ⊆ open & Finite(f) & f �= ∅ →

�(f) ∈ open�

End ficu

-- Nozioni basilari sulle ‘mappe’, intese semplicemente come insiemi di coppie, sulle fun-zioni e sulle biiezioni.-- Map range

Def maps · 4. range(X) =Def

�x[2] : x ∈ X

�

-- MapDef maps · 5. Is map(X) ↔Def �∀p ∈ X | p =

�p[1], p[2]

� �-- Single-valued map predicate

Def maps · 6. Svm(X) ↔Def Is map(X) & �∀p ∈ X, q ∈ X | p[1] = q[1] → p = q�-- One-one map predicate

Def maps · 7. One 1 map(X) ↔Def Svm(X) & �∀p ∈ X, q ∈ X | p[2] = q[2] → p = q�

-- Restrictions of one-one maps are one-oneTheorem 58. One 1 map(F)→ One 1 map(F|S). Proof:

Suppose not(f, s) ⇒ Stat0 : One 1 map(f) & ¬One 1 map(f|s)Use def

`One 1 map(f)

´⇒ Auto

Use def`Svm(f)

´⇒ Auto

Use def`Is map(f)

´⇒ Auto

EQUAL ⇒ Stat1 : �∀x ∈ f | x =�x[1], x[2]

� � & �∀x ∈ f, y ∈ f | x[1] = y[1] → x = y� & �∀x ∈ f, y ∈ f | x[2] = y[2] → x = y�Use def (|) ⇒ Stat2 : f|s =

�p ∈ f | p[1] ∈ s

�

Set monot ⇒�p ∈ f | p[1] ∈ s

�⊆ {p ∈ f | true}

(Stat0�)ELEM ⇒ Stat3 : f|s ⊆ f & ¬One 1 map(f|s)Suppose ⇒ ¬�∀x ∈ f|s | x =

�x[1], x[2]

� �(Stat1�)ELEM ⇒ Stat4 : ¬�∀x ∈ f|s | x =

�x[1], x[2]

� � & �∀x ∈ f | x =�x[1], x[2]

� �

�x1, x1��→Stat4(Stat3�) ⇒ false; Discharge ⇒ AutoSuppose ⇒ ¬�∀x ∈ f|s , y ∈ f|s | x[1] = y[1] → x = y�(Stat1�)ELEM ⇒ Stat5 : ¬�∀x ∈ f|s , y ∈ f|s | x[1] = y[1] → x = y� & �∀x ∈ f, y ∈ f | x[1] = y[1] → x = y��x2, y2, x2, y2��→Stat5(Stat3�) ⇒ false; Discharge ⇒ AutoSuppose ⇒ ¬�∀x ∈ f|s , y ∈ f|s | x[2] = y[2] → x = y�(Stat1�)ELEM ⇒ Stat6 : ¬�∀x ∈ f|s , y ∈ f|s | x[2] = y[2] → x = y� & �∀x ∈ f, y ∈ f | x[2] = y[2] → x = y��x3, y3, x3, y3��→Stat6(Stat3�) ⇒ false; Discharge ⇒ AutoUse def

`One 1 map(f|s)

´⇒ Auto

Use def`Svm(f|s)

´⇒ Auto

Use def`Is map(f|s)

´⇒ Auto

(Stat3�)Discharge ⇒ Qed

-- Monotonicity of range and domain setsTheorem 65. F ⊆ G → range(F) ⊆ range(G) & domain(F) ⊆ domain(G). Proof:

Suppose not(f, g) ⇒ AutoSet monot ⇒

�x[1] : x ∈ f

�⊆

�x[1] : x ∈ g

�

Set monot ⇒�x[2] : x ∈ f

�⊆

�x[2] : x ∈ g

�

Use def (domain) ⇒ domain(f) ⊆ domain(g)Use def (range) ⇒ false; Discharge ⇒ Qed

-- Map image elements belong to the map rangeTheorem 71. X ∈ domain(F)→ F�X ∈ range(F). Proof:

Suppose not(x0, f) ⇒ AutoUse def (domain(f)) ⇒ AutoUse def (range(f)) ⇒ Auto

Use def (�) ⇒ Stat1 : x0 ∈�p[1] : p ∈ f

�& arb

�f|{x0}

�[2]/∈

�p[2] : p ∈ f

�

Use def (|) ⇒ f|{x0} =�p ∈ f | p[1] ∈ {x0}

�

�p0��→Stat1(Stat1�) ⇒ Stat2 : x0 = p0[1] & p0 ∈ f

EQUAL ⇒ Stat3 : arb��

p ∈ f | p[1] ∈�p0

[1]��[2]

/∈�p[2] : p ∈ f

�

�arb“n

p ∈ f | p[1] ∈n

p0[1]

oo”��→Stat3(Stat3�) ⇒ Stat4 :

arb��

p ∈ f | p[1] ∈�p0

[1]��

/∈ fSuppose ⇒ Stat5 : p0 /∈

�p ∈ f | p[1] ∈

�p0

[1]��

�p0��→Stat5(Stat2,Stat2�) ⇒ false; Discharge ⇒ AutoLoc def ⇒ a = arb

��p ∈ f | p[1] ∈

�p0

[1]��

(Stat4)ELEM ⇒ Stat6 : a ∈�p ∈ f | p[1] ∈

�p0

[1]��

& a /∈ f

� ��→Stat6(Stat6�) ⇒ false; Discharge ⇒ Qed

-- Map image formula

Theorem 74. Svm(F) & P ∈ F → F�P[1] = P[2]. Proof:Suppose not(f, p0) ⇒ AutoUse def

`Is map(f)

´⇒ Auto

Use def (Svm) ⇒ Stat0 : �∀q ∈ f | q =�q[1], q[2]

� � & Stat1 : �∀q ∈ f, p ∈ f | q[1] = p[1] → q = p� & p0 ∈ f & f�p0[1] �= p0

[2]

Use def (�) ⇒ f�p0[1] = arb

�f|{p0[1]}

�[2]

�p0��→Stat0(Stat0�) ⇒ Stat2 : p0 =�p0

[1], p0[2]

�& p0 ∈ f & arb

�f|{p0[1]}

�[2]�= p0

[2]

Use def (|) ⇒ Stat3 : f|{p0[1]} =�p ∈ f | p[1] ∈

�p0

[1]��

Suppose ⇒ Stat4 : p0 /∈�p ∈ f | p[1] ∈

�p0

[1]��

�p0��→Stat4(Stat2,Stat2�) ⇒ false; Discharge ⇒ AutoSet monot ⇒

�p ∈ f | p[1] ∈

�p0

[1]��

⊆ {p ∈ f | true}Loc def ⇒ p1 = arb

�f|{p0[1]}

�

(Stat3)ELEM ⇒ Stat5 : p1 ∈�p ∈ f | p[1] ∈

�p0

[1]��

& p1 ∈ f

� ��→Stat5(Stat5�) ⇒ Stat6 : p1[1] = p0

[1]

�p0, p1��→Stat1(Stat0,Stat5,Stat6�) ⇒ p1 = p0

EQUAL �Stat2�⇒ false; Discharge ⇒ Qed

Theory Must be svm�b(X), s, u

�

End Must be svm

Enter theory Must be svm

-- Single-valued map formerTheorem Must be svm · 1. Svm

�{[x, b(x)] : x ∈ s}

�& domain({[x, b(x)] : x ∈ s}) = s &

range({[x, b(x)] : x ∈ s}) = {b(x) : x ∈ s} &�u ∈ s → {[x, b(x)] : x ∈ s} �u = b(u)

�. Proof:

Suppose not() ⇒ AutoSuppose ⇒ Stat1 : ¬Svm

�{[x, b(x)] : x ∈ s}

�

Use def

“Is map

`{[x, b(x)] : x ∈ s}

´”⇒ Auto

Use def (Svm) ⇒¬

��∀q ∈ {[x, b(x)] : x ∈ s} | q =�q[1], q[2]

� � & �∀q ∈ {[x, b(x)] : x ∈ s} , p ∈ {[x, b(x)] : x ∈ s} | q[1] = p[1] → q = p��

Suppose ⇒ Stat2 : ¬�∀q ∈ {[x, b(x)] : x ∈ s} | q =�q[1], q[2]

� ��q0��→Stat2(Stat2�) ⇒ Stat3 : q0 ∈ {[x, b(x)] : x ∈ s} & q0 �=

�q0

[1], q0[2]

�

�x0��→Stat3(Stat3) ⇒ false; Discharge ⇒ Stat4 : ¬�∀q ∈ {[x, b(x)] : x ∈ s} , p ∈ {[x, b(x)] : x ∈ s} | q[1] = p[1] → q = p��q1, p1��→Stat4(Stat4�) ⇒ Stat5 :

q1, p1 ∈ {[x, b(x)] : x ∈ s} & q1[1] = p1

[1] & q1 �= p1

�x1, x2��→Stat5(Stat5) ⇒ x1 = x2 & b(x1) �= b(x2)EQUAL �Stat5�⇒ false; Discharge ⇒ Auto

Suppose ⇒ Stat6 : domain({[x, b(x)] : x ∈ s}) �= sUse def (domain) ⇒

�p[1] : p ∈ {[x, b(x)] : x ∈ s}

��= s

SIMPLF �Stat6 � �⇒ Stat7 :�

[x, b(x)][1] : x ∈ s��= s

�e��→Stat7(Stat7�) ⇒ e ∈�

[x, b(x)][1] : x ∈ s��= e ∈ s

Suppose ⇒ Stat8 : e ∈�

[x, b(x)][1] : x ∈ s�

�x3��→Stat8(Stat7�) ⇒ false; Discharge ⇒ Stat9 : e /∈�

[x, b(x)][1] : x ∈ s�

& e ∈ s

�e��→Stat9(Stat9�) ⇒ false; Discharge ⇒ AutoSuppose ⇒ Stat10 : range({[x, b(x)] : x ∈ s}) �= {b(x) : x ∈ s}Use def (range) ⇒

�p[2] : p ∈ {[x, b(x)] : x ∈ s}

��= {b(x) : x ∈ s}

SIMPLF �Stat10 � �⇒ Stat11 :�

[x, b(x)][2] : x ∈ s��= {b(x) : x ∈ s}

�c��→Stat11(Stat11) ⇒ false; Discharge ⇒ Stat14 : u ∈ s & {[x, b(x)] : x ∈ s} �u �= b(u)

Use def (�) ⇒ arb�{[x, b(x)] : x ∈ s}|{u}

�[2]�= b(u)

Use def (|) ⇒ {[x, b(x)] : x ∈ s}|{u} =�p ∈ {[x, b(x)] : x ∈ s} | p[1] ∈ {u}

�

SIMPLF �Stat14 � �⇒�p ∈ {[x, b(x)] : x ∈ s} | p[1] ∈ {u}

�=

�[x, b(x)] : x ∈ s | [x, b(x)][1] ∈ {u}

�

EQUAL �Stat14�⇒ arb��

[x, b(x)] : x ∈ s | [x, b(x)][1] ∈ {u}��[2]

�= b(u)

Loc def ⇒ Stat15 : a = arb��

[x, b(x)] : x ∈ s | [x, b(x)][1] ∈ {u}��


[x, b(x)] : x ∈ s | [x, b(x)][1] ∈ {u}�

= ∅�u��→Stat16(Stat14,Stat16) ⇒ false; Discharge ⇒ Auto

(Stat15)ELEM ⇒ Stat17 : a ∈�

[x, b(x)] : x ∈ s | [x, b(x)][1] ∈ {u}�

�x4��→Stat17(Stat17) ⇒ x4 = u & a[2] = b(x4)EQUAL �Stat14�⇒ false; Discharge ⇒ Qed


Display Must be svm

Theory Must be svm�b(x), s, u

�

⇒Svm

�{[x, b(x)] : x ∈ s}

�& domain({[x, b(x)] : x ∈ s}) = s & range({[x, b(x)] : x ∈ s}) = {b(x) : x ∈ s} &

�u ∈ s → {[x, b(x)] : x ∈ s} �u = b(u)

�

End Must be svm

-- Doubletons as maps

Theorem 92. Is map({[X,Y] , [Z,W]}) & domain({[X,Y] , [Z,W]}) = {X,Z} &

range({[X,Y] , [Z,W]}) = {Y,W} &�X �= Z → Svm({[X,Y] , [Z,W]})

�. Proof:

Suppose not(x0, y0, z0, w0) ⇒ AutoSuppose ⇒ ¬Is map({[x0, y0] , [z0,w0]})Use def (Is map) ⇒ Stat1 : ¬�∀p ∈ {[x0, y0] , [z0,w0]} | p =

�p[1], p[2]

� ��p1��→Stat1(Stat1) ⇒ false; Discharge ⇒ AutoSuppose ⇒ Stat2 : domain({[x0, y0] , [z0,w0]}) �= {x0, z0}Use def (domain({[x0, y0] , [z0, w0]})) ⇒ AutoSuppose ⇒ Stat3 : x0 /∈

�p[1] : p ∈ {[x0, y0] , [z0,w0]}

�

� [x0, y0] ��→Stat3(Stat3�) ⇒ false; Discharge ⇒ AutoSuppose ⇒ Stat4 : z0 /∈

�p[1] : p ∈ {[x0, y0] , [z0,w0]}

�

� [z0, w0] ��→Stat4(Stat4�) ⇒ false; Discharge ⇒ Auto(Stat2�)ELEM ⇒ Stat5 : domain({[x0, y0] , [z0,w0]}) �⊆ {x0, z0}�e��→Stat5(Stat2�) ⇒ Stat6 : e ∈

�p[1] : p ∈ {[x0, y0] , [z0,w0]}

�& e /∈ {x0, z0}

�p��→Stat6(Stat6) ⇒ false; Discharge ⇒ AutoUse def

`Svm({[x0, y0] , [z0, w0]})

´⇒ Auto

Suppose ⇒ Stat7 : range({[x0, y0] , [z0,w0]}) �= {y0,w0}Use def (range({[x0, y0] , [z0, w0]})) ⇒ AutoSuppose ⇒ Stat8 : y0 /∈

�q[2] : q ∈ {[x0, y0] , [z0,w0]}

�

� [x0, y0] ��→Stat8(Stat8�) ⇒ false; Discharge ⇒ AutoSuppose ⇒ Stat9 : w0 /∈

�q[2] : q ∈ {[x0, y0] , [z0,w0]}

�

� [z0, w0] ��→Stat9(Stat9�) ⇒ false; Discharge ⇒ Auto(Stat7�)ELEM ⇒ Stat10 : range({[x0, y0] , [z0,w0]}) �⊆ {y0,w0}�d��→Stat10(Stat7�) ⇒ Stat11 : e ∈

�q[1] : q ∈ {[x0, y0] , [z0,w0]}

�& e /∈ {x0, z0}

�q��→Stat11(Stat11) ⇒ false; Discharge ⇒ Stat12 : ¬�∀p ∈ {[x0, y0] , [z0,w0]} , q ∈ {[x0, y0] , [z0,w0]} | p[1] = q[1] → p = q� & x0 �= z0

�p0, q0��→Stat12(Stat12) ⇒ false; Discharge ⇒ Qed

-- Doubletons as maps, 2Theorem 93. X �= Z → {[X,Y] , [Z,W]} �X = Y. Proof:

Suppose not(x, z, y, w) ⇒ Auto

Use def (�) ⇒ arb�{[x, y] , [z,w]}|{x}

�[2]�= y

Use def (|) ⇒ {[x, y] , [z,w]}|{x} =�p ∈ {[x, y] , [z,w]} | p[1] ∈ {x}

�

EQUAL ⇒ arb��

p ∈ {[x, y] , [z,w]} | p[1] ∈ {x}��[2] �= y

Suppose ⇒ Stat1 :�p ∈ {[x, y] , [z,w]} | p[1] ∈ {x}

�= ∅

� [x, y] ��→Stat1(Stat1) ⇒ false; Discharge ⇒ Stat2 :�p : p ∈ {[x, y] , [z,w]} | p[1] ∈ {x}

��= ∅

Loc def ⇒ a = arb��

p ∈ {[x, y] , [z,w]} | p[1] ∈ {x}��

(Stat2)ELEM ⇒ Stat3 : a ∈�p ∈ {[x, y] , [z,w]} | p[1] ∈ {x}

�

� ��→Stat3(Stat3�) ⇒ Stat4 : a ∈ {[x, y] , [z,w]} & a[1] = xEQUAL ⇒ Stat5 : a[2] �= y & x �= z(Stat4,Stat5)Discharge ⇒ Qed

-- Domain of restrictionTheorem 94. domain(F|S) = domain(F) ∩ S. Proof:

Suppose not(f, s) ⇒ AutoUse def (|) ⇒ Stat0 : domain(

�q ∈ f | q[1] ∈ s

�) �= domain(f) ∩ s

Use def (domain) ⇒�p[1] : p ∈

�q ∈ f | q[1] ∈ s

��=

�p[1] : p ∈ f

�∩ s

SIMPLF ⇒ Stat1 :�p[1] : p ∈ f | p[1] ∈ s

��=

�p[1] : p ∈ f

�∩ s

�e��→Stat1(Stat1�) ⇒ Stat2 : e ∈�p[1] : p ∈ f | p[1] ∈ s

��= e ∈

�p[1] : p ∈ f

�∩ s

Suppose ⇒ Stat3 : e ∈�p[1] : p ∈ f | p[1] ∈ s

�

�p0��→Stat3(Stat2�) ⇒ Stat4 : p0[1] /∈

�p[1] : p ∈ f

�& p0 ∈ f

�p0��→Stat4(Stat4�) ⇒ false; Discharge ⇒ Stat5 : e ∈�p[1] : p ∈ f

�& e /∈

�p[1] : p ∈ f | p[1] ∈ s

�& e ∈ s

�p1, p1��→Stat5(Stat5�) ⇒ false; Discharge ⇒ Qed-- Cartesian Product

Def maps · 8. X × Y =Def {[x, y] : x ∈ X, y ∈ Y}

-- Subsets of Cartesian productsTheorem 141. Y ⊆ S ×T↔ Is map(Y) & domain(Y) ⊆ S & range(Y) ⊆ T. Proof:

-- This follows trivially from the fact that a map is a set each of whose elements x is apair

�x[1], x[2]

�

Suppose not(y0, s, t) ⇒ AutoUse def ( × ) ⇒ Stat0 : y0 ⊆ {[x, y] : x ∈ s, y ∈ t} �= Is map(y0) & domain(y0) ⊆ s & range(y0) ⊆ tSuppose ⇒ Stat1 : y0 ⊆ {[x, y] : x ∈ s, y ∈ t}Suppose ⇒ Stat2 : domain(y0) �⊆ sUse def (domain) ⇒ Stat3 :

�x[1] : x ∈ y0

��⊆ s

�p��→Stat3 ⇒ Stat4 : p ∈�x[1] : x ∈ y0

�& p /∈ s

�a��→Stat4(Stat1�) ⇒ Stat5 : a ∈ {[x, y] : x ∈ s, y ∈ t} & a[1] /∈ s�x1, y1��→Stat5(Stat5) ⇒ false; Discharge ⇒ AutoSuppose ⇒ Stat6 : range(y0) �⊆ tUse def (range) ⇒ Stat7 :

�x[2] : x ∈ y0

��⊆ t

�q��→Stat7 ⇒ Stat8 : q ∈�x[2] : x ∈ y0

�& q /∈ t

�b��→Stat8(Stat1�) ⇒ Stat9 : b ∈ {[x, y] : x ∈ s, y ∈ t} & b[2] /∈ t�x2, y2��→Stat9(Stat9) ⇒ false; Discharge ⇒ AutoUse def

`Is map(y0)

´⇒ Auto

(Stat0�)ELEM ⇒ Stat10 : ¬�∀p ∈ y0 | p =�p[1], p[2]

� �

�p0��→Stat10(Stat1�) ⇒ Stat11 : p0 ∈ {[x, y] : x ∈ s, y ∈ t} & p0 �=�p0

[1], p0[2]

�

�x3, y3��→Stat11(Stat11) ⇒ false; Discharge ⇒ AutoUse def

`Is map(y0)

´⇒ Auto

Use def (domain(y0)) ⇒ AutoUse def (range(y0)) ⇒ Auto(Stat0�)ELEM ⇒ Stat12 :

y0 �⊆ {[x, y] : x ∈ s, y ∈ t} & �∀p ∈ y0 | p =�p[1], p[2]

� � &�q[1] : q ∈ y0

�⊆ s &

�q[2] : q ∈ y0

�⊆ t

�p1, p1��→Stat12(Stat12�) ⇒ Stat13 : p1 /∈ {[x, y] : x ∈ s, y ∈ t} & p1 ∈ y0 & p1 =�p1

[1], p1[2]

�

�p1[1], p1

[2]��→Stat13(Stat13�) ⇒ p1[1] /∈ s ∨ p1

[2] /∈ tSuppose ⇒ p1

[1] /∈ s(Stat12�)ELEM ⇒ Stat14 : p1

[1] /∈�q[1] : q ∈ y0

�

�p1��→Stat14(Stat13�) ⇒ false; Discharge ⇒ Auto(Stat12�)ELEM ⇒ Stat15 : p1

[2] /∈�q[2] : q ∈ y0

�

�p1��→Stat15(Stat13�) ⇒ false; Discharge ⇒ Qed

-- CoveringDef Set2. Covers(X,Y) ↔Def

�X = Y

-- Fin intersection propertyDef Set3. HasFip(X) ↔Def {x ⊆ X | Finite(x) & x �= ∅ & inters(x) = ∅} = ∅

-- Teoria di base sugli spazi topologici

Theory topologicalSpace(open){x ⊆ open |

�x /∈ open} = ∅

�∀x ∈ open, y ∈ open, u ∈ x ∩ y,∃z ∈ open | u ∈ z & z ⊆ x ∩ y��open �= ∅

End topologicalSpace

Enter theory topologicalSpace

-- supportDef topologicalSpace0. supportΘ =Def

�open

-- compactnessDef topologicalSpace1. IsCompactΘ(X) ↔Def �∀u ⊆ open | Covers(u,X) → �∃d ⊆ u | Finite(d) & Covers(d,X)��

-- closed setsDef topologicalSpace2. closedΘ =Def {supportΘ\u : u ∈ open}

-- intersectionDef topologicalSpace3. intΘ(X) =Def if X = ∅ then supportΘ else inters(X) fi

APPLY � � ficu(open �→ open)⇒

-- finite intersection closednessTheorem topologicalSpace0. �∀x, y | {x, y} ⊆ open → x ∩ y ∈ open� & �∀f | f ⊆ open & Finite(f) & f �= ∅ → inters(f) ∈ open�.

Theorem topologicalSpace10. supportΘ �= ∅. Proof:Suppose not ⇒ AutoAssump ⇒

�open �= ∅

Use def (supportΘ) ⇒ false; Discharge ⇒ QedTheorem topologicalSpace11. a ⊆ open ∨ a ⊆ closedΘ → �∀w ∈ a | w ⊆ supportΘ�. Proof:

Suppose not(a0) ⇒ AutoELEM ⇒ Stat0 : ¬�∀w ∈ a0 | w ⊆ supportΘ��w0��→Stat0 ⇒ w0 ∈ a0 & w0 �⊆ supportΘ

Suppose ⇒ a0 ⊆ open

Use def (supportΘ) ⇒ Stat1 : w0 �⊆�

open

�x0��→Stat1 ⇒ x0 ∈ w0 & x0 /∈�

open

Use def (S

) ⇒ Stat2 : x0 /∈ {w : y ∈ open,w ∈ y}�w0, x0��→Stat2 ⇒ false; Discharge ⇒ a0 ⊆ closedΘ

Use def (closedΘ) ⇒ Stat3 : w0 ∈ {supportΘ\u : u ∈ open}�u0��→Stat3 ⇒ false; Discharge ⇒ Qed

Theorem topologicalSpace12. u ⊆ open → {supportΘ\k : k ∈ u} ⊆ closedΘ. Proof:Suppose not(u0) ⇒ u0 ⊆ open & Stat0 : {supportΘ\k : k ∈ u0} �⊆ closedΘ

�k0��→Stat0 ⇒ Stat1 : k0 ∈ {supportΘ\k : k ∈ u0} & k0 /∈ closedΘ

�k1��→Stat1 ⇒ k1 ∈ u0 & k0 = supportΘ\k1

Use def (closedΘ) ⇒ Stat2 : closedΘ = {supportΘ\u : u ∈ open}�k2��→Stat2 ⇒ false; Discharge ⇒ Qed

Theorem topologicalSpace13. c ⊆ closedΘ → {supportΘ\k : k ∈ c} ⊆ open. Proof:Suppose not(c0) ⇒ c0 ⊆ closedΘ & Stat0 : {supportΘ\k : k ∈ c0} �⊆ open

�k0��→Stat0 ⇒ Stat1 : k0 ∈ {supportΘ\k : k ∈ c0} & k0 /∈ open

�k1��→Stat1 ⇒ k1 ∈ c0 & k0 = supportΘ\k1

Use def (closedΘ) ⇒ closedΘ = {supportΘ\k : k ∈ open}ELEM ⇒ Stat2 : k1 ∈ {supportΘ\k : k ∈ open}�k2��→Stat2 ⇒ k1 = supportΘ\k2 & k2 ∈ open

EQUAL ⇒ k0 = supportΘ\(supportΘ\k2)

-- k0 = supportΘ ∩ k2

� {k2} ��→T topologicalSpace11 ⇒ Stat3 : �∀w ∈ {k2} | w ⊆ supportΘ��k2��→Stat3 ⇒ false; Discharge ⇒ Qed

Theorem topologicalSpace14. c �= ∅ & inters(c) = ∅→ Covers({supportΘ\k : k ∈ c} , supportΘ). Proof:Suppose not(c0) ⇒ AutoUse def (Covers) ⇒

�{supportΘ\k : k ∈ c0} �= supportΘ

�supportΘ, c0��→T23 ⇒ supportΘ\inters(c0) =�

{supportΘ\k : k ∈ c0}EQUAL ⇒ supportΘ =

�{supportΘ\k : k ∈ c0}

Use def (Covers) ⇒ Covers({supportΘ\k : k ∈ c0} , supportΘ)ELEM ⇒ false; Discharge ⇒ Qed

Theorem topologicalSpace15. Covers(u, supportΘ)→ u �= ∅. Proof:

Suppose not(u0) ⇒ AutoUse def (Covers) ⇒

�u0 = supportΘ

�u0��→T3f ⇒ supportΘ = ∅Use def (supportΘ) ⇒ supportΘ =

�open

EQUAL ⇒�

open = ∅Assump ⇒

�open �= ∅

ELEM ⇒ false; Discharge ⇒ Qed

Theorem topologicalSpace16. Covers(u, supportΘ)→ inters({supportΘ\k : k ∈ u}) = ∅. Proof:Suppose not(u0) ⇒ Auto�u0��→T topologicalSpace15 ⇒ u0 �= ∅Use def (Covers) ⇒

�u0 = supportΘ

�supportΘ, u0��→T23a ⇒ supportΘ\�

u0 = inters({supportΘ\k : k ∈ u0})ELEM ⇒ supportΘ\

�u0 = ∅

EQUAL ⇒ inters({supportΘ\k : k ∈ u0}) = ∅ELEM ⇒ false; Discharge ⇒ Qed

Theorem topologicalSpace17. �∀w ∈ u | w ⊆ supportΘ� → {supportΘ\(supportΘ\k) : k ∈ u} = u. Proof:Suppose not(u0) ⇒ Stat1 : {supportΘ\(supportΘ\k) : k ∈ u0} �= {k : k ∈ u0} & �∀w ∈ u0 | w ⊆ supportΘ��k0, k0��→Stat1 ⇒ false; Discharge ⇒ Qed

Theorem topologicalSpace18. �∀w ∈ u | w ⊆ supportΘ� →�Finite(u) ↔ Finite({supportΘ\k : k ∈ u})

�. Proof:

Suppose not(u0) ⇒ AutoSuppose ⇒ Finite(u0)APPLY � � finiteImage

`s0 �→ u0, f(K) �→ supportΘ\K

´⇒ Finite({supportΘ\k : k ∈ u0})

Discharge ⇒ Finite({supportΘ\k : k ∈ u0}) & ¬Finite(u0)�u0��→T topologicalSpace17 ⇒ {supportΘ\(supportΘ\k) : k ∈ u0} = u0

SIMPLF ⇒ {supportΘ\k : k ∈ {supportΘ\k : k ∈ u0}} = u0

APPLY � � finiteImage`s0 �→ {supportΘ\k : k ∈ u0} , f(K) �→ supportΘ\K

´⇒

Finite({supportΘ\k : k ∈ {supportΘ\k : k ∈ u0}})EQUAL ⇒ false; Discharge ⇒ Qed

Enter theory topologicalSpace

Theorem topologicalSpace19. d ⊆ u → {supportΘ\k : k ∈ d} ⊆ {supportΘ\k : k ∈ u} . Proof:Suppose not(d0, u0) ⇒ d0 ⊆ u0 & Stat0 : {supportΘ\k : k ∈ d0} �⊆ {supportΘ\k : k ∈ u0}�w0��→Stat0 ⇒ Stat1 : w0 ∈ {supportΘ\k : k ∈ d0} & w0 /∈ {supportΘ\k : k ∈ u0}ELEM ⇒ Stat2 : w0 /∈ {supportΘ\k : k ∈ u0}�k0��→Stat1 ⇒ w0 = supportΘ\k0 & k0 ∈ d0

ELEM ⇒ k0 ∈ u0

�k0��→Stat2 ⇒ false; Discharge ⇒ Qed

-- characterization of compactnessTheorem topologicalSpace20. IsCompactΘ(supportΘ)↔ �∀c ⊆ closedΘ | c �= ∅ & HasFip(c) → inters(c) �= ∅�. Proof:

Suppose not([]) ⇒ Auto

Suppose ⇒ IsCompactΘ(supportΘ) & Stat0 : ¬�∀c ⊆ closedΘ | c �= ∅ & HasFip(c) → inters(c) �= ∅��c0��→Stat0 ⇒ c0 ⊆ closedΘ & c0 �= ∅ & HasFip(c0) & inters(c0) = ∅Use def (HasFip) ⇒ Stat1 : {x ⊆ c0 | Finite(x) & x �= ∅ & inters(x) = ∅} = ∅

Use def (IsCompactΘ) ⇒ Stat2 : �∀u ⊆ open | Covers(u, supportΘ) → �∃d ⊆ u | Finite(d) & Covers(d, supportΘ)��

Loc def ⇒ Stat22 : u0 = {supportΘ\k : k ∈ c0}

-- c0 = ∅

Suppose ⇒ u0 = ∅�z0��→Stat22 ⇒ false; Discharge ⇒ u0 �= ∅

�c0��→T topologicalSpace13 ⇒ u0 ⊆ open

�u0��→Stat2 ⇒ Covers(u0, supportΘ)→ �∃d ⊆ u0 | Finite(d) & Covers(d, supportΘ)�

�c0��→T topologicalSpace14 ⇒ Covers({supportΘ\k : k ∈ c0} , supportΘ)EQUAL ⇒ Covers(u0, supportΘ)ELEM ⇒ Stat3 : �∃d ⊆ u0 | Finite(d) & Covers(d, supportΘ)�

�d0��→Stat3 ⇒ d0 ⊆ u0 & Finite(d0) & Covers(d0, supportΘ)�d0��→T topologicalSpace16 ⇒ inters({supportΘ\k : k ∈ d0}) = ∅�d0��→T topologicalSpace15 ⇒ d0 �= ∅

Loc def ⇒ Stat4 : k0 = {supportΘ\k : k ∈ d0}EQUAL ⇒ inters(k0) = ∅

Suppose ⇒ k0 = ∅�b0��→Stat4 ⇒ false; Discharge ⇒ k0 �= ∅

-- d0 ⊆ u0 ed u0 ⊆ open

�d0��→T topologicalSpace11 ⇒ �∀w ∈ d0 | w ⊆ supportΘ��d0��→T topologicalSpace18 ⇒ Finite({supportΘ\k : k ∈ d0})EQUAL ⇒ Finite(k0)

�d0, u0��→T topologicalSpace19 ⇒ {supportΘ\k : k ∈ d0} ⊆ {supportΘ\k : k ∈ u0}EQUAL ⇒ k0 ⊆ {supportΘ\k : k ∈ u0}EQUAL ⇒ k0 ⊆ {supportΘ\k : k ∈ {supportΘ\k : k ∈ c0}}SIMPLF ⇒ k0 ⊆ {supportΘ\(supportΘ\k) : k ∈ c0}

-- c0 ⊆ closedΘ

�c0��→T topologicalSpace11 ⇒ �∀w ∈ c0 | w ⊆ supportΘ��c0��→T topologicalSpace17 ⇒ k0 ⊆ c0

�k0��→Stat1 ⇒ false; -

Discharge ⇒ ¬IsCompactΘ(supportΘ) & Stat5 : �∀c ⊆ closedΘ | c �= ∅ & HasFip(c) → inters(c) �= ∅�Use def (IsCompactΘ) ⇒ Stat6 : ¬�∀u ⊆ open | Covers(u, supportΘ) → �∃d ⊆ u | Finite(d) & Covers(d, supportΘ)��u1��→Stat6 ⇒ u1 ⊆ open & Covers(u1, supportΘ) & ¬�∃d ⊆ u1 | Finite(d) & Covers(d, supportΘ)�

Loc def ⇒ Stat7 : c1 = {supportΘ\k : k ∈ u1}�u1��→T topologicalSpace12 ⇒ {supportΘ\k : k ∈ u1} ⊆ closedΘ

EQUAL ⇒ c1 ⊆ closedΘ

�u1��→T topologicalSpace15 ⇒ u1 �= ∅Suppose ⇒ c1 = ∅�b1��→Stat7 ⇒ false; Discharge ⇒ c1 �= ∅

�c1��→Stat5 ⇒ HasFip(c1)→ inters(c1) �= ∅ELEM ⇒ inters(c1) = ∅→¬HasFip(c1)�u1��→T topologicalSpace16 ⇒ inters({supportΘ\k : k ∈ u1}) = ∅EQUAL ⇒ ¬HasFip(c1)

Use def (HasFip) ⇒ Stat8 : {x ⊆ c1 | Finite(x) & x �= ∅ & inters(x) = ∅} �= ∅ELEM ⇒ Stat9 : ¬�∃d ⊆ u1 | Finite(d) & Covers(d, supportΘ)��x1��→Stat8 ⇒ x1 ⊆ c1 & Finite(x1) & x1 �= ∅ & inters(x1) = ∅

Loc def ⇒ Stat10 : d1 = {supportΘ\k : k ∈ x1}

ELEM ⇒ x1 ⊆ c1

�x1, c1��→T topologicalSpace19 ⇒ {supportΘ\k : k ∈ x1} ⊆ {supportΘ\k : k ∈ c1}EQUAL ⇒ d1 ⊆ {supportΘ\k : k ∈ {supportΘ\k : k ∈ u1}}SIMPLF ⇒ {supportΘ\k : k ∈ {supportΘ\k : k ∈ u1}} = {supportΘ\(supportΘ\k) : k ∈ u1}

-- u1 ⊆ open

�u1��→T topologicalSpace11 ⇒ �∀w ∈ u1 | w ⊆ supportΘ��u1��→T topologicalSpace17 ⇒ {supportΘ\k : k ∈ {supportΘ\k : k ∈ u1}} = u1

EQUAL ⇒ d1 ⊆ u1

-- c1 ⊆ closedΘ x1 ⊆ c1

�x1��→T topologicalSpace11 ⇒ �∀w ∈ x1 | w ⊆ supportΘ��x1��→T topologicalSpace18 ⇒ Finite({supportΘ\k : k ∈ x1})EQUAL ⇒ Finite(d1)

�x1��→T topologicalSpace14 ⇒ Covers({supportΘ\k : k ∈ x1} , supportΘ)EQUAL ⇒ Covers(d1, supportΘ)

�d1��→Stat9 ⇒ false; -

Discharge ⇒ QedEnter theory Set theory

Display topologicalSpace

Theory topologicalSpace(open){x ⊆ open |

�x /∈ open} = ∅

�∀x ∈ open, y ∈ open, u ∈ x ∩ y,∃z ∈ open | u ∈ z & z ⊆ x ∩ y��open �= ∅

⇒supportΘ �= ∅

End topologicalSpace

TECNOLOGIA DELLA DIMOSTRAZIONE - CleverCoder.net - Gil...

Documents

Transcript of TECNOLOGIA DELLA DIMOSTRAZIONE - CleverCoder.net - Gil...