The Axiom of Multiple Choice and Models for Constructive Set Theory

Por • 4 may, 2012 • Sección: Opinion

Benno van den Berg, Ieke Moerdijk

Abstract: We propose an extension of Aczel’s constructive set theory CZF which is acceptable from a generalised-predicative point of view, because interpretable in Martin-Lof’s type theory; strong enough to prove the Set Compactness Theorem and capture a substantial part of formal topology; and preserved by the model constructions of exact completion, realizability and sheaves. More concretely, our proposal is to extend CZF with an axiom postulating the existence of W-types and a choice principle we call the Axiom of Multiple Choice (and which is a slightly simpler and weaker version of the axiom as originally introduced by Palmgren and the second author). We will also show that this extension has a certain robustness about it in that these additional axioms are also reflected by the model constructions we mentioned.

arXiv:1204.4045v1 [math.LO]

Post to Twitter

Etiquetado con: , , ,

Escribe un comentario