Benvenuto
Gruppo di Logica e Geometria della Cognizione
coordinatore: V. Michele Abrusci

 

Dipartimento di Filosofia
Università di Roma Tre
Via Ostiense 234
00144 Roma -Italia

 

Il fondamento scientifico della costituzione del gruppo risiede nell'interesse che tutti i suoi componenti portano alla moderna teoria della dimostrazione. Questo settore della logica matematica ha conosciuto recentemente una vera e propria "rinascita", dovuta al suo incontro con l'informatica: la corrispondenza di Curry-Howard stabilisce una corrispondenza tra dimostrazioni e programmi e tra esecuzione dei programmi ed eliminazione del taglio (un procedimento di trasformazione delle dimostrazioni ben noto ai logici). La scoperta di questa semplice e fondamentale corrispondenza è il punto di partenza per un nuovo approccio alla nozione di costruttività in logica ed alla programmazione in informatica.

In quest'ambito si colloca l'apparizione della logica lineare, che unisce gli aspetti "costruttivi" della logica intuizionista alle simmetrie della logica classica. La logica lineare nasce da un'analisi matematica molto fine della semantica delle dimostrazioni della logica intuizionista. Dalla sua apparizione nel 1986, essa si è imposta come strumento usato in vari settori di ricerca, dalla teoria della dimostrazione al lambda-calcolo, dalle macchine astratte al calcolo distribuito, dalla teoria della complessità alla programmazione logica.


News

Dimostrazioni e tipi nella logica del secondo ordine

Speaker:
Paolo Pistone (Università Roma Tre/Aix-Marseille Université)
Quando:
06/02/2015 - 11:30
Dove:
Dipartimento di Matematica e Fisica, Aula Seminari 311 largo San L. Murialdo 1 - Roma
Abstract

In questo intervento, che ripercorre alcuni contenuti della mia tesi di dottorato, saranno esaminate alcune forme di « circolarità » che appaiono nella teoria della dimostrazione della logica del secondo ordine e della sua controparte costruttiva, il Sistema F.
Queste circolarità, o « circoli viziosi » (Poincaré 1906), saranno analizzate sulla base della distinzione tra due punti di vista corrispondenti a metodologie distinte e irriducibili (a causa dei teoremi di incompletezza): il primo (« le pourquoi », Girard 2000) é focalizzato sulla questione della coerenza e dell’Hauptsatz e richiede dei metodi di dimostrazione infinitari (ovvero non elementari). Il secondo (« le comment », Girard 2000) é focalizzato sul contenuto computazionale e combinatorio delle dimostrazioni, dato dalla corrispondenza tra prove e programmi, e non richiede che metodi elementari di dimostrazione.
Questa distinzione metodologica permette di mettere in luce nel dettaglio le limitazioni epistemologiche a cui va incontro la logica del secondo ordine (cosa può essere deciso in modo elementare, ovvero con certezza? Cosa invece non può mai essere stabilito al di là di ogni ragionevole dubbio?)


Verso una teoria del dialogo in Ludica

Speaker:
Francesca Ferrante (Université Aix-Marseille & “Resurgences” )
Quando:
23/01/2015 - 11:30
Dove:
Dipartimento di Matematica e Fisica, Aula Seminari 311 largo San L. Murialdo 1 - Roma
Abstract

La Ludica è un programma di ricerca iniziato da J.-Y. Girard nel 2001 allo scopo di fornire un fondamento della logica basato sull'interazione. Attualmente, diversi studi sono condotti, che guardano alla ludica come un modello computazionale del linguaggio naturale e, in particolare, del dialogo. Lo scopo del seminario sarà introdurre gentilmente – anche attraverso qualche esempio - a questo campo della ricerca.


Stati Entangled e Matrici di Bell

Speaker:
Silvia Rognone (Università Roma Tre)
Quando:
19/12/2014 - 11:30
Dove:
Aula 310, Dipartimento di Matematica e Fisica, Largo S. Leonardo Murialdo 1
Abstract

Richard Feynman fu il primo pensatore a percepire la necessità di ampliare il concetto di computer in base
alla teoria della meccanica quantistica. Se la realtà in cui viviamo è descritta in maniera più efficace dalla
teoria quantistica piuttosto che dalla classica, non dovrebbe essere così anche per i simulatori della realtà, i computer?

Saranno presentate le basilari nozioni di qubit (la cella di informazione quantistica) e di porte logiche quantistiche
(unarie e binarie), mostrando una panoramica generale sui circuiti quantistici, sul fenomeno dell’entanglement
e sul concetto di separabilità. Si discuteranno la definizione e le proprietà di una particolare famiglia di matrici,
le matrici di Bell, in grado di implementare l'operazione logica di entanglement.

In particolare, si mostrerà come, dal circuito che genera coppie EPR, si sia arrivati alla scoperta della porta binaria di Bell;
infine, tramite una definizione ricorsiva, si presenterà l'agoritmo che genera matrici di Bell che intrecciano fino ad n-qubit.


Sulla Sintassi Trascendentale

Speaker:
Arnaud Valence (Università Roma Tre/Université Lyon 3)
Quando:
21/11/2014 - 11:30
Dove:
Dipartimento di Matematica e Fisica, Aula Seminari 311 largo San L. Murialdo 1 - Roma
Abstract

La storia della teoria della dimostrazione rivela un lento processo di adattamento della sintassi alla semantica e della semantica alla sintassi. Questo processo è la manifestazione della sintassi-trascendentale-come-gioco-dinamico. Con la “GoI VI” (“Geometry of Interaction VI”), la sintassi e la semantica sembrano giungere ad un punto di convergenza decisivo dove la sintassi è libera. Questo fenomeno è la manifestazione della sintassi-trascendentale-come-framework. Nel seminario saranno presentati i principali aspetti della sintassi trascendentale nelle sue due accezioni.


