UNIVERSITÀ DEGLI STUDI ROMA TRE FACOLTÀ DI SCIENZE MATEMATICHE FISICHE E

NATURALI

Tesi di Laurea in Matematica di

Claudia Corsi

Sul ruolo della cut-rule e della cut-elimination nei principali

risultati della Logica Matematica

Relatore

Prof. Vito Michele Abrusci

Il Relatore Il Candidato

ANNO ACCADEMICO 2002 - 2003 LUGLIO 2003

Sintesi

Non appena si comincia a leggere un qualsiasi testo matematico, ci si imbatte nella parola ”dimostrazione”. Ci si pone l’obiettivo di ricercare tutto ciò che è insito in questa parola, di comprenderne il significato matematico e logico e l’utilizzo che da sempre se ne è fatto nelle scienze matematiche e filosofiche. Ancora di più, si vuole tentare di capire i ”meccanismi” che legano le molteplici dimostrazioni che sono alla base della matematica. Si vedrà come Gentzen, uno dei maggiori logici, abbia caratterizzato la struttura delle dimostrazioni introducendo il calcolo dei sequenti, in cui sono codificate le regole di tutta la logica matematica. Questo metodo sancisce la corrispondenza tra la composizione delle dimostrazioni di un enunciato e la cut-rule.

Sia L un linguaggio formale del primo ordine, un sequente è un’espressione Γ ⊢ Δ dove Γ e Δ sono sequenze finite di formule di L. Il sistema del calcolo dei sequenti si basa su delle regole che possono essere dvise in tre classi: le regole basilari che mettono in evidenza la dualità A, ¬A (A come ipotesi, A come conclusione). Tali regole sono la regola dell’identità e la cut-rule o regola del taglio. La seconda classe di regole è costituita dalle regole strutturali che mettono in evidenza formule senza considreare come esse siano costituite, sono la regola del weakening e la regola della contrazione. Le regole logiche costituiscono la terza classe di formule, esse concernono i simboli logici V (”vero”), F (”falso”), ∧ (”e”), ∨ (”o”), ∀ (”per ogni”), ∃ (”esiste”).

Le regole basilari sono le seguenti:

Regola dell’identità

\overline{⊢ ¬A, A}(id)

È un sequente valido: ”una fra A e ¬A è vera” può essere letta come: principio del terzo escluso, ”A è falsa oppure A è vera” principio di identità, ”dalla falsità di ¬A segue la verità di A”, ossia ”da A segue A” principio di non contraddizione, ”¬A e A non possono essere entrambe vere”.

Cut-rule o regola del taglio

\frac{⊢ Γ, A ⊢ ¬A, Δ}{⊢ Γ, Δ} (cut)

La regola del taglio può essere vista come una ”composizione” di due dimostrazioni, una avente la proposizione A fra le sue conclusioni e l’altra avente la stessa proposizione A fra le sue ipotesi: se una proposizione A è dimostrabile da certe ipotesi ¬Γ (A è conclusione), e se Δ è dimostrabile da A (A è ipotesi), allora Δ è dimostrabile da ¬Γ.

¬Γ A  ¬Γ
⋮ ⋮ ⟹ ⋮
A Δ  Δ

La dimostrazione di Δ da ¬Γ si ottiene componendo la dimostrazione di A da ¬Γ con la dimostrazione di Δ da A.

Le regole strutturali sono le seguenti:

Regola del weakening o regola dell’indebolimento

\frac{⊢ Γ}{⊢ Γ, A}(W)

La regola del weakening permette di aggiungere ipotesi ad una derivazione per ottenere le conclusioni, e di aggiungere conclusioni non ottenute dalle ipotesi.

Regola della contrazione

\frac{⊢ Γ, A, A}{⊢ Γ, A}(C)

La regola di contrazione permette di disinteressarsi di quante volte sia stata usata una stessa ipotesi in una dimostrazione, e di quante volte sia stata ottenuta una conclusione in una dimostrazione.

Le regole logiche sono le seguenti:

vero moltiplicativo

\overline{⊢ V} (V_{m})

vero additivo

\overline{⊢ Γ, V} (V_{a})

falso moltiplicativo

\frac{⊢ Γ}{⊢ Γ, F} (F_{m})

∧ moltiplicativa

\frac{⊢ Γ, A ⊢ B, Δ}{⊢ Γ, A ∧ B, Δ} (⊗)

∧ additiva

\frac{⊢ Γ, A ⊢ Γ, B}{⊢ Γ, A ∧ B} (&)

∨ additiva

\frac{⊢ Γ, A}{⊢ Γ, A ∨ B} (⊕1)

\frac{⊢ Γ, B}{⊢ Γ, A ∨ B} (⊕2)

