A Boolean topos is a topos that is also a Boolean category. There are several conditions on a topos that are necessary and sufficient to be Boolean: Let be a Boolean pretopos, i.e. a pretopos in which is also a Boolean category, and let be the classifying topos for . Then it does not follow that is Boolean. In fact, this is rarely the case, even if is the classifying pretopos for a theory in classical first-order logic. See Blass and Scedrov for a characterization of which classical first-order theories have Boolean classifying topoi – in particular, any such theory is -categorical. Nevertheless, as discussed below, Barr's theorem shows that any topos admits a surjection from a Boolean topos. The internal logic of a Boolean topos with natural numbers object can serve as foundations for “ordinary” mathematics, except for that which relies on the axiom of choice. If you add the axiom of choice, then you get (an internal version of) ETCS; conversely, if you use an arbitrary topos, then you get constructive mathematics. (For some high-powered work, you may also need to add a version of the axiom of replacement or an axiom of Grothendieck universes.) Every cartesian closed Boolean pretopos is in fact a topos. This is why ‘generalised predicativism’ (with function types but not power types) is necessarily a feature of constructive mathematics only. For a topos, then the following are equivalent: is a Boolean topos; Every subtopos of is Boolean. Every subtopos of is an open subtopos. Every subtopos of is a closed subtopos. Let be a Lawvere-Tierney topology on . Then is Boolean iff there exists a subterminal object such that is the largest topology such that is -closed, or equivalently, that is a -sheaf. Topologies satisfying the latter condition are called quasi-closed and sometimes denoted . They can also be described by the Heyting algebra operations on as the composite The corresponding quasi-closed subtoposes are the double negation subtoposes of the closed subtoposes...