MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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)?

share|cite|improve this question
up vote 5 down vote accepted


…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.

share|cite|improve this answer
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.)

share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.