Does Choice Really Imply Excluded Middle? Part I: Regimentation of the Goodman–Myhill Result, and Its Immediate Reception†

ABSTRACT The one-page 1978 informal proof of Goodman and Myhill is regimented in a weak constructive set theory in free logic. The decidability of identities in general ($a\!=\!b\vee\neg a\!=\!b$) is derived; then, of sentences in general ($\psi\vee\neg\psi$). Martin-Löf’s and Bell’s receptions of the latter result are discussed. Regimentation reveals the form of Choice used in deriving Excluded Middle. It also reveals an abstraction principle that the proof employs. It will be argued that the Goodman–Myhill result does not provide the constructive set theorist with a dispositive reason for not adopting (full) Choice.

Does Choice Really Imply Excluded Middle? Part II: Historical, Philosophical, and Foundational Reflections on the Goodman–Myhill Result†

ABSTRACT Our regimentation of Goodman and Myhill’s proof of Excluded Middle revealed among its premises a form of Choice and an instance of Separation. Here we revisit Zermelo’s requirement that the separating property be definite. The instance that Goodman and Myhill used is not constructively warranted. It is that principle, and not Choice alone, that precipitates Excluded Middle. Separation in various axiomatizations of constructive set theory is examined. We conclude that insufficient critical attention has been paid to how those forms of Separation fail, in light of the Goodman–Myhill result, to capture a genuinely constructive notion of set.

Homotopy type-theoretic interpretations of constructive set theories

We introduce a family of (k, h)-interpretations for 2 ≤ k ≤ ∞ and 1 ≤ h ≤ ∞ of constructive set theory into type theory, in which sets and formulas are interpreted as types of homotopy level k and h, respectively. Depending on the values of the parameters k and h, we are able to interpret different theories, like Aczel’s CZF and Myhill’s CST. We also define a proposition-as-hproposition interpretation in the context of logic-enriched type theories. The rest of the paper is devoted to characterising and analysing the interpretations considered. The formulas valid in the prop-as-hprop interpretation are characterised in terms of the axiom of unique choice. We also analyse the interpretations of CST into homotopy type theory, providing a comparative analysis with Aczel’s interpretation. This is done by formulating in a logic-enriched type theory the key principles used in the proofs of the two interpretations. Finally, we characterise a class of sentences valid in the (k, ∞)-interpretations in terms of the ΠΣ axiom of choice.

Multisets in type theory

A multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a given multiset. In this work we will investigate the notion of iterative multisets, where multisets are iteratively built up from other multisets, in the context Martin–Löf Type Theory, in the presence of Voevodsky’s Univalence Axiom.In his 1978 paper, “the type theoretic interpretation of constructive set theory” Aczel introduced a model of constructive set theory in type theory, using a W-type quantifying over a universe, and an inductively defined equivalence relation on it. Our investigation takes this W-type and instead considers the identity type on it, which can be computed from the univalence axiom. Our thesis is that this gives a model of multisets. In order to demonstrate this, we adapt axioms of constructive set theory to multisets, and show that they hold for our model.

FROM MULTISETS TO SETS IN HOMOTOPY TYPE THEORY

We give a model of set theory based on multisets in homotopy type theory. The equality of the model is the identity type. The underlying type of iterative sets can be formulated in Martin-Löf type theory, without Higher Inductive Types (HITs), and is a sub-type of the underlying type of Aczel’s 1978 model of set theory in type theory. The Voevodsky Univalence Axiom and mere set quotients (a mild kind of HITs) are used to prove the axioms of constructive set theory for the model. We give an equivalence to the model provided in Chapter 10 of “Homotopy Type Theory” by the Univalent Foundations Program.

The axiom of multiple choice and models for constructive set theory

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-Löf's type theory (hence acceptable from a constructive and generalized-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.