Rencontre,
22 septembre 2022
Guillaume Geoffroy (IRIF), A first-order completeness result about characteristic Boolean algebras in classical realizability
Programme
- 22 septembre 2022, 14:00 - 15:00
Résumé
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.