Michele Basaldella (RIMS, Japan), A gentle introduction to ludics
Schedule
- Feb. 9, 2012, 15:30 - 16:15
Abstract
When one is interested in understanding the duality between syntax
(proofs) and semantics (models) in logic, a primary obstacle is that
proofs are finite and concrete objects, while models are infinite and
abstract structures. Since proofs and models are so different by their
nature, they hardly interact together.
This lack of interaction between the two worlds prevents a deeper
analysis of the relations between syntax and semantics.
Ludics is a research program started by Girard aimed to explain various
logical and computational phenomena from an interactive point of view. The
universe of ludics consists of designs: partial and
infinitary proofs in which the logical type-information has been almost
erased. In this vast universe, both proofs and models can be
homogeneously represented as designs. Moreover, since designs come from
proofs, we can make them interact together via normalization
(cut-elimination). This induces an orthogonality relation, based on the
termination of the computation of the normal form, which allows to
reconstruct the logical types, as bi-orthogonality-closed sets of designs.
In this talk we introduce and discuss the basic concepts of ludics and
show some completeness results for proofs.
When one is interested in understanding the duality between syntax (proofs) and semantics (models) in logic, a primary obstacle is that proofs are finite and concrete objects, while models are infinite and abstract structures. Since proofs and models are so different by their nature, they hardly interact together. This lack of interaction between the two worlds prevents a deeper analysis of the relations between syntax and semantics.
Ludics is a research program started by Girard aimed to explain various logical and computational phenomena from an interactive point of view. The universe of ludics consists of designs: partial and infinitary proofs in which the logical type-information has been almost erased. In this vast universe, both proofs and models can be homogeneously represented as designs. Moreover, since designs come from proofs, we can make them interact together via normalization (cut-elimination). This induces an orthogonality relation, based on the termination of the computation of the normal form, which allows to reconstruct the logical types, as bi-orthogonality-closed sets of designs.
In this talk we introduce and discuss the basic concepts of ludics and show some completeness results for proofs.