Some notes on plump ordinals

TL;DR

This paper formalizes the concept of plump ordinals within weak intuitionistic set theories, explores their properties in relation to G"odel's constructible universe, and demonstrates their application in constructing Heyting-valued models.

Contribution

It provides a formal framework for plump ordinals in weak set theories and shows how they can be used to build Heyting-valued models with specific properties.

Findings

Plump ordinals can be formalized in weak intuitionistic theories.

Properties of plump ordinals relate to G"odel's constructible universe.

Construction of Heyting-valued models using plump ordinals is possible.

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\"odel'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$.