First order in Ludics
Marie-Renée Fleury, Myriam Quatrini · Mathematical Structures in Computer Science · 2004
In Girard (2001), J.-Y. Girard presents a new theory, The Ludics, which is a model of realisibility of logic that associates proofs with designs, and formulas with behaviours. In this article we study the interpretation in this semantics of formulas with first-order quantifications and their proofs. We extend to the first-order quantifiers the full completeness theorem obtained in Girard (2001) for . A significant part of this article is devoted to the study of a uniformity property for the families of designs that represent proofs of formulas depending on a first-order free variable.