Questo sito utilizza cookie di terze parti per inviarti pubblicità in linea con le tue preferenze. Se vuoi saperne di più clicca QUI 
Chiudendo questo banner, scorrendo questa pagina, cliccando su un link o proseguendo la navigazione in altra maniera, acconsenti all'uso dei cookie. OK

Una semantica per la logica lineare

Questo lavoro vuole essere una descrizione minuziosa degli strumenti algebrici che ci permettono di costruire una semantica di tipo tarskiano della logica lineare (ideata da Girard).
Non è sicuramente innovativo a riguardo, ma lo possiamo definire organizzativo ed esemplificativo di una serie di procedure studiate e descritte da logici contemporanei, tra cui vanno sottolineati A.S. Troelstra ed H. Ono.
Dopo una prima parte introduttiva sulla sintassi della logica lineare, nella seconda parte del lavoro si passa a descrivere strutture algebriche via via più complesse che alla fine ci permetteranno di interpretare adeguatamente il sistema formale e di dimostrare la completezza semantica.
Aspetto da sottolineare è che vengono fornite le dimostrazioni, in modo oserei dire pedante, di tutto ciò che viene affermato: poco è lasciato come dimostrazione per il lettore.
Quindi nella seconda parte si descrivono le proprietà, in ordine:
dei Monoidi;
dei Reticoli;
delle IL-algebre, e l'equivalenza con i Quantali;
delle CL-algebre;
e delle CLM-algebre.

Mostra/Nascondi contenuto.
4 Introduzione La logica lineare è stata elaborata da J. Y. Girard intorno al 1986/7 e, dopo la sua formulazione, si è manifestata subito come proficuo campo di studio, e soprattutto, strumento utilizzabile in diversi ambiti del sapere. La sua costruttività sommata all'accresciuta esp ressività rispetto alle logiche tradizionali ne fa uno strumento molto utilizzato in informatica, e il suo valore ep istemico ne permette l'ut ilizzo in tentativi di formalizzare scienze non solo matematiche. Il nostro lavoro tralascia completamente ogni risvolto strumentale della logica lineare per fissare l'attenzione sullo strumento stesso e darne una descrizione logica, e soprattutto, descrivere minuziosamente una semantica di tipo tarskiano per cui si dimostra la completezza semantica. La prima parte del lavoro sarà una presentazione sintattica di un sistema formale: CLL. CLL è un calcolo dei sequenti alla Gentzen per la logica lineare classica o semplicemente logica lineare. La seconda parte provvederà a descrivere una classe, K, di strutture isomorfe a CLL per cui un sequente S è dimostrabile in CLL se e solo se la sua interpretazione è vera in tutte le strutture di K. 1. Logica lineare, cenni storici. L'ambito di ricerca in cui nasce e si sviluppa la logica lineare è quello della semantica della dimostrazione, e precisamente dal lavoro di rigorizzazione della semantica di Heyting per la logica intuizionista compiuto da Girard. Intorno al 1985 Girard elabora una semantica della dimostrazione per la logica intuizionista basata sugli spazi coerenti e le funzioni stabili. Una p roposizione viene associata ad uno spazio coerente che è una particolare classe di insiemi e rappresenta l'insieme delle dimostrazioni della proposizione; e le dimostrazioni formali dalle assunzioni alla conclusione sono interpretate con funzioni cosiddette stabili che vanno da spazi coerenti a spazi coerenti.

Tesi di Laurea

Facoltà: Lettere e Filosofia

Autore: Santo Scaramuzzo Contatta »

Composta da 102 pagine.

 

Questa tesi ha raggiunto 1549 click dal 20/03/2004.

 

Consultata integralmente una volta.

Disponibile in PDF, la consultazione è esclusivamente in formato digitale.