Completeness theorem via syntactic categories

Question

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.

Answer 1

I think this is Proposition 1.5.1 in the Elephant. As Omar Antolín-Camarena says, one first shows that the generic model is complete. Then this extends to set models, not by picking a particular representable, but by showing that the collection of all representables is jointly conservative.

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 \}$.

Regarding your `context': the law of excluded middle says that in each model any formula is either true or false, but of course not that all formulas should take the same thruth value in all models. So you've proved that group theory is incomplete, as many other theories, e.g., arithmetic.