# Is the interpretation of the Morleyization of a first order theory in a Heyting category automatically classical?

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_\varphi\vdash C_\psi$ for each axiom $\varphi\vdash\psi$ 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 $\varphi\in T$ the axioms $$\vdash C_\varphi\vee D_\varphi$$ and $$C_\varphi\wedge D_\varphi\vdash \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_\varphi\vee D_\varphi,\neg C_\varphi\vdash D_\varphi$ just from intuitionistic logic, and from this and the first of the above two axioms we can derive $\neg C_\varphi\vdash D_\varphi$; and from the second of those two axioms alone we can derive $D_\varphi\vdash\neg C_\varphi$. Hence $\vdash C_\varphi\vee\neg C_\varphi$ will hold because $\vdash C_\varphi\vee 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?

I believe your deduction of $$\vdash C_\varphi \vee \neg C_\varphi$$ is entirely correct, and in this specific sense, any model of the Morleyization (in any topos) satisfies the law of excluded middle.