∨ moltiplicativa

\frac{⊢ Γ, A, B}{⊢ Γ, A ∨ B} (℘)

Regola del ∀

\frac{⊢ Γ, A}{⊢ Γ, ∀xA}(∀) se x non libera in Γ

Regola del ∃

\frac{⊢ Γ, A[a]}{⊢ Γ, ∃xA[x]}(∃)

L’applicazione della cut-rule introduce dei problemi di ”purezza”: in logica classica si dice che una dimostrazione π :⊢ Γ è ”pura” quando ogni concetto presente ed usato nella prova è presente nella successione di proposizioni Γ. Tutte le regole ad eccezione della cut-rule fanno passare da dimostrazioni pure a dimostrazioni pure.

Questo non succede per la cut-rule infatti se π_{1} :⊢ Γ, A e π_{2} :⊢ ¬A, Δ sono dimostrazioni pure e alcuni concetti usati nelle dimostrazioni sono presenti soltanto nelle proposizioni A e ¬A, allora la dimostrazione ψ :⊢ Γ, Δ ottenuta mediante la cut-rule non è pura proprio perchè A e ¬A non sono presenti in Γ, Δ.

Tutte le regole, tranne la cut-rule, sono dette regole cut-free.

Gentzen, mediante il teorema di cut-elimination, per le proposizioni logiche che sono chiusura universale di formule del primo ordine, riesce a superare i problemi di purezza introdotti dalla cut-rule, questo teorema afferma che se ⊢ Γ è un sequente derivabile, allora ⊢ Γ è derivabile senza l’uso della cut-rule, cioè con una derivazione cut-free, ovvero con una derivazione pura.

Teorema (Cut-elimination) Esiste una procedura tale che data una derivazione π produce in un numero finito di passi una derivazione ψ cut-free tale che la conclusione di π è la conclusione di ψ; se π è senza regole strutturali anche ψ è senza regole strutturali.

Il teorema di cut-elimination, può essere considerato come un algoritmo, che da una dimostrazione di un sequente in cui viene utilizzata la cut-rule, fa passare alla dimostrazione dello stesso sequente senza l’utilizzo della cut-rule mediante le regole di riduzione.

Ma quale ruolo hanno la cut-rule e la cut-elimination nei risultati raggiunti dalla Logica Matematica? Si vede che il teorema di completezza sia strettamente legato alla cut-elimination. Infatti il teorema di completezza di Göedel afferma che le proposizioni logiche vere che sono chiusura universale di formule del primo ordine, sono sempre dimostrabili mediante una dimostrazione logica;

Teorema (Completezza) Sia A una formula del primo ordine, se ∀[A] è vera allora ∀[A] è dimostrabile logicamente.

Le stesse proposizioni, per il teorema di eliminabilità del taglio di Gentzen, sono sempre dimostrabili con dimostrazioni logiche pure:

Teorema Sia A una formula del primo ordine, se ∀[A] è dimostrabile logicamente allora ∀[A] è dimostrabile cut-free.

Quindi per le proposizioni logiche vere che sono chiusura universale di formule del primo ordine, si può affermare che esse sono dimostrabili logicamente e con dimostrazioni pure:

Sia A una formula del primo ordine, se ∀[A] è vera allora ∀[A] è dimostrabile cut-free.

D’altronde se esiste una dimostrazione logica (pura) di una proposizione, essa è sicuramente vera:

se esiste una dimostrazione logica pura (cut-free) di ∀[A] allora ∀[A] è vera.

Per cui si dimostra il seguente risultato che lega il teorema di completezza di Göedel e il teorema di eliminabilità del taglio di Gentzen:

Teorema Sia A una formula del primo ordine, ∀[A] è vera se e soltanto se esiste una dimostrazione logica pura di ∀[A].

Inoltre la presenza della cut-rule è strettamente legata alla dimostrazione di un altro teorema basilare, quello di compattezza. Tale teorema, in logica classica, afferma che se un insieme di formule chiuse di un linguaggio del primo ordine è finitamente soddisfacibile allora tale insieme è soddisfacibile. Il teorema di compattezza si può dimostrare seguendo due ragionamenti differenti; il primo si avvale del concetto di analisi canonica con cut, il secondo si basa sul concetto che ogni insieme di formule finitamente soddisfacibile può essere esteso a un insieme di formule finitamente soddisfacibile e massimale. L’applicazione della cut-rule corrisponde, nella seconda dimostrazione, al passaggio alla massimalità.

