A first-order completeness result about characteristic Boolean algebras in classical realizability

TL;DR

This paper establishes a completeness result in classical realizability, showing that any Boolean algebra with at least two elements can be represented by a Krivine-style model with an elementarily equivalent characteristic Boolean algebra.

Contribution

It introduces a method to construct realizability models with characteristic Boolean algebras elementarily equivalent to any given Boolean algebra, controlling nondeterminism in the model.

Findings

Any Boolean algebra with at least two elements can be realized in a Krivine-style model.

The construction precisely controls angelic and demonic nondeterminism.

Models can be tailored to match the elementary theory of any given Boolean algebra.

Abstract

We prove the following completeness result about classical realizability: given any Boolean algebra with at least two elements, there exists a Krivine-style classical realizability model whose characteristic Boolean algebra is elementarily equivalent to it. This is done by controlling precisely which combinations of so-called "angelic" (or "may") and "demonic" (or "must") nondeterminism exist in the underlying model of computation.