The Axiom of Multiple Choice and Models for Constructive Set Theory

TL;DR

This paper extends constructive set theory with an axiom for inductive types and choice, demonstrating interpretability in type theory, proof of key theorems, stability under constructions, and applicability of derived rules.

Contribution

It introduces a new extension of CZF that incorporates inductive types and choice, with proven interpretability, robustness, and applicability of derived rules.

Findings

Interpretability in Martin-Löf's type theory

Proof of the Set Compactness Theorem

Stability under algebraic set theory constructions

Abstract

We propose an extension of Aczel's constructive set theory CZF by an axiom for inductive types and a choice principle, and show that this extension has the following properties: it is interpretable in Martin-Lof's type theory (hence acceptable from a constructive and generalised-predicative standpoint). In addition, it is strong enough to prove the Set Compactness Theorem and the results in formal topology which make use of this theorem. Moreover, it is stable under the standard constructions from algebraic set theory, namely exact completion, realizability models, forcing as well as more general sheaf extensions. As a result, methods from our earlier work can be applied to show that this extension satisfies various derived rules, such as a derived compactness rule for Cantor space and a derived continuity rule for Baire space. Finally, we show that this extension is robust in the sense that it is also reflected by the model constructions from algebraic set theory just mentioned.