Il teorema di cut-elimination fornisce un vero e proprio algoritmo di trasformazione di una qualsiasi derivazione π di una formula del primo ordine chiusa universalmente in una derivazione ψ cut-free della stessa formula. Tale processo di trasformazione è deterministico se la derivazione π non contiene regole strutturali, infatti scelto il cut su cui agire, c’è una sola regola che si può applicare, e, qualora ce ne fossero più di una, esse traformano la derivazione π in una stessa derivazione. Mentre in presenza delle regole strutturali, il processo diviene non deterministico, infatti, nel caso in cui entrambe le premesse della cut-rule su cui si vuole agire sono state ottenute mediante la regola di contrazione o la regola del weakening, si possono applicare due regole di riduzione che danno luogo a derivazioni diverse, se, ad esempio, si considera la seguente derivazione:

\frac{\begin{aligned}⋮π_{1} & ⋮π_{2} \\ ⊢ Γ & ⊢ Δ \\ \overline{⊢ Γ, A}^{(W)} & \overline{⊢ ¬A, Δ}^{(W)} \end{aligned}}{\begin{matrix}⊢ Γ, Δ \\ ⋮π_{3} \end{matrix}} (cut)

applicando la regola di riduzione a destra, si ottiene la derivazione:

\begin{matrix}⋮π_{1} \\ ⊢ Γ \\ \overline{⊢ Γ, Δ} & (W) \\ ⋮π_{3} \end{matrix}

mentre, applicando la regola di riduzione a sinistra, si ottiene la derivazione:

\begin{matrix}⋮π_{2} \\ ⊢ Δ \\ \overline{⊢ Γ, Δ} & (W) \\ ⋮π_{3} \end{matrix}

differente da quella precedente.

Ciò non accade nella logica intuizionista e nella logica lineare. Per questo motivo si possono interpretare questi due frammenti della logica classica come metodi per rendere deterministico il processo di cut-elimination.

Nella logica intuizionista si perdono le concezioni della dualità e della simmetria concezioni base della logica classica perchè viene fissato un particolare punto di vista in modo che ciascuna formula è dichiarata positiva o negativa affinchè nessuna possa essere dichiarata sia positiva che negativa, vengono considerati solo i sequenti (detti ”intuizionisti”) in cui c’è una e una sola formula positiva (quindi le altre sono negative), infine vengono considerate solo le derivazioni nelle quali le regole sono applicate in maniera tale da far passare da sequenti intuizionisti a sequenti intuizionisti.

In questo modo si esclude il caso in cui entrambe le premesse della cutrule sono state ottenute mediante la regola di contrazione o la regola del weakening, infatti se A è la formula che viene tagliata ed è stata ottenuta mediante weakening o contrazione, allora la formula ¬A nell’altra premessa della cut-rule non può essere ottenuta mediante weakening o contrazione.

Sempre nell’ambito della logica intuizionista si mostra come il sistema della deduzione naturale, introdotto dallo stesso Gentzen, sia equivalente al sistema del calcolo dei sequenti.

L’idea di base della deduzione naturale è la seguente: una dimostrazione è una struttura ad albero con una o più ipotesi e una sola conclusione. Una deduzione è scritta come un albero finito, in particolare, le foglie dell’albero sono etichettate dalle formule, e le diramazioni dalle regole logiche. Si introduce inoltre il lambda calcolo tipato semplice, un linguaggio introdotto da Church negli anni ’30 in cui le ”parole” sono le ”formule di calcolo”. Il lambda calcolo consiste in una struttura di operazioni: l’”applicazione” che consiste nell’ applicare una formula f a un’altra formula x, l’astrazione λ, la β-riduzione che rappresenta l’esecuzione di un programma.

Per il frammento della logica intuizionista costituita dai soli connettivi ∧ e →, l’isomorfismo di Curry-Howard stabilisce una corrispondenza tra il sistema della deduzione naturale e il lambda calcolo tipato semplice, in questo modo nozioni della teoria della programmazione corrispondono a nozioni di teoria della dimostrazione.

Tramite tale isomorfismo, ciascun redex corrisponde a un cut nella deduzione naturale e ciascun cut in una deduzione naturale corrisponde a un redex; ciascuna regola di riduzione di un redex corrisponde a una regola di riduzione di un cut in una deduzione naturale e ciascuna regola di riduzione di un cut in una deduzione naturale corrisponde a una regola di riduzione di un redex; il teorema di cut-elimination corrisponde al teorema di normalizzazione (teorema che afferma la terminazione dell’esecuzione dei programmi).

