An equiconsistency proof for $\mathrm{CZF} + V = L$

TL;DR

The paper proves that for $CZF$, adding the axiom $V = L$ does not increase the theory's consistency strength by constructing a realizability model inside $BI$ that satisfies $V = L$. It develops a sophisticated coding framework based on a distinguished ordinal $\alpha_0$ and a sequence $f_0: \omega \to \mathcal{P}(\omega)$ of strongly incomparable images in $L$, enabling the encoding of subcountable sets into constructible stages. The core result is that $\mathcal{P}(\omega) \subseteq L$ in the model, hence $V = L$, and since $BI$ is equiconsistent with $CZF$, one obtains $CZF \equiv_{Con} CZF + V = L$. This extends earlier intuitionistic results to the constructive setting, providing a concrete realizability and coding mechanism to establish the equiconsistency claim. The work clarifies how the constructible universe interacts with constructive set theories and offers a method that could inform similar equiconsistency analyses for related theories.

Abstract

In many axiomatic set theories, Gödel's constructible universe $L$ is known as an inner model, that is, a definable class satisfying the same axioms (and containing the same ordinals). This gives a trivial proof that adding the axiom $V = L$ does not increase the consistency strength of the theory. In this paper, we shall look at a system of intuitionistic set theory known as $\mathrm{CZF}$, where $L$ fails to exhibit such nice properties. We will demonstrate that, here, the theory $\mathrm{CZF} + V = L$ is still equiconsistent with $\mathrm{CZF}$, but the proof will involve a much more complicated realisability model and a recursion-theoretic argument.

Theorems & Definitions (21)

• Theorem 1: $\mathrm{IKP}$, lubarsky93-intuitionistic-l
• Theorem 2: rathjen20-power-kp-choice
• Theorem 3: matthews-rathjen24-constructible-universe
• Lemma 1: $\mathrm{PA}$
• proof
• Proposition 1: Subcountability
• proof
• Proposition 2
• Lemma 2
• proof