Boolean classifying topoi

AbstractLet λ be a finitary geometric theory and δ its classifying topos. We prove that δ is Boolean if and only if (1) every first-order formula in the language of λ is ⧸-provably equivalent to a geometric formula and (2) for any finite list of varibles, x, there are, up to ⧸-provable equivalence, only finitely many formulas, in the language of λ with free variables among x. We use this characterization to show that, when δ 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