Reals and forcing with an elementary topos. (English) Zbl 0756.03025

Logic from computer science, Proc. Workshop, Berkeley/CA (USA) 1989, Publ., Math. Sci. Res. Inst. 21, 373-385 (1992).
[For the entire collection see Zbl 0741.00073.]
This expository paper indicates how generalized sheaf theoretic methods in the context of topos theory can be used in formulating independence proofs by forcing. This article is very clearly written and covers a surprising amount of material. Yet this material is presented in a highly readable fashion and should be accessible to any mathematically sophisticated reader with a background in logic.
Beginning with Lawvere’s insights into describing sets with function composition as the primitive notion rather than set membership, the article proceeds through a description of the definition of an elementary topos, a discussion of presheaves and sheafification, and then looks at Cohen’s proof of the independence of the Continuum Hypothesis from a categorical perspective. This is followed by discussion of Kripke-Joyal semantics for the intuitionistic logic of toposes, Freyd’s proof of the independence of the Axiom of Choice, and the equiconsistency of the notion of well-pointed topos with the set-theoretic system BZC of bounded Zermelo set theory with choice.
The reviewer believes that well-written and informative articles such as this one are a welcome addition to the mathematical literature; there should be more of them.


03E35 Consistency and independence results
03G30 Categorical logic, topoi
18B25 Topoi


Zbl 0741.00073