Linear Realisability and Implicative Algebras
Alexandre Lucquin, Luc Pellissier, Thomas Seiller
TL;DR
This work formalizes a deep link between linear realizability models (as studied in geometry of interaction, ludics, and interaction graphs) and Kleene/Krivine realizability by embedding linear realizability into Miquel’s implicative algebras. It shows that linear realizability models naturally yield linear implicative algebras, and develops a robust interpretation of multiplicative, additive, and exponential fragments within this framework, including quotient constructions and a fixpoint-based exponentials approach. By connecting linear realizability to tripos-to-topos constructions and topos theory, the paper suggests a path toward a linear tripos and a decomposition of logical and categorical structures across intuitionistic and classical realizability. The results unify several realizability traditions and offer a structured method to analyze and extend linear realizability models across a broad logical spectrum, with potential applications to semantic decompositions of models in set theory and beyond.
Abstract
Realizability, introduced by Kleene, can be understood as a concretization of the Brouwer-Heyting-Kolmogorov (BHK) interpretation of proofs, providing a framework to interpret mathematical statements and proofs in terms of their constructive or computational content. Over time, this concept has evolved through various extensions, such as Kreisel's modified realizability or Krivine's classical realizability. Parallel to these developments, Girard's work on linear logic introduced another perspective, often seen as another concrete realization of the BHK interpretation. The resulting constructions, encompassing models like geometry of interaction, ludics, and interaction graphs, were recently unified under the term linear realizability models to stress the intuitive connection with intuitionnistic and classical realizability. The present work establishes for the first time a formal link between linear realizability models and the realizability constructions of Kleene and Krivine. Our approach leverages Miquel's framework: just as linear logic can be viewed as a decomposition of intuitionistic and classical logic, we propose a linear decomposition of implicative algebras and show that linear realisability models provide concrete examples of such decompositions.