P2 A first-order completeness result about characteristic Boolean algebras in classical realizability
经典可实现性中特征布尔代数的一阶完备性结果
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 1/10 · 该论文是纯逻辑与形式语义研究，讨论经典可实现性模型中的特征布尔代数完备性，不涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析，与用户研究画像几乎无直接交集。引用 0inbox
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.
@inproceedings{abs-2209-08838,
title = {A first-order completeness result about characteristic Boolean algebras in classical realizability},
author = {Guillaume Geoffroy},
booktitle = {LICS},
year = {2022},
doi = {10.1145/3531130.3532484}
}