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.

  • 4
    $\begingroup$ 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. $\endgroup$ – Omar Antolín-Camarena Oct 10 '13 at 4:08
  • $\begingroup$ @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." $\endgroup$ – Giorgio Mossa Oct 10 '13 at 15:00

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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