# Completeness theorem via syntactic categories

The nLab says in its internal logic article that the Completeness Theorem can be proven via a generic model'' of the theory. The model is generic in the sense that the only things true of it are those provable from the axioms. Since a model of $T$ is a functor $\text{Syn}(T)\rightarrow \text{Set}$, and they say the generic model is obtained via the Yoneda lemma, presumably it corresponds to some representable $\text{Syn}(T)(-, \Gamma)$, but I can't see what $\Gamma$ should be. This is probably obvious once explained, but I understand the syntactic category construction poorly enough that I can't work it out myself.

Some context: this is what some of my other thoughts about this subject sound like. "Clearly, these generic models can only exist in some sort of constructive' environment. In the theory of groups, we can state $x: G, x^2 = e \vdash x = e$, with $e$ denoting the identity. We can also state $\vdash (\exists (x : G)(x^2 = e \wedge x \neq e)$, if we allow ourself $\exists$ and negation. Both of these have a model where they are false, so neither can hold of the generic model, which seems to be at least a weak failure of the Law of Excluded Middle."

Am I way off of the right idea? Thank you for clarifying.

• The nLab seems to be unavailable at the moment so I can't read the article you link to, but I would guess that by model they mean a functor $\textrm{Syn}(T) \to C$ where $C$ is not necessarily sets but rather any category with the appropriate structure. In that case the identity functor $\textrm{Syn}(T) \to\textrm{Syn}(T)$ is the generic model. – Omar Antolín-Camarena Oct 10 '13 at 4:08
• @OmarAntolín-Camarena that's actually the answer to the question: quoting directly from the nlab " By the Yoneda lemma, the syntactic category $Syn(T)=C_T$ contains a “generic” model of the theory. Moreover, by the construction of $C_T$ (see syntactic category), the valid sequents in this model are precisely those provable from the theory." – Giorgio Mossa Oct 10 '13 at 15:00

If I'm correct, the idea is that a sequent $A \vdash B$ over variables $\vec{x}$ is provable iff the formula $\theta := (\vec{x} = \vec{y}) \wedge A$ is a morphism $\{ \vec{x}.A \} \to \{ \vec{y}.B[\vec{y}/\vec{x}] \}$ in $\mathit{Syn}(T)$. Now, $A \vdash B$ holds in the model obtained from the representable over $\{ \vec{x}.A \}$ iff $\theta$ is a morphism in $\mathit{Syn}(C)$, hence iff it is provable. So the provability of any universally true sequent $A \vdash B$ is witnessed by the model given by the representable over $\{ \vec{x}.A \}$.