Are there enough injective sets?

Abstract: The axiom of choice ensures precisely that, in ZFC, every set is projective: that is, a projective object in the category of sets. In constructive ZF (CZF) the existence of enough projective sets has been discussed as an additional axiom taken from the interpretation of CZF in Martin-Loef's intuitionistic type theory. On the other hand, every non-empty set is injective in classical ZF, which argument fails to work in CZF. The aim of this paper is to shed some light on the problem whether there are (enough) injective sets in CZF. We show that no two element set is injective unless the law of excluded middle is admitted for negated formulas, and that the axiom of power set is required for proving that there are strongly enough injective sets. The latter notion is abstracted from the singleton embedding into the power set, which ensures enough injectives both in every topos and in IZF. We further show that it is consistent with CZF to assume that the only injective sets are the singletons. In particular, assuming the consistency of CZF one cannot prove in CZF that there are enough injective sets. As a complement we revisit the duality between injective and projective sets from the point of view of intuitionistic type theory.

Review text

The article analyses the notion of injective set in constructive Zermelo-Fraenkel set theory (CZF), that is a variant of ZF based on intuitionistic logic, with crucial restrictions to the schema of separation and the axiom of powerset. In the category of sets, the notion of injective set is defined as follows: a set E is injective if every map with codomain E can be extended to any superset of its domain. Given this notion of injective set, the authors then consider the statement: (*) ``there are enough injective sets, which holds if every set is the domain of an injective map whose codomain is an injective set. The statement thus is a dual of the presentation axiom, that states that there are enough projective sets. The latter is a choice principle validated under Aczel's interpretation of CZF in Martin-Löf type theory. In ZF, every set is injective if and only if it is non-empty. Therefore, trivially, there are enough injective sets. However, the authors observe that, if we move to the more general context of CZF, we can not prove the existence of enough injective sets. The aim of the article is to analyse the notion of injective set and the statement (*) on the basis of CZF. For example, it is shown that the statement ``every inhabited set is injective is equivalent to the law of restricted excluded middle, that is, to the excluded middle for \(\Delta_0\) formulas. (Note that in constructive settings a set is inhabited if it has an element.) Another statement that is proved is that it is consistent with CZF that the only injective sets are the singletons. One might wonder whether the fact that we cannot prove that there are enough injective sets in CZF is due only to the shift to intuitionistic rather than classical logic. However, as the authors recall, it is well known that in IZF, which is an intuitionistic variant of ZF with full separation and powerset, one can still prove that there are enough injective sets. In fact, the powerset axiom seems to play a crucial role here, and so the authors study its relation with a strengthening of (*).

Recommendations

Cites work

Cited in

(5)

This page was built for publication: Are there enough injective sets?

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2377052)