Some notes on plump ordinals
Shuwei Wang
TL;DR
This work develops a self-contained, intuitionistic framework for plump ordinals by formulating a $\Pi_1$-definable notion of plumpness within $\mathrm{IKP}$ and constructing the plump constructible universe $L_{\mathrm{pl}}$. It establishes arithmetic and coding tools for plump ordinals, including a robust theory of plump ordinal addition, multiplication, and incomparability-based encodings, and shows that $L_{\mathrm{pl}}$ can satisfy $\mathrm{IKP}$ with bounding principles under suitable hypotheses. The paper then applies Heyting forcing on generalized Cantor space to force $\mathcal{P}(\check{x})$ into $L_{\mathrm{pl}}$ (hence into $L$) for any fixed $x$, illustrating how plump ordinal methods enable embedding of large sets into constructible-like inner models in an intuitionistic setting. Overall, it links ordinal combinatorics, inner-model theory, and forcing semantics to provide a route for constructive coding of subsets into $L$ via Heyting-valued models.
Abstract
In this exposition, we attempt to formalise a treatment of Paul Taylor's notion of plump ordinals in weak intuitionistic axiomatic set theories such as IKP. We will explore basic properties of plump ordinals, especially in relation to Gödel's constructible universe $L$ and incomparable codings. As a quick application, we explain at the end how plump ordinals can be used to build a Heyting-valued model $V^\mathbb{H}$ from a classical $V \vDash \mathrm{ZFC}$ such that for some arbitrary, fixed $x \in V$ we have $V^\mathbb{H} \vDash \mathcal{P}{\left(\check{x}\right)} \in L$.