Infinitary Completeness in Ludics

Traditional Gödel completeness holds between finite proofs and infinite models over formulas of finite depth, where proofs and models are heterogeneous. Our purpose is to provide an interactive form of completeness between infinite proofs and infinite models over formulas of infinite depth (that include recursive types), where proofs and models are homogenous. We work on a nonlinear extension of ludics, a monistic variant of game semantics which has the same expressive power as the propositional fragment of polarized linear logic. In order to extend the completeness theorem of the original ludics to the infinitary setting, we modify the notion of orthogonality by defining it via safety rather than termination of the interaction. Then the new completeness ensures that the universe of behaviours (interpretations of formulas) is Cauchy-complete, so that every recursive equation has a unique solution. Our work arises from studies on recursive types in denotational and operational semantics, but is conceptually simpler, due to the purely logical setting of ludics, the completeness theorem, and use of coinductive techniques.