Constructing the Constructible Universe Constructively
Logic
2023-09-27 v3
Abstract
We study the properties of the constructible universe, L, over intuitionistic theories. We give an extended set of fundamental operations which is sufficient to generate the universe over Intuitionistic Kripke-Platek set theory without Infinity. Following this, we investigate when L can fail to be an inner model in the traditional sense. Namely, we show that over Constructive Zermelo-Fraenkel (even with the Power Set axiom) one cannot prove that the Axiom of Exponentiation holds in L.
Keywords
Cite
@article{arxiv.2206.08283,
title = {Constructing the Constructible Universe Constructively},
author = {Richard Matthews and Michael Rathjen},
journal= {arXiv preprint arXiv:2206.08283},
year = {2023}
}
Comments
27 pages. Revised following referee's recommendations