Boolean classifying topoi

Let [lambda] be a finitary geometric theory and [delta] its classifying topos. We prove that [delta] is Boolean if and only if (1) every first-order formula in the language of [lambda] is [+45 degree rule]-provably equivalent to a geometric formula and (2) for any finite list of varibles, x, there are, up to [+45 degree rule]-provable equivalence, only finitely many formulas, in the language of [lambda] with free variables among x. We use this characterization to show that, when [delta] is Boolean, it is an atomic topos and can be viewed as a finite coproduct of topoi of continuous G-sets for topological groups G satisfying a certain finiteness condition.Peer Reviewedhttp://deepblue.lib.umich.edu/bitstream/2027.42/25248/1/0000690.pd