I am interested in a more specific reference or explanation of "the categorical view" explained in the article http://ncatlab.org/nlab/show/theory#CategoricalView. In particular, I am interested in trying to prove full completeness for a geometric model of multiplicative linear logic and I want to use a category theoretic approach in order to do so. So, when it is mentioned that

Models of a theory $\mathcal{T}$ are identified with functors $$C_{\mathcal{T}} \rightarrow \textbf{Set}$$ that preserve some (typically property-like) structures on $C_{\mathcal{T}}$, such as certain classes of colimits or limits, pertinent to the logic at hand, where $C_{\mathcal{T}}$ is the syntactic category of terms for the theory $\mathcal{T}$.

I interpret that as being that for a particular model of a theory, I want to define a functor which can be identified with that theory (in my case, the geometric model of multiplicative linear logic). Yet, I am unsure as to how I would know what properties I want it to preserve on $C_{\mathcal{T}}$.

Furthermore, the article mentions that a completeness theorem would be the statement that

the canonical map $$C_{\mathcal{T}} \rightarrow \prod_{\text{models in $\textbf{Set}$}} \textbf{Set}$$ is a full faithful embedding.

In this context, how would I prove completeness for one model of the theory, or does only refer to completeness of a theory in all possible models of that theory? In particular, a proof of the full completeness of multiplicative linear logic was given by Samson Abramsky and Radha Jagadeesan in "Games and Full Completeness for Multiplicative Linear Logic (1994)" Does this mean that completeness is proved for multiplicative linear logic in general, or just for the game-theoretic model defined in the paper?

To summarize, my questions are as follows:

1) Given a language for a signature (in the syntactic view of a theory), how do I define a functor $C_{\mathcal{T}} \rightarrow \textbf{Set}$ which can be identified with this theory?

2) In the categorical view, is completeness of a theory defined over all models for that theory, or can we prove completeness for a specific model of that theory. If the later holds, what exactly do I need to prove is a full faithful embedding?


"I interpret that as being that for a particular model of a theory, I want to define a functor which can be identified with that theory"

This sentence seems wrong. The theory itself isn't any functor, but rather the category CT. Or, if you allow models in arbitrary categories with the right sort of structure (the technical word is 'doctrine', which is a particular sort of 2-category), then the theory is the identity functor on CT (for example, geometric logic has the doctrine of categories in which geometric logic can be interpreted, and the syntactic category of a geometric theory is one of these categories. Since $Set$ is a Boolean topos, you can basically interpret any sort of theory in it. But in instances like this, you only think of it as having just the structure that the syntactic category has.

The answer your first question, then, is that you are asking the wrong question. You are in a sense asking: "given a syntactic description of a theory, how to I construct a model which is that theory?" You may instead want to ask how to construct the syntactic category $C_T$. If so, that can be supplied ;-)

In answer to your second question, it only refers to all possible models, in that the theory can be reconstructed from all models (as a subcategory of the product on the right), or that truth in the theory corresponds to truth in all possible models, since the theory embeds fully faithfully -- diagonally -- in the product over all models.

| cite | improve this answer | |
  • $\begingroup$ I don't know about the implicit question about linear logic in the body of your post, I'm afraid. $\endgroup$ – David Roberts Feb 11 '13 at 7:05
  • $\begingroup$ @David Roberts: Thank you for the response, it seems that when you are initially learning about these topics that you end up asking the wrong questions due to a lack of understanding. If you are willing to give an explanation of how to construct the syntactic category, I would love to read it! $\endgroup$ – Samuel Reid Feb 11 '13 at 7:11
  • 1
    $\begingroup$ I could, but not right now! An easier, warm-up case to consider is that of a Lawvere theory, which is a special sort of theory which only uses equational logic. The syntactic category can either be seen as some small category with finite products, such that every object is isomorphic to a finite power of a specified object, or equivalently as the opposite of the category of finitely generated free models for the theory. There is a more general description at ncatlab.org/nlab/show/syntactic+category, with some cryptic remarks as to how that relates to what I just wrote. $\endgroup$ – David Roberts Feb 11 '13 at 7:18
  • $\begingroup$ Another next step up is limit sketches (corresponding to infinitary essentially algebraic theories), and there is a powerful theorem that says any locally presentable category is the category of models for a limit sketch. $\endgroup$ – David Roberts Feb 11 '13 at 7:23
  • $\begingroup$ If I remember correctly, the situation for MLL is a little simpler than that. The proof of completeness for propositional logic using interpretation in a Boolean algebra for a simpler example along similar lines. $\endgroup$ – François G. Dorais Feb 11 '13 at 7:29

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.