## Syntax in categorical logic

**Abstract:**

Last time, March 10th, I departed from the previously
announced subject, and got down to basics about completeness in
categorical logic. Joseph Helfer asked a question (one of several of
his questions) that, I am sure he felt too, was not adequately
addressed (for lack of time, of course): how the completeness of (any)
one specific deductive system for first-order logic is related to the
categorical completeness for coherent categories I was talking
about. This has a "short" answer, which I will start with next time -
but it also has a long answer, which involves the story of how syntax
has been dealt with in categorical logic. There is a, to some extent,
justifiable first impression, namely that categorical logic suppresses
syntax, and thereby obliterates something that is deservedly held to
be central in mathematical logic: logical complexity.
(What is the main theorem of logic? The abstract completeness theorem:
first-order logical validity is a recursively enumerable concept, in
fact, complete-r.e., *i.e.* (complete) SIGMA-ZERO_ONE in the
arithmetical hierarchy, which is a hierarchy based of logical
complexity based on counting unbounded quantifiers in the defining
formulas - and (therefore), it (validity) is not recursive, *i.e.*,
not DELTA-ZERO, (equivalently, not PI-ZERO-ONE), in that
hierarchy. [Theorem due to Godel and Church: go to S.C. Kleene: Intro
to Metamathematics, 1952 and numerous later editions.])

I will endeavor to counteract the above "first impression" by talking
about the following topics: 1) the fibrational formulation of logic;
2) the generalized sketch approach to syntax; 3) FOLDS = first-order
logic with dependent sorts, 4) computads as the syntax for the logic
of higher categories. This may sound a lot -- but I want to give some
idea where categorical logic has gone since the subject of our book
with Gonzalo Reyes of 1977.

## Supplemental notes