Dai grandi teoremi della logica del XX secolo alla Sintassi Trascendentale

Speaker:
V. Michele Abrusci (Università Roma Tre)
Quando:
07/11/2014 - 11:30
Dove:
Dipartimento di Matematica e Fisica, Aula Seminari 311 largo San L. Murialdo 1 - Roma
Abstract

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 sviluppare la logica matematica ed affrontare sistematicamente tali questioni.


Seminario sui fondamenti

Speaker:
Vito Michele Abrusci
Quando:
31/10/2014 - 09:00
Dove:
Dipartimento di Matematica e Fisica, Largo S. Leonardo Murialdo 1, palazzina C, aula 311
Abstract

Saranno sviluppati e approfonditi alcuni temi trattati da Jean-Yves Girard nel suo seminario al Colloquium di Matematica, 8 ottobre 2014


Seminario sui fondamenti

Speaker:
Vito Michele Abrusci
Quando:
24/10/2014 - 09:00
Dove:
Dipartimento di Matematica e Fisica, Largo S. Leonardo Murialdo 1, palazzina C , aula 311
Abstract

Saranno sviluppati e approfonditi alcuni temi trattati da Jean-Yves Girard nel suo seminario al Colloquium di Matematica, 8 ottobre 2014


String diagrams e categorie: dimostrazione della coerenza delle categorie monoidali simmetriche tramite riscrittura

Speaker:
Matteo Acclavio (Aix-Marseille Université)
Quando:
24/10/2014 - 11:30
Dove:
Dipartimento di Matematica e Fisica, Largo S. Leonardo Murialdo, palazzina C, Aula 311
Abstract

Una categoria monoidale simmetrica è una categoria munita di un prodotto (binario) associativo e commutativo e di un oggetto che rappresenta l'unità per questo prodotto. Queste proprietà sono soddisfatte modulo isomorfismi naturali che verificano delle condizioni di coerenza. Il teorema di coerenza afferma la commutatività di tutti i diagrammi (lineari) costituiti da questi isomorfismi.
Dopo un'introduzione agli string diagrams e alla riscrittura, dimostreremo il teorema di coerenza provando la convergenza del sistema di riscrittura di Y. Lafont e usando questo per costruire una base dell'omotopia tramite la quale verificare la commutatività di ogni diagramma in una categoria monoidale simmetrica.


Analytique/synthétique, a priori/a posteriori: une relecture du typage

Speaker:
Jean-Yves Girard
Quando:
10/10/2014 - 11:00
Dove:
Dipartimento di Filosofia, Comunicazione, Spettacolo, Università Roma Tre, via Ostiense 234, Roma. Aula Verra (piano terra)
Abstract

En termes kantiens, l’objet nu et son type, c’est analytique/synthétique.

L’analytique est ce qu’il reste quand on a évacué le sens, ie, l’engagement : tout est sur la table. Il se décline en constatatif (incrémental) et performatif (destructif). Le paradigme d’unification permet de représenter le performatif sans agent extérieur.

Le synthétique est ce qui donne le sens à l’analytique ; engagé, il est soumis au doute. Il se divise en deux branches. L’a posteriori ou format, qui donne un sens à l’analytique constatatif, consiste à passer des sortes de tests de sortie d’usine, comme dans les réseaux de démonstration : c’est le sens comme question.
L’a priori ou socialisation donne un sens à l’analytique performatif, c’est ici que s’insinue le doute fondationnel : c’est le sens comme usage.

Les deux synthétiques sont les deux façons de dire « A est A » : axiome (a posteriori) et coupure (a priori), rallonge entre deux prises opposées vs raccordement de prises. Alors que la rallonge n’est pas soumise au doute, le branchement est problématique, dangereux. Y a-t-il équilibre entre les droits (la prise comme sortie) et les devoirs (sa prise opposée comme entrée) ?

Le synthétique a posteriori est formulable à travers une sorte d’analytique non déterministe. L’objet mathématique se présente finalement comme une épure, une combinaison véhicule (analytique) + gabarit (synthétique). Le synthétique a priori combine les épures selon leurs gabarits, leurs types ; et il n’y a pas de certitude absolue, légitime, quant à ces combinaisons.

Techniquement parlant, le passage aux épures devrait répondre à un certain nombre de questions irritantes, comme celle de trouver des habitants au type vide : ce seraient des entités qui ne séparent pas nettement l’objet et le sujet.


Colloquium di matematica: Foundations in the post-foundational era

Speaker:
Jean-Yves Girard
evento esterno
Quando:
08/10/2014 - 16:00
Dove:
Dipartimento di Matematica e Fisica, Università Roma Tre, Largo S. Leonardo Murialdo 1, Aula F (blocco delle aule, primo piano)
Abstract

Most philosophers won’t hesitate to nominate 2+2=4 as the paragon of a mathematical theorem : a complete misunderstanding.

We can either see 2+2=4 as a computation, i.e., an activity not involving any sense, any reasoning : analytic in the kantian acception. Or we can see 2+2=4 as the result of a reasoning — hence synthetic — however based on experience : everything can be checked, there is no room for doubt. This synthetic a posteriori is not typical of mathematics, which is naturally synthetic a priori. This means that mathematics cannot be justified — hence the failure of the foundational programs of a century ago.

If these programs didn’t succeed in alleviating our — however, unreasonable — doubts, they however individuated, inside mathematics, a synthetic a posteriori layer. This on a large scale, not limited to finite computations. How is it possible to deal with infinity and still be based on experience ? And what does this mean ?