In this work we provide an alternative, and equivalent, formulation of the concept of λ-theory without introducing the notion of substitution and the sets of all, free and bound variables occurring in a term. We call α β-relations our alternative versions of λ-theories. We also clarify the actual role of α-renaming in the lambda calculus: it expresses a property of extensionality for a certain class of terms. To motivate the necessity of α-renaming, we construct an unusual denotational model of the lambda calculus that validates all structural and beta conditions but not α-renaming. The article also has a survey character.

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.

We prove that is possible to extend Girard's Ludics so as to have repetitions (hence exponentials), and still have the results on semantical types which characterize Ludics in the panorama of Game Semantics. The results are obtained by using less structure than in the original paper; this has an interest on its own, and we hope that it will open the way to applying the approach of Ludics to a larger domain.