Si illustra, poi, come la logica lineare renda deterministico il processo di trasformazione di una qualsiasi prova di una formula del primo ordine chiusa universalmente in una prova cut-free della stessa formula, ma senza perdere la concezione di dualità e di simmetria. Infatti in logica lineare le regole di riduzione divengono deterministiche mediante un ”raffinamento” della logica classica in modo da mantenere la dualità, e, dove ”raffinare” significa ”controllare le regole strutturali”. Si introducono due nuovi connettivi ”?” (”why not”) e ”!” (”of course”) detti connettivi esponenziali. L’idea è quella di controllare le formule su cui vengono applicate le regole strutturali ”etichettandole” con un ”?” per cui esse possono essere applicate solo sulle formule interrogate; si osservi che il duale di una formula interrogata è una formula esclamata:

(?A)^{⊥} = (!A^{⊥})

In questo modo si esclude il caso in cui entrambe le premesse della cutrule sono state ottenute mediante la regola di contrazione o la regola del weakening, infatti se ?A è stata ottenuta mediante weakening o contrazione ed è la formula tagliata dalla cut-rule, allora la formula !A^{⊥}, duale di ?A, nell’altra premessa della cut-rule non può essere ottenuta mediante weakening o contrazione in quanto non è una formula interrogata.

A conclusione di questo lavoro ci si è interrogati su cosa venga preservato nel processo di cut-elimination. Per rispondere a tale domanda, si introduce la nozione di ”spazio coerente”:

Definizione (Spazio coerente) X è uno spazio coerente se e soltanto se X è un grafo riflessivo e non orientato, ossia se e soltanto se X = (|X|, ⌣^{⌢}_{X}) dove |X| è un insieme detto supporto, e ⌣^{⌢}_{X} è una relazione binaria riflessiva e simmetrica su |X| (relazione di coerenza).

Gli elementi di uno spazio coerente sono detti ”cricche”:

Definzione (Cricca) Sia X uno spazio coerente. a è una cricca di X, si scrive a ⊑ X, se e soltanto se a ⊆ |X| e

∀x ∈ a ∀y ∈ a x ⌣^{⌢}_{X} y.

Si associa ad ogni formula A uno spazio coerente A^{∗}, ad ogni dimostrazione π di A una cricca π^{∗} dello spazio coerente A^{∗}. Se ψ è la derivazione cut-free di A ottenuta da π mediante il processo di cut-elimination, e ψ^{∗} è la cricca associata a ψ, allora si ottiene che

π^{∗} = ψ^{∗}

per cui la cricca viene preservata nel processo di cut-elimination.

Bibliografia

[1] V. M. Abrusci, ”Logica Matematica, corso introduttivo”, Edizioni Fratelli Laterza, 1992.

[2] V. M. Abrusci, ”L’arte di dimostrare che la forma è sostanza”, Il Sole 24 Ore, 28 Novembre 1999.

[3] V. M. Abrusci, ”Logica Matematica”, Anno Accademico 2000-2001.

[4] V. M. Abrusci, ”Corso di Logica”, Anno Accademico 2002-2003.

[5] J. Bell, M. Machover, ”A course in Mathematical Logic”, North Holland, 1997.

[6] ”Il teorema di Goedel”, a cura di F. M. Bianchi.

[7] C. Cellucci, ”La naturalizzazione della logica e della matematica”.

[8] ”Uomo-macchina”, Clarence News.

[9] M. Dummett, ”Viaggio al principio della mente”, Il Corriere della Sera, 13 Gennaio 2002.

[10] ”Enciclopedia Garzanti di Filosofia”, Garzanti Editore, 1993.

[11] J. Y. Girard, ”Proof theory and logical complexity, Vol.1”, Bibliopolis, 1987.

[12] J. Y. Girard, P. Taylor, Y. Lafont, ”Proof and types”, Cambridge University Press, 1989.

[13] J. Y. Girard, ”Linear Logic: its syntax and semantics”.

[14] J. Y. Girard, ”Linear Logic”.

[15] E. Giusti, ”Analisi Matematica 1”, Bollati Boringhieri, 1996.

[16] J. Laird, ”A deconstruction of Non-deterministic Classical Cut Elimination”.

[17] R. Laurenti, ”Aristotele: la logica”.

[18] A. Maffini, ”Le basi dell’analisi non-standard”.

[19] A. Massarenti, ”Omaggio a Goedel”, Il Sole 24 Ore, 28 Novembre 1999.

[20] G. di Nola, ”Calcolo proposizionale”.

[21] P. S. Novikov, ”Elementi di Logica Matematica”, Editori riuniti.

[22] G. Sambin, ”Una guida alla logica”.

[23] A. Selleri, ”Il teorema di Goedel”.

[24] E. Sernesi, ”Geometria 2”, Bollati Boringhieri, 1996.

[24] ”Ingegneria del software”, a cura dell’università di Brescia, 1998-1999.

[25] ”Logica proposizionale”, a cura dell’università di Parma.