Vtyjkyuk

In Johnstone's Sketches of an Elephant (D1.5.13), he describes how given a first order theory $T$ in a signature $Sigma$, one can devise a coherent theory $T'$ over a new signature $Sigma'$ (the Morleyization of $T$) such that in Boolean Coherent categories the two theories have essentially the same models.

Initially, when I heard this result, I had believed that both the coherent and first order theory would have non-classical models in Heyting categories that might differ in that setting, but coincide in a classical setting; but it's seeming as though I was incorrect, and that the Morleyization will have classical models in any Heyting category. Constructive reasoning is something I'm just getting the hang of, so I wanted to get confirmation or correction as appropriate.

My thinking goes like this: Given the theory $T$ in the signature $Sigma$, the Morleyization adds to $Sigma$ two atomic predicate symbols $C_varphi, D_varphi$ for every $Sigma$-formula $varphi$ (with the same free variables as $varphi$); this gives us $Sigma'$. $T'$ is obtained by taking as an axiom the sequent $C_varphivdash C_psi$ for each axiom $varphivdashpsi$ in $T$, plus a collection of axioms that make sure that the interpretations of these new atomic predicates are based on the structure of the formula in their subscript. In particular, $T'$ contains for each $varphiin T$ the axioms $$vdash C_varphivee D_varphi$$ and $$C_varphiwedge D_varphivdash bot$$ ensuring that the subobjects interpreting these predicates are complementary.

Now let's say we take the theory $T'$, but interpret it in a logic that has the connective "$Rightarrow$" available. Then it looks like we can prove $C_varphivee D_varphi,neg C_varphivdash D_varphi$ just from intuitionistic logic, and from this and the first of the above two axioms we can derive $neg C_varphivdash D_varphi$; and from the second of those two axioms alone we can derive $D_varphivdashneg C_varphi$. Hence $vdash C_varphiveeneg C_varphi$ will hold because $vdash C_varphivee D_varphi$ does.

Have I made a mistake on this, or am I correct that excluded middle will hold in the Morleyization if implication is allowed? If I'm not in error, is there an easy tweak that makes $D_varphi$ behave more like a general Heyting negation of $C_varphi$ instead of a strict classical negation?