An equiconsistency proof for $\mathrm{CZF} + V = L$
Logic
2026-02-17 v1
Abstract
In many axiomatic set theories, G\"odel's constructible universe 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 does not increase the consistency strength of the theory. In this paper, we shall look at a system of intuitionistic set theory known as , where fails to exhibit such nice properties. We will demonstrate that, here, the theory is still equiconsistent with , but the proof will involve a much more complicated realisability model and a recursion-theoretic argument.
Cite
@article{arxiv.2602.13917,
title = {An equiconsistency proof for $\mathrm{CZF} + V = L$},
author = {Shuwei Wang},
journal= {arXiv preprint arXiv:2602.13917},
year = {2026}
}