Una semantica per la logica lineare

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.