Are there enough injective sets?

DOI10.1007/S11225-011-9365-8zbMATH Open1319.03053arXiv1111.5180OpenAlexW2170071327WikidataQ114223406 ScholiaQ114223406MaRDI QIDQ2377052FDOQ2377052

Authors: Peter Aczel, Benno van den Berg, Peter Schuster, Johan Georg Granström 

Publication date: 27 June 2013

Published in: Studia Logica (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1111.5180

Recommendations

• Injective power objects and the axiom of choice
• Independence results around constructive ZF
• The axiom of multiple choice and models for constructive set theory
• Injective types in univalent mathematics
• scientific article; zbMATH DE number 5064954

zbMATH Keywords

injective objectintuitionistic type theoryaxiom of powersetconstructive Zermelo-Fraenkel set theoryrestricted excluded middle

Mathematics Subject Classification ID

Nonclassical and second-order set theories (03E70) Other constructive mathematics (03F65)

Cites Work

• Sheaves in geometry and logic: a first introduction to topos theory
• Title not available (Why is that?)
• A course in constructive algebra
• Title not available (Why is that?)
• Title not available (Why is that?)
• Injectivity, Projectivity, and the Axiom of Choice
• Title not available (Why is that?)
• Title not available (Why is that?)
• Aspects of predicative algebraic set theory. II: Realizability
• What does it take to prove Fermat's last theorem? Grothendieck and the logic of number theory
• The shrinking principle and the axiom of choice
• On constructing completions
• Binary refinement implies discrete exponentiation
• 100 Years of Zermelo’s Axiom of Choice: What was the Problem with It?

Cited In (5)

• Towards formal Baer criteria
• Injective power objects and the axiom of choice
• Towards constructivising the Freyd-Mitchell embedding theorem
• The weak choice principle WISC may fail in the category of sets
• A characterization of those categories whose internal logic is Hilbert's \(\varepsilon\)-calculus

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)