Realizing the totally unordered structure of ordinals

TL;DR

The work analyzes how ordinals are represented in realizability models of $ZF_{\varepsilon}$, where two membership relations and two equality notions complicate standard ordinal theory. It develops robust ordinal-name tools, notably $\text{
} r(\alpha)$ and $\hat{\alpha}$, and establishes how successors and $\omega$ are realized, linking them to the classical ordinals $\boldsymbol{\omega}$ and $\text{Ord}$. It then proves cardinal-preservation results mirroring forcing: regular $\delta > |\Lambda|$ remain cardinals in the realizability model, provided NEAC holds, and it develops a chain-condition framework to manage potential collapses. The paper also investigates $ε$-TODs, building classes via lifted Boolean operations, and provides criteria under which the collection of $ε$-TODs forms a set, thereby clarifying the ordinals’ coding and the interaction with class theory in this non-extensional setting. Overall, the results furnish tools to compute $ω$ inside realizability models, control cardinal behavior, and connect forcing intuitions with Krivine-style realizability in $ZF_{\varepsilon}$.

Abstract

We present tools for analysing ordinals in realizability models of classical set theory built using Krivine's technique for realizability. This method uses a conservative extension of $ZF$ known as $ZF_{\varepsilon}$, where two membership relations co-exist, the usual one denoted $\in$ and a stricter one denoted $\varepsilon$ that does not satisfy the axiom of extensionality; accordingly we have two equality relations, the extensional one $\simeq$ and the strict identity $=$ referring to sets that satisfy the same formulas. We define recursive names using an operator that we call reish, and we show that the class of recursive names for ordinals coincides extensionally with the class of ordinals of realizability models. We show that reish$(ω)$ is extensionally equal to omega in any realizability model, thus recursive names provide a useful tool for computing $ω$ in realizability models. We show that on the contrary $\varepsilon$-totally ordered sets do not form a proper class and therefore cannot be used to fully represent the ordinals in realizability models. Finally we present some tools for preserving cardinals in realizability models, including an analogue for realizability algebras of the forcing property known as the $κ$-chain condition.

Theorems & Definitions (133)

• definition 1
• definition 2
• definition 3
• theorem 1: Friedman / Krivine
• definition 4
• definition 5
• definition 6
• proposition 1
• proof
• proposition 2: Peirce's Law