Linear Realisability and Implicative Algebras

TL;DR

This paper establishes a formal connection between linear realizability models and classical realizability constructions, using implicative algebras to unify various logical frameworks and their computational interpretations.

Contribution

It introduces a linear decomposition of implicative algebras, linking linear realizability models with Kleene and Krivine's realizability frameworks for the first time.

Findings

Linear realizability models are shown to be concrete examples of implicative algebra decompositions.

A formal link between linear realizability and classical realizability is established.

The work unifies various realizability models under a common linear framework.

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.