# Are the axioms for higher category-theory effectively computable?

I ask this, although I don't conduct any research in the area, or even plan to. -- There seems to be general agreement that the axioms for higher categories grow very rapidly in complexity as the order $n$ of the category grows to infinity. I am referring to the ''algebraic style'' axioms here, axiomatising a ''maximally weak'' notion of $n$-category. I assume this makes enough sense to make the following question meaningful:

is it known (or guessed at) whether there is a Turing-machine that computes these axioms (taking the order $n$ of the category as input)?

-

Yes.

…at least, for Leinster’s reformulation of Batanin’s definition of globular operadic weak ω-category (and hence also for the finite-dimensional versions of this). Showing this is essentially a matter of repeatedly applying one lemma: if $\mathbf{T}$ is an essentially algebraic theory with a computable presentation, then the free $\mathbf{T}$-structure on a computably presented object is again computably presented. By “computably presented”, I mean essentially that the sets of operations and axioms are all computably enumerable.

In the Leinster/Batanin definition, one starts with strict $\omega$-categories (certainly a computably presentable theory, by the standard explicit axiomatisaion); by their observation above, their monad $T$ is computably presentable; from this, one can show that the theory of $T$-operads is computably presentable; similarly, then, the theory of $T$-operads-with-contraction; so the free $T$-operad-with-contraction $L$ is computably presentable.

But now the operations of the theory of weak $\omega$-categories are the elements of $L$; and the axioms are given by elements of “powers” of $L$, in the monoidal structure $\otimes$ built by $T$ and pullbacks; so these sets are all computably enumerable, so we’re done.

From here on I’m a little beyond my comfort zone, and wouldn’t want to swear that the details hold up: someone who knows realizability toposes better than I do can probably tell better whether I’ve missed some subtlety.

A nice way to look at the above argument could be to say: develop the theory of weak $\omega$-categories in $\newcommand{\Eff}{\mathcal{E}\textit{ff}} \Eff$, the effective topos — that is, repeat all the normal definitions in the internal logic of $\Eff$, to get an internal theory $\mathbf{T}^{\Eff}_\omega$. (Possibly $\mathbf{PER}$ or some other category of ‘computably presented sets and functions’ might work better than $\Eff$.)

Now, the global sections functor $\Gamma \colon \Eff \to \mathbf{Sets}$ is a left exact left adjoint, so in particular, it will commute with pullbacks and with most ‘free object’ constructions — so, with all the ingredients used in the definition of the theory of weak $\omega$-categories. So when we hit $\mathbf{T}^{\Eff}\omega$ with $\Gamma$, we just recover the original external theory $\mathbf{T}\omega$. That is, $\mathbf{T}^{\Eff}\omega$ is a computable presentation of $\mathbf{T}_\omega$

Intuitively, we’re ‘shadowing’ every construction we do in $\mathbf{Sets}$ with a computable presentation, by performing the same constructions in parallel up in $\Eff$.

This approach should also work for most other theories of higher categorical structures — power-sets and non-finite exponentiation are the main logical constructions not preserved by $\Gamma$, and off the top of my head, only the definitions of higher categories which involve topological constructions will require these.

-
Sorry about the inconsistent use of subscripts in $\mathbf{T}_\omega$, by the way; I got weird LaTeX errors when I tried to use them more consistently, and this was the least bad workaround I could find. –  Peter LeFanu Lumsdaine Jan 16 '11 at 19:41

It's an interesting question, although you could make it more precise by saying exactly which algebraic-style axioms you're talking about---there are several proposals.

Here's something between a comment and an answer. To avoid the question of which axiom system we're using, I'll just talk about 2-categories (weak ones, i.e. bicategories). 2-categories are defined in such a way that "all diagrams commute", and the same goes for n-categories in general. Sure, there's a finite axiomatization, but we only know it's the right one because it allows us to prove that "all" diagrams commute.

You can write a computer program that spits out, in turn, all the diagrams that are supposed to commute. In that sense, the axioms are recursively enumerable.

An interesting observation is that 2-categories can be finitely axiomatized. In fact, this is the axiomatization that everyone meets: you have a pentagon, and a triangle, and some naturality squares. But in principle you have an infinite collection of coherence axioms: the "all diagrams" I referred to.

So the theory of 2-categories is finitely axiomatizable, but I don't know of any explanation of why it had to be. More generally, if you take a finitely axiomatizable algebraic theory (e.g. monoids) and categorify it (obtaining e.g. monoidal categories), I don't know whether that categorified theory must inevitably be finitely axiomatizable.

(Of course, finite axiomatizability is not the same as computability, but it's a closely related question.)

-
So even fineteness of the axiom-system is somewhat non-obvious.. Well, I asked the question because of the great mathematical-philosophical importance (as I perceive it) of higher category-theory. Any argument on computablity here would surely be of great value. More exactly: WHY are these axioms so difficult, philosohically speaking? -- I'm new to MO, but I guess I will "accept" your answer (now or in an moment?). Thanks! –  Pelle Salomonsson Jan 14 '11 at 20:19
Wait a while! There are a lot of people on here who might want to weigh in on this very interesting question. –  Steven Gubkin Jan 14 '11 at 20:44
Regarding c.e. axiomatizability versus decidable axiomatizability, in first order logic every theory with a c.e. set of axioms has a decidable set of axioms. The simple trick is to replace each axiom instance $\varphi$ with a very long but equivalent formulation, such as $\varphi\wedge\varphi\wedge\cdots\wedge\varphi$, where the length of the assertion is the time that $\varphi$ is enumerated in the c.e. enumeration. The end result is a decidable axiomatization. I think the same kind of trick should work in your case. –  Joel David Hamkins Jan 16 '11 at 20:16