Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

In 1978, in a series of unpublished conferences in Montréal, A. Joyal announced a remarkable theorem that unified several completeness theorems for fragments of first order logic, as well as first order logic itself. Given a coherent category $T$, we have the evaluation functor $e_T: T \to \mathcal{S}et^{\mathcal{M}od_c(T)}$, where $\mathcal{M}od_c(T)$ is the category of coherent models of $T$, and the evaluation functor sends an object $A$ to the set-valued functor from $\mathcal{M}od_c(T)$ that simply evaluates a model $M$ in $A$. The theorem is question is the following:

Theorem (Joyal): If $T$ is a Heyting category, then $e_T$ is a conservative Heyting functor.

The power and elegance of Joyal's formulation resides in the fact that it subsumes at least three different completeness theorems: that of coherent logic, that of classical first order logic, and, finally, that of intuitionistic first order logic. Indeed, the first follows from the conservativity of $e_T$, while the second is just the particular case when $T$ is a Boolean category (in which case coherent models are all Boolean). It is the third completeness theorem the most unexpected and amazing, and about which my question refers. The key fact here is that a Kripke model for an intuitionistic first order theory $T$ is the same thing as a Heyting functor $\mathcal{C}_T \to \mathcal{S}et^P$, where $P$ is the underlying poset of the model and $\mathcal{C}_T$ is the (Heyting) syntactic category of the theory. Now, the category $\mathcal{M}od_c(T)$ is not necessarily a poset (though it can be taken to be small), but Joyal's theorem provides us anyway with a generalized Kripke model which only differs in that aspect. In fact, the notion of forcing at a node $M$ coincides precisely with the satisfaction in the model $M$.

Now my question. In a paper by Makkai, the author mentions that "from the formulation of Joyal's theorem, it is quite easy to prove the existence of a conservative Heyting embedding of the form $e_T: T \to \mathcal{S}et^P$ with a poset $P$, with possible further conditions on $P$ (for example, regarding its size, or that it be a forest -a tree with many roots)". How exactly can this be achieved? The size is not an issue, since due to Löwenheim-Skolem theorem one can always cut down the category of models to restrict the cardinality. From the proof of Joyal's theorem, which can be found in Makkai-Reyes "First order categorical logic", I can also see that it is enough to consider only elementary embeddings as the morphisms in the category of models. Yet, this still doesn't necessarily make it into a poset. I also have an idea of which models can be taken as the roots of the forest, and how to derive a tree from a general poset with a bottom node, but cannot see how to bring the category of models into a posetal one. So, which is the argument Makkai is referring to?


EDIT

Andreas has given the right answer to the question. The non trivial thing in his construction of the poset $P$ is to prove that the functor $E^*: \mathcal{S}et^M \to \mathcal{S}et^P$ preserves $\forall$. Here is the calculation:

For a natural transformation $f: F \to G$ in $\mathcal{S}et^M$ and a subfunctor $A$ of $F$, we need to show that $E^*(\forall_fA)$ is the same subfunctor of $E^*(G)$ as $\forall_{E^*(f)}E^*(A)$. By definition, for any object $p$ in $P$ and $y \in E^*(G)(p)=G(E(p))$, we have $y \in \forall_{E^*(f)}E^*(A)(p)$ if and only if for all arrows $l: p \to q$ in $P$ one has:

$$E^*(f)_q^{-1}(G(E(l))(y)) \subseteq E^*(A)(q)$$

$$\iff (\forall x E^*(f)_q(x)=G(E(l))(y) \implies x \in E^*(A)(q))$$

$$\iff (\forall x f_{E(q)}(x)=G(E(l))(y) \implies x \in A(E(q))) (1)$$

On the other hand, also by definition, for $y \in G(E(p))$ one has $y \in \forall_fA(E(p))$ if and only if for all arrows $t: E(p) \to r$ in $M$ one has:

$$f_r^{-1}(G(t)(y)) \subseteq A(r)$$

$$\iff (\forall x f_r(x)=G(t)(y) \implies x \in A(r)) (2)$$

But because the functor $E$ is surjective (both on objects and arrows), we can find $q, l \in P$ such that $r=E(q)$ and $t=E(l)$, from which we deduce that $(1)$ and $(2)$ above are equivalent. Hence, $E^* \forall=\forall E^*$, as we wanted.

share|improve this question
add comment

1 Answer 1

up vote 7 down vote accepted

The following is based on vague memories from long ago, so it comes with no guarantees. If it turns out to be totally wrong, then someone will surely say so and I'll delete it.

I think the poset $P$ that you want, to replace the category $M=\mathcal Mod_c(T)$, consists of finite composable sequences of morphisms of $M$, i.e., chains $A_0\to A_1\to\cdots\to A_n$ in $M$. One such sequence is below another in $P$ if the former is an initial segment of the latter. There's a functor from $E:P\to M$ sending each chain to the last object in it and sending any morphism $f$ of $P$ to the composite of the morphisms of $M$ that are in the codomain minus the domain of $f$. Then, given Joyal's version of $e_T$, compose it with $\mathcal Set^E$, and (if my memory is right) you get Makkai's $e_T$.

The actual definition of this construction can be found in Mac Lane and Moerdijk's Sheaves in Geometry and Logic, Th. 9.1. This is used to prove the existence of the Diaconescu cover.

share|improve this answer
    
Andreas, this seems to be exactly right. One only has to prove that E*: Set^M-->Set^P is a Heyting functor. That it preserves limits, unions and covers follows from the fact that these three things are computed pointwise in a presheaves category, so the functor is certainly coherent and one only needs to spell out what preserving the forall quantifier means. I'll try to write this down in detail –  godelian Jul 3 '13 at 0:00
    
Done. I forgot to mention conservativity, but it follows easily from the fact that E is surjective on objects and arrows. –  godelian Jul 3 '13 at 1:28
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.