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

Aspetti computazionali della negazione: dal lambda-calcolo di Church alla Logica Lineare.

Speaker:
Jean-Baptiste Joinet (Université Lyon 3)
Quando:
19/05/2015 - 12:00
Dove:
Scuola di Lettere, Filosofia e Lingue, via Ostiense 234, Aula 15
Abstract


Beyond Logic

Organizzatori:
"Beyond Logic, Hypothetical Reasoning in Philosophy of Science, Informatics, and Law", joint French-German research project funded by ANR and DFG;
Gruppo di Logica e Geometria della Cognizione, Università Roma Tre
Inizio:
21/05/2015
Fine:
22/05/2015
Dove:
Dipartimento di Matematica e Fisica, Largo S. Leonardo Murialdo 1
Descrizione

Program:

Thursday, May 21, 2015

“Aula F”

15:00-16:00 Luiz Carlos Pereira (PUC Rio de Janeiro)
Translations: a view from proof-theory

16:15-17:15 Cesare Cozzo (Sapienza Univ. Roma)
Dummett on inference

17:30-18.30 Arnaud Valence (Univ. Roma Tre)
Dewey's Logic Revisited

20:00 Dinner

Friday, May 22, 2015

“Aula 311”

9.30-10.30 Jean Fichot (IHPST, Univ. Paris 1)
Principles(s) of conservativity

10:45-11:45 Jean-Baptiste Joinet (Univ. Lyon 3)
Actional processes, individuals and identity criteria

12:00-13:00 Paolo Pistone (Univ. Roma Tre & Aix-Marseille Univ.)
Untyped validity: completeness through parametricity

13:15 Lunch (“Sala riunioni”)

“Aula 211”

15:00-16:00 Maël Pégny (IHPST, Univ. Paris 1)
Constructivity and the Church-Turing thesis

16:15-17:15 Thomas Piecha (Univ. Tübingen)
Inversion of logical rules

17:30-18:30 Peter Schroeder-Heister (Univ. Tübingen)
Proof-theoretic semantics and the sequent calculus

20:00 Dinner

Local organizers: V. Michele Abrusci and Paolo Pistone
Further informations: http://ls.informatik.uni-tuebingen.de/bl/project.html


Dimostrazioni e tipi nella logica del secondo ordine (seconda parte)

Speaker:
Paolo Pistone (Università Roma Tre/Aix-Marseille Université)
Quando:
20/03/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?)


"Proofs and types", 25 years later

Organizzatori:
Gruppo di Logica e Geometria della Cognizione
HYPOTHESES, Hypothetical Reasoning – Its Proof-Theoretic Analysis, joint French-German research project funded by ANR and DFG
Inizio:
26/03/2015
Fine:
28/03/2015
Dove:
Dipartimento di “Filosofia, Comunicazione, Spettacolo", Scuola di "Lettere, Filosofia, Lingue” (ex Facoltà di Lettere e Filosofia), via Ostiense 234.
Descrizione

The publication, twenty-five years ago, of the by now classical textbook "Proofs and Types" (Girard, Lafont, Taylor 1989) marked the consolidation of the tradition arising from the Curry-Howard connection between logic (natural deduction) and theoretical computer science (typed lambda calculi).
Many developments and extensions of this connection have been investigated in the last years (by means of linear logic, abstract machines, geometry of interaction, ludics, just to name some directions of research), providing at the same time several theoretical challenges to the original Curry-Howard paradigm.
Then, some important questions related to logic and philosophy naturally arise, e.g. the following two questions:
1) What has the correspondence between logic and computation evolved into during these years?
2) What was the impact of this tradition on the philosophical investigations on the foundations of logic and mathematics?

Program:

Thursday, 26 March, Aula Verra (ground floor)

15 :30-16 :15 Wagner de Campos Sanz (Universidade de Goiás, Brasil)
TBA

16 :15-17 :00 Giulio Guerrieri (PPS, Univ. Paris 7)
Injectivity of relational semantics for connected MELL proof-structures via Taylor expansion

17 :00-17 :15 Coffee break

17 :15-18 :00 Jean Fichot (IHPST, Univ. Paris 1)
May Falsum be true?

Friday, 27 March, Aula Verra (ground floor)

9 :00-10 :15 Jean-Yves Girard (I2M, Aix-Marseille Univ.)
La surprenante syntaxe transcendantale du calcul des prédicats

10 :30-13 :30 Defense of Paolo Pistone’s thesis
On proofs and types in second order logic

13 :30-15 :30 Lunch (foyer next to the Aula Magna)

15 :30-16 :15 Pierre-Louis Curien (PPS, Univ. Paris 7)
Curry-Howard correspondence, abstract machines, sequent calculus, and classical logic

16 :15-17 :00 Jean-Baptiste Joinet (Univ. Lyon 3)
On the « primitive » distinction Individual/Predicate

17 :00-17 :15 Coffee break

17 :15- 18 :00 Pierre Livet (Aix-Marseille Univ.)
Epistemic circularity: self-justification versus self-application; meaning as the source of use or computational functioning as the regulation of impredicativity?

Saturday, 28 March, Aula Verra (ground floor)

9 :30-10 :15 Alain Lecomte (Univ. Paris 8)
Ludics and philosophy of language: from literal meaning to dialogue modeling

10 :15-10 :30 Coffee break

10 :30-11 :15 Marco Pedicini (Univ. Roma Tre)
Sequential and parallel abstract machines for optimal reduction

11 :15 -12 :00 Vito Michele Abrusci (Univ. Roma Tre)
Logic, first-order logic, second-order logic in Hilbert’s logical school (1920-1940): some historical remarks


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