Michele Basaldella (RIMS, Japan), A gentle introduction to ludics


  • Feb. 9, 2012, 15:30 - 16:15


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.