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?


1 Answer 1


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.

However, one could interpret the phrase "the law of excluded middle" also more broadly, including instances which can be formulated in the internal language of toposes but which cannot in the framework of first-order theories. Those instances will in general still be false.

This phenomenon already happens with the easiest theory, the empty one, which doesn't have any sorts or atomic propositions. This theory has precisely one model in any topos, namely the empty family of objects.

Regarding your second question, I don't think so but I'm no expert.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .