Let $T$ be a theory in classical (finitary) first-order logic over some language $L$. Then $T$ is equivalent over classical logic to its Morleyization $T^m$, i.e. the theory in the language $L^m$ which has a relation symbol for each formula of $L$ and the obvious axioms. That is, the natural interpretation of $L$ in $L^m$ induces a bijection of $Set$-models, which is even an equivalence of categories if we use elementary embeddings for morphisms.
This leads to the following conundrum:
By D1.5.13 in the Elephant, the theory $T^m$ admits an axiomatization in coherent logic.
The category $\operatorname{Def}_{T^m}$ of $T^m$-definable sets is clearly Boolean (i.e. subobjects have complements), so the classifying topos $\mathcal E_{T^m}$ is also Boolean.
But Blass and Scedrov showed in Boolean Classifying Topoi that the classifying topos $\mathcal E_{S}$ of a coherent theory $S$ is Boolean only under much more restrictive conditions (stronger than being $\aleph_0$-categorical!).
But
- There exist classical first-order theories which are not $\aleph_0$-categorical.
This is a contradiction. So I'm not understanding something.
Question 1: Where am I going wrong here?
Question 2: I suppose the most likely answer is that just because a coherent category is Boolean, perhaps that doesn't imply that its classifying topos is Boolean? If that's the case, what would be a simple counterexample where one can see this in action?
Question 3: If classifying topoi of classical theories which eliminate quantifiers are not necessarily (or even typically!) Boolean, then is there some other way to characterize them among topoi? Or at least some interesting necessary condition they satisfy, such as being DeMorgan?