Abstract:This work presents a transfinite version of the bar-recursion in the context of classical realizability models for set theory. Bar-recursion has been previously used to obtain realizability interpretations of countable choice and dependent choice, and was employed by Krivine to realize the continuum hypothesis in classical realizability. In this paper, we introduce a transfinite variant of bar-recursion and use it to construct realizability models validating uncountable fragments of the Axiom of Choice. Moreover, our construction reveals that this generalized bar-recursion is related to preservation of cardinals. To show this, we define an analogue of the forcing notion of $\kappa$-closure for classical realizability algebras that we call $\kappa$-fully-closed. We show that, in realizability algebras satisfying the $\kappa$-full-closure property, generalized bar-recursion realizes that any cardinal up to $\kappa$ admits a representative in the realizability model which remains a cardinal.
From: Jacopo Furlan [view email]
[v1]
Wed, 24 Jun 2026 08:59:55 UTC (48 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。