Gruppo di Logica e Geometria della Cognizione

Classical realizability is a technique for extracting computational content from classical proofs. It was introduced by Krivine in the middle of the 1990's combining ideas from traditional Kleene realizability and from logical translations from classical to intuitionistic logics. Its fundamental contribution is to put the notion of interaction (between a proof and a counter-proof, or between a program and its environment) in a central position explicitly. Subsequently, it provides enlightening descriptions of the computational behaviour of classical tautologies as synchronization mechanisms between threads of a program.

In this talk, I will survey the fundamental ideas that lead to the interactive study of proofs with the tools of classical realizability, in the original framework of the ?-calculus with control operators. I will show how these ideas relate to other models for proof systems (games, ludics…), how it can be extended to other models of computation and what it can teach us about the ongoing question of the proof-program correspondence for concurrent computation.

Saranno presentate e discusse alcune questioni filosofiche connesse con la piena comprensione dei principali teoremi della logica del XX secolo (teorema di completezza della logica del primo ordine, teorema di eliminazione del taglio dalle dimostrazioni logiche del primo ordine, teoremi di incompletezza di Goedel, .. ) e sarà mostrato come la Sintassi Trascendentale sia un nuovo programma di ricerca per lo sviluppo della logica matematica che mira ad affrontare sistematicamente tali questioni.

Un sistema di riscrittura è dato da un insieme di oggetti e delle relazioni per trasformarli.
I primi string rewriting system furono introdotti nel 1917 cercare per risolvere il problema della parola per i semigruppi finitamente presentati. In seguito allo sviluppo della teoria della calcolabilità, si dimostrò che rappresentavano un modello di calcolo Turing-completo, permettendo di affermare l'indecidibilità del problema della parola.
Obiettivo dell'incontro sarà dimostrare il teorema di Squier che permette di caratterizzare geometricamente delle interessanti proprietà computazionali di un monoide.

La teoria delle lenti (Hancock, Ordinals and Interactive Programs, 2000) formalizza la corrispondenza intuita da Gentzen, che associa ai tipi su cui un sistema formale può applicare il principio di induzione le funzioni rappresentabili (equivalentemente, i buoni ordini provabili) nel sistema. La generalizzazione di tale corrispondenza, attraverso alcuni concetti e risultati provenienti dalla teoria dei dilatatori, fornisce una prospettiva "dinamica" per lo studio della teoria impredicativa dei tipi (sistema F).

Giovedì 20 giugno in Aula Verra (Dipartimento di Filosofia, Via Ostiense, 234) si terranno le discussioni delle due seguenti tesi di dottorato:

1) Alle ore 14:00, tesi di Andrei Dorman (cotutela Roma Tre-Paris 13), dal titolo "Concurrency in Interaction Nets and Graph Rewriting"
Drettori di tesi:
L. Tortora de Falco (Roma Tre)
D. Mazza, S. Guerrini (Paris 13)
Commissione: F. Gadducci (Pisa), S. Guerrini (Paris 13), D. Hirschkoff (Ecole Normale Supérieure Lyon), C. Laneve (Bologna), D. Mazza (CNRS-Paris 13), L. Tortora de Falco (Roma Tre)
Referee: C. Palamidessi (INRIA, école Polytechnique), M. Fernandez (King's College London)

2) Alle ore 16:00, tesi di Giulio Guerrieri (cotutela Roma Tre-Paris 7), dal titolo "Differential nets, experiments and reduction"
Drettori di tesi:
L. Tortora de Falco (Roma Tre)
T. Ehrhard (Paris 7)
Commissione: V. M. Abrusci (Roma Tre), D. Mazza (CNRS-Paris 13), T. Ehrhard (CNRS-Paris 7), L. Tortora de Falco (Roma Tre)
Referee: M. Fiore (Cambridge), L. Regnier (IML-Université Aix-Marseille)

Per l'occasione, si terrà venerdì 21 giugno dalle 10 alle 14 in aula 009 (presso il Dipartimento di Matematica e Fisica, Largo S. Leonardo Murialdo, 1) un workshop informale sulle tematiche delle due tesi di dottorato, con interventi dei membri delle commissioni e successiva discussione aperta.

Per ulteriori informazioni:
tortora@uniroma3.it

A cura del gruppo di ricerca in "Logica e Geometria della Cognizione" diretto dal prof. V. Michele Abrusci, e in collaborazione con il prof. Riccardo Chiaradonna (docente di Storia della Filosofia Antica), si terrà un seminario di studio su una rilettura dei "Topici" di Aristotele alla luce di alcuni contributi della ricerca logica contemporanea.

Programma.
V. Michele Abrusci: Sillogismo, sillogismo dimostrativo, sillogismo dialettico
Francesca Romana Ferrante: Lettura e commento di alcuni "luoghi" dei Topici di Aristotele
Riccardo Chiaradonna: Logica e Dialettica
Francesca Romana Ferrante: Rappresentazione di alcuni "luoghi" dei Topici di Aristotele entro la Ludica di J.-Y. Girard

Oggetto del seminario sarà un "tutorial" sulla GoI6 (ovvero la sesta, più recente, versione
della Geometria dell'Interazione), frutto del lavoro dei precedenti incontri del
laboratorio.

Diagrams form a 2-dimensional formal language generalizing words and
terms. Moreover, it is possible to rewrite them. We shall consider
some examples. In particular, we get a refinement of matrix calculus.