nLab 3-theory

Idea

In the context of an account of logic described in terms of $n$-theories (Shulman 18a), a 3-theory specifies a kind of 2-category. It does so by prescribing the allowable judgment structures of the 2-theories that can be expressed within it.

Examples

1. The 3-theory of (totally unstructured) 2-categories. Syntactically, this corresponds to “unary type (2-)theories” with judgments such as $x:A \vdash b:B$ with exactly one type to both the left and the right of the turnstile (LS 15).

2. The 3-theory of cartesian monoidal 2-categories (or cartesian 2-multicategories). Syntactically, this corresponds to “simple type (2-)theories” with judgments such as $x:A, y:B, z:C \vdash d:D$ with a finite list of types to the left but exactly one type to the right, and no dependent types (LSR 17).

3. The 3-theory of first-order logic. Syntactically, this corresponds to type 2-theories with one layer of dependency: there is one layer of types which cannot depend on anything, and then there is a second layer of types (“propositions” in the logical reading) which can depend on types in the first layer, but not on each other. 2-theories here are for hyperdoctrines and indexed monoidal categories, and include (typed) first-order classical logic, first-order intuitionistic logic, first-order linear logic, the type theory of indexed monoidal categories, first-order modal logic, etc. Semantic 2-theories in this 3-theory should be a sort of “2-hyperdoctrine”. A higher-order logic is a 2-theory which adds rules specifying a universe of propositions.

4. The 3-theory that corresponds syntactically to “dependent type (2-)theories” with judgments such as $x:A, y:B(x), z:C(x, y) \vdash d:D(x, y, z)$. The semantic version of this should be some kind of “comprehension 2-category” (Shulman 18b). Homotopy type theory is a 2-theory defined in this 3-theory.

5. The 3-theory that corresponds syntactically to “classical simple type (2-)theories” with judgments such as $A,B,C \vdash D,E$ that allow finite lists of types on both sides of the turnstile. For instance, the 2-theory of $\ast$-autonomous categories (classical linear logic), and also of Boolean algebras (classical nonlinear logic), live in this 3-theory, as does the 2-theory for symmetric monoidal categories described in (Shulman 19). Variants would allow composition along multiple types at once (corresponding to a prop), composition only along one type at a time (corresponding to a polycategory), or both.

6. The classical 3-theory that extends the first-order 3-theory by allowing multiple sequents. (The term ‘classical’ here and above owes its origin to the contrast between systems LK and LJ of Gentzen's sequent calculus, where LJ provides a proof system for intuitionistic logic via restriction to single sequents of the rules of LK for classical logic. This naming practice leads to a certain confusion as it is quite possible to represent classical first-order logic in a single sequent system such as Gentzen’s NJ.)

A 3-theory may be said to subsume another 3-theory, in the sense that a 2-theory written in the latter may be formulated in the former. Here the first four 3-theories are ordered in terms of increasing expressivity. (5) subsumes (2), and (6) subsumes (3), but (4) and (5) are not comparable.

Modal variants of 2-theories may be defined in 3-theories where the types appearing in judgments are indexed by a system (2-category) of modes (Shulman 18b).

References

• Mike Shulman, What Is an n-Theory?, (blog post)

• Dan Licata, Mike Shulman, Adjoint logic with a 2-category of modes, in Logical Foundations of Computer Science 2016 (pdf, slides)

• Daniel Licata, Mike Shulman, and Mitchell Riley, A Fibrational Framework for Substructural and Modal Logics (extended version), in Proceedings of 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (doi: 10.4230/LIPIcs.FSCD.2017.25, pdf)

• Mike Shulman, Type 2-theories, (HoTTEST seminar)

• Dan Licata, Synthetic Mathematics in Modal Dependent Type Theories, tutorial at Types, Homotopy Theory and Verification, 2018 (pdf)

• Mike Shulman, A practical type theory for symmetric monoidal categories, (arXiv:1911.00818)