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