论文标题
经典可实现的特征布尔代数的一阶完整性结果
A first-order completeness result about characteristic Boolean algebras in classical realizability
论文作者
论文摘要
我们证明了有关经典可实现性的以下完整性结果：鉴于至少有两个元素的任何布尔代数，存在一个Krivine风格的经典可实现性模型，其特征布尔代数在基本上等同于其。这是通过精确控制所谓的“天使般”（或“ May”）和“ Demonic”（或“必须”）非确定性的哪些组合来完成的。
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.
