En 1978, en una serie de conferencias inéditas en la ciudad de Montreal, A. Joyal anunció una notable teorema que unificó varios teoremas de completitud de los fragmentos de primer orden de la lógica, así como de primer orden de la lógica misma. Dada una categoría coherente $T$, tenemos la evaluación functor $e_T: T \to \mathcal{S}et^{\mathcal{M}od_c(T)}$ donde $\mathcal{M}od_c(T)$ es la categoría de modelos coherentes de $T$, y la evaluación functor envía un objeto $A$ para el conjunto de valores de functor de $\mathcal{M}od_c(T)$ que evalúa un modelo de $M$ en $A$. El teorema en cuestión es el siguiente:
Teorema (Joya): Si $T$ es un Heyting categoría, a continuación, $e_T$ es un conservador de Heyting functor.
El poder y la elegancia de la Joya de la formulación reside en el hecho de que subsume al menos tres diferentes teoremas de completitud: el de la lógica coherente, que de la clásica de primer orden de la lógica, y, por último, que de intuitionistic de primer orden de la lógica. De hecho, la primera de la siguiente manera a partir de la conservativity de $e_T$, mientras que el segundo es sólo el caso en particular, cuando $T$ es un valor Booleano de la categoría (en el que caso de modelos coherentes son todos Booleano). Es la tercera integridad teorema de la forma más inesperada y sorprendente, y sobre el cual mi pregunta se refiere. El hecho clave aquí es que un modelo de Kripke para un intuitionistic de primer orden de la teoría de la $T$ es la misma cosa como una Heyting functor $\mathcal{C}_T \to \mathcal{S}et^P$ donde $P$ es el subyacente poset de la modelo y $\mathcal{C}_T$ es el (Heyting) categoría sintáctica de la teoría. Ahora, la categoría de $\mathcal{M}od_c(T)$ no es necesariamente un poset (aunque puede ser llevado a ser pequeños), pero Joyal del teorema nos provee de todos modos con una generalizada de Kripke modelo que sólo se diferencia en ese aspecto. De hecho, la idea de forzar a un nodo $M$ coincide precisamente con la satisfacción en el modelo de $M$.
Ahora mi pregunta. En un papel por Makkai, el autor menciona que "a partir de la formulación de Joyal del teorema, es muy fácil demostrar la existencia de un conservador de Heyting la incrustación de la forma $e_T: T \to \mathcal{S}et^P$ con un poset $P$, con las posibles condiciones en $P$ (por ejemplo, en cuanto a su tamaño, o que sea un bosque un árbol con muchas raíces)". Exactamente cómo se consigue esto? El tamaño no es un problema, ya que, debido a Löwenheim-Skolem teorema uno siempre se puede reducir a la categoría de modelos para restringir la cardinalidad. A partir de la prueba de Joyal del teorema, el cual puede ser encontrado en Makkai-Reyes "de Primer orden categórica de la lógica", también puedo ver que es suficiente considerar sólo la primaria incrustaciones como los morfismos en la categoría de modelos. Sin embargo, esto no necesariamente lo hacen en un poset. También tengo una idea de que los modelos pueden ser tomadas como las raíces de los bosques, y cómo derivar a un árbol de un general poset con un nodo inferior, pero no se puede ver cómo llevar a la categoría de modelos en un posetal uno. Así que, cual es el argumento Makkai se está refiriendo?
EDITAR
Andreas ha dado la respuesta correcta a la pregunta. El no trivial en su construcción de la poset $P$ es demostrar que el functor $E^*: \mathcal{S}et^M \to \mathcal{S}et^P$ preserva $\forall$. Aquí está el cálculo:
Para una transformación natural $f: F \to G$ en $\mathcal{S}et^M$ y un subfunctor $A$ de % de$F$, tenemos que mostrar que $E^*(\forall_fA)$ es el mismo subfunctor de $E^*(G)$ as $\forall_{E^*(f)}E^*(A)$. Por definición, para cualquier objeto $p$ en $P$ e $y \in E^*(G)(p)=G(E(p))$, tenemos $y \in \forall_{E^*(f)}E^*(A)(p)$ si y sólo si para todas las flechas $l: p \to q$ en $P$ una cuenta:
$$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)$$
Por otro lado, también por definición, para $y \in G(E(p))$ uno ha $y \in \forall_fA(E(p))$ si y sólo si para todas las flechas $t: E(p) \to r$ en $M$ una cuenta:
$$f_r^{-1}(G(t)(y)) \subseteq A(r)$$
$$\iff (\forall x f_r(x)=G(t)(y) \implies x \in A(r)) (2)$$
Pero debido a que el functor $E$ es surjective (tanto en los objetos y las flechas), podemos encontrar $q, l \in P$ tal que $r=E(q)$ e $t=E(l)$, de la que podemos deducir que el $(1)$ e $(2)$ anteriores son equivalentes. Por lo tanto, $E^* \forall=\forall E^*$, como queríamos.
