  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.
