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.
Diagonal Argument 