3 papers
cs.LO2026
Blurred Drinker Paradoxes and Blurred Choice Axioms: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem
Dominik Kirst, Haoyi Zeng
In the setting of constructive reverse mathematics, we analyse the downward Löwenheim-Skolem (DLS) theorem of first-order logic, stating that every infinite model has a countable e…
cs.LO2025
Syntactic Effectful Realizability in Higher-Order Logic
Liron Cohen, Ariel Grunfeld, Dominik Kirst +1
Realizability interprets propositions as specifications for computational entities in programming languages. Specifically, syntactic realizability is a powerful machinery that hand…
cs.LO2025
From Partial to Monadic: Combinatory Algebra with Effects
Liron Cohen, Ariel Grunfeld, Dominik Kirst +1
Partial Combinatory Algebras (PCAs) provide a foundational model of the untyped -calculus and serve as the basis for many notions of computability, such as realizability theory.…