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

 A: 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.
A: 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.)
