Implicative algebras: a new foundation for realizability and forcing

TL;DR

This paper introduces implicative algebras as a unified algebraic framework that captures the essence of forcing and realizability models in logic, bridging proofs and types.

Contribution

It defines implicative algebras and demonstrates they induce triposes that encompass all known forcing and realizability models in logic.

Findings

Implicative algebras induce Set-based triposes.

All forcing and realizability triposes are encompassed by implicative triposes.

The structure unifies models in intuitionistic and classical logic.

Abstract

We introduce the notion of implicative algebra, a simple algebraic structure intended to factorize the model constructions underlying forcing and realizability (both in intuitionistic and classical logic). The salient feature of this structure is that its elements can be seen both as truth values and as (generalized) realizers, thus blurring the frontier between proofs and types. We show that each implicative algebra induces a (Set-based) tripos, using a construction that is reminiscent from the construction of a realizability tripos from a partial combinatory algebra. Relating this construction with the corresponding constructions in forcing and realizability, we conclude that the class of implicative triposes encompass all forcing triposes (both intuitionistic and classical), all classical realizability triposes (in the sense of Krivine) and all intuitionistic realizability triposes built from partial combinatory algebras.