John Baez and I have been conducting a conversation about his ideas for first-order categorical logic. This page serves as an annotated table of contents, bibliography, and general repository for supporting material.

First-Order Categorical Logic 1: Lawvere’s hyperdoctrines, related to Halmos’ polyadic boolean algebras and Tarski’s cylindric algebras. A hyperdoctrine is a special sort of functor from the category FinSet of finite sets to the category BoolAlg of boolean algebras. If *f*:*X*→*Y* is a morphism in FinSet, then think of *X* and *Y* as sets of variables. If *B* is a hyperdoctrine, then *B*(*X*) and *B*(*Y*) could be boolean algebras of logical equivalence classes of formulas, with *B*(*f*) corresponding to the substitution of variables.

First-Order Categorical Logic 2: We resolve a puzzle about variance (covariant vs. contravariant).

First-Order Categorical Logic 3: While BoolAlg is the category of boolean algebras, each boolean algebra itself can be regarded as a special kind of category. The morphisms of BoolAlg are functors. As noted in post 1, *B*(*f*) represents substitution of variables; taking adjoints in various ways gives us universal and existential quantification, as well as the equality predicate.

First-Order Categorical Logic 4: An adjoint chart. The Beck-Chevalley and Frobenius conditions: for a functor from FinSet to BoolAlg to be a hyperdoctrine, it must satisfy these, as well as being “adjointful” (each *B*(*f*) must have left and right adjoints).

First-Order Categorical Logic 5: Expressing Gödel’s completeness theorem in the language of hyperdoctrines. We show that if any of the boolean algebras in a hyperdoctrine is inconsistent (that is, has true = false), they all are. This then becomes our definition of “inconsistent hyperdoctrine” (but we change it in the next post).

First-Order Categorical Logic 6: An addendum to the previous post: a supposedly pathological ‘scaffold’ (a functor from FinSet to BoolAlg) provides the semantics for an empty structure. We decide this isn’t pathological after all, and modify our definition of ‘consistent’: *B*(0) is the 2-element boolean algebra. It follows from post 5 that if *any B*(*n*) with *n*>0 is trivial, then they *all* are, but *B*(0) could still be non-trivial.

**Some Links**

This post by John at the *n*-Category Café (Polyadic Boolean Algebras) gives some of his early thoughts.