Are there enough injective sets? (Q2377052): Difference between revisions

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 (*).