First-Order Categorical Logic: The Series

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.

First-Order Categorical Logic 7: We resume (after five years) with a recap. Also some MW misconceptions which JB clears up.

First-Order Categorical Logic 8: Recap of the adjoints. Injections give quantifications, surjections give equalities.

First-Order Categorical Logic 9: B(f) is a boolean algebra homomorphism. What can we say about its adjoints? Also, Toby Bartel’s general formulas for the adjoints.

First-Order Categorical Logic 10: We finish deriving the equations and inequalities of post 8 via categorical arguments.

First-Order Categorical Logic 11: A model is a natural transformation F:B→C, where B is “syntactic” and C is “semantic”. The empty structure is not a model of an inconsistent theory! A clarification on what morphisms we allow in BoolAlg. The “key question”: does the natural transformation play nicely with quantifiers?

First-Order Categorical Logic 12: Respecting quantifiers and the Beck–Chevalley condition.

First-Order Categorical Logic 13: No free lunch: constructing counter-examples to the B–C condition for respecting quantifiers. A three layer cake, with morphisms of hyperdoctrines on the top. Are we finally ready to prove the Gödel completeness theorem?

First-Order Categorical Logic 14: The Stone Representation Theorem, and how it might help provide a proof of Gödel’s Completeness Theorem. A test case: DLO, the theory of Dense Linear Orderings without endpoints.

Some Links

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

Bibliography

Joseph G. Rosenstein. Linear Ordering. Academic Press, 1982.