Bar-recursion and Preservation of Cardinals

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 $κ$-closure for classical realizability algebras that we call $κ$-fully-closed. We show that, in realizability algebras satisfying the $κ$-full-closure property, generalized bar-recursion realizes that any cardinal up to $κ$ admits a representative in the realizability model which remains a cardinal.