What is a logical formula in the language of categories? How can we express basic model theoretic concepts categorically?

Question

At the beginning of a course in Model Theory, one is introduced to the definition of signature, structure and homomorphism. It is then clear that the class of all structures over a fixed signature $L$ forms a category. Or that taking the reduction of a structure to a smaller signature gives raise to a functor.

The fact is that as we go further, we build a lot of syntax from our signature: we introduce terms, atomic formulas and then a full, possibly infinitary laguage. We speak of theories, and most fundamentally of the Tarski truth relation "$\models$".
It is not clear to me how one can formalize these syntactic concepts and their interplay with semantics categorically, and I would be very curious to know about possible vocabularies between the two fields.

For instance: what is, categorically a formula? How can we express its truth in a structure?

Any help or reference would be great, especially if introductory.

Thanks in advance

Answer 1

If I understand your question, you are looking for a categorical interpretation of first-order classical logic. I guess this paper perfectly answers your question (in particular, see p. 18 and later), if you are in a language where the only terms are individual variables (sometimes such a framework is called relational first-order logic). The paper is supposed to be self-contained.

The idea is simple. The syntactic category representing relational first-order logic is given by:

• objects are the formulas of relational first-order logic;
• arrows represent the entailment relation $\models$ between formulas ($A \models B$ means that $B$ is a logical consequence of $A$);
• composition of arrows stands for the transitivity of $\models$ (if $A \models B$ and $B \models C$ then $A \models C$).

Of course, to make it work, there are several details to check, in particular to correctly interpret quantifications.

Unfortunately the machinery required to interpret full first-order logic (with constants and function symbols) is much more complex. The aforementioned paper cites Jacobs' book for that, in particular Chapter 4 is devoted to full first-order logic.

Answer 2

If you're talking about constructing the syntax of a language internal to a category, the best development I've seen of this is in this thesis by Shawn Henry, starting p.16. The setting for this construction is a topos $\mathcal{E}$ with a natural numbers object $N$.

The idea is that you define a (relational, in this case) signature with some data,

• Objects $S,R,V$ of sorts, relation symbols, and variables,
• A morphism $a:R\to \Sigma_N (N^*S)^{[n]}$ giving the arity of each relation symbol

A structure for this signature is given by

• A morphism $d:D\to S$, which one thinks of as an indexed family of domains for each sort,
• A subobject of $a^*\Sigma_N(N^*d)^{[n]}$ (as an object in the slice category $\mathcal{E}/R$)

The constructions of formulas, theories, and the notion of a structure being a model of a theory are very fiddly, but are essentially the straightforward category theoretic interpretation of the usual set theoretic manipulations of syntax trees and subsets.

It's worth noting that the notion of syntax you end up with here can be kind of weird. Your syntactic objects may have a sheaf structure (as an example) that is figuring in to how it relates to the structure that interprets it. But in some contexts this is a feature rather than a bug.