Ludics

From Girard Reading Group

A purely interactive approach to logic. Detailed in Locus Solum by Jean-Yves Girard.

Treats the location, or locus, of a subformula as more important more important than the actual subformula. Sequents of a restricted form made from loci are called pitchforks. Proofs constructed by paying attention to the loci rather than the subformulae are called designs.

Attempts to provide a logic of inference rules. A form of design that looks familiarly like a proof of a sequent calculus is a dessin. However, a dessin is not abstract enough and so Girard replaces them by the more abstract and less familiar looking dessein. At this abstract level, the pitchforks themselves no longer matter and only the inference rules used are left. That is, the inference rule applied at each step contains all the information needed to characterize that step; the actual pitchfork in the premise or conclusion does not matter. In this way, it is logic of inference rules.

This work has its roots in Girard's work on the logic LU.

[edit] External links

• "Introduction to ludics" by Pierre-Louis Curien (slides).

• "Sérieuse ludique…" by Alain Lecomte (non-technical article, in French).