Theorem for some structure that it cannot be axiomatized in any language? Godel’s theorem states that there cannot be an enumerable axiomatization of arithmetic $(\mathbb N,0,1,+)$ in first order logic. By implication, there cannot be any axiomatization in any language that is complete. 

But this doesn’t mean that arithmetic cannot be axiomatized at all. E.g. we have second order Peano axioms that characterizes arithmetic up to isomorphism. It just means that we cannot derive all propositions from this axiomatization (which is possible because second-order logic is not complete).

My question is: is there a different theorem, similar in spirit to Godel’s, for some mathematical structure that can be constructed explicitly, that there cannot be an axiomatization that characterizes it up to isomorphism, in any language? (I.e. not first order, or second order, or higher order, or anything else that I don’t know about).

Intuitively, I would guess there might be, because: There is only a countable amount of possible enumerable axiomatizations in all languages combined, since there is only a countable amount of Turing machines. On the other hand there is an uncountable amount of structures. So there must be some structure that cannot be axiomatized. My question is whether there is an explicit constructable structure where we know that it cannot be.
A crucial point in your question is the following broad claim:

There is only a countable amount of possible enumerable axiomatizations in all languages combined, since there is only a countable amount of Turing machines.

There's an implicit restriction here to logics which are &quot;computably describable.&quot; Of course this is necessary to hope for a positive answer, but it's not immediately clear what this should mean - especially since you explicitly want to include things like second-order logic whose semantics are absurdly complicated.
One possible idea is the following: roughly, say that a definable logic consists of a computable set of things we call sentences and a semantics given by a formula in the language of set theory. This encapsulates all the higher-order logics, computable infinitary logic, and so forth. I don't know of a single candidate for a natural logic which has countably many sentences but is not a definable logic in the above sense, so this seems reasonable.
It turns out, however, that it is consistent that every structure can be pinned down up to isomorphism by some sentence in some definable logic. This is a consequence of the existence of pointwise-definable models; the obstacle to the &quot;obvious&quot; proof of contradiction here is that definable logics can be arbitrarily complicated to define in terms of the Levy hierarchy so we can't definably diagonalize against them (per Tarski).
In fact, even handling second-order logic alone is quite difficult. While a quick counting argument shows that there must be a countable structure which is not pinned down up to isomorphism by any computable set of second-order sentences, there is no known candidate, and in fact it is consistent with $\mathsf{ZFC}$ that every countable structure is pinned down up to isomorphism by its full second-order theory (see the discussion here). And any attempt to develop a &quot;Godel-flavored&quot; analysis of second-order logic immediately runs into the problem that the entailment relation for second-order logic is not second-order definable in arithmetic (in contrast with the situation for first-order logic, which follows from the completeness theorem).

That said, there is a version of Godel's first incompleteness theorem which applies to any (set-sized) logic.
First, let me prove my statement above about the complexity of the second-order entailment relation. The syntax for $\mathsf{SOL}$ is computable, and there is a second-order sentence $\theta$ which pins down $\mathbb{N}$ up to isomorphism. If the second-order entailment relation were second-order definable over $\mathbb{N}$, the full second-order theory of $\mathbb{N}$ would be second-order definable in $\mathbb{N}$. This would give us a second-order-definable-over-$\mathbb{N}$ listing of the second-order-definable-over-$\mathbb{N}$ sets; diagonalizing against that listing would give us a contradiction. (This last sentence is really just Tarski's argument, but I think this phrasing makes it easier to think about.)
This generalizes in a precise, if messy, way to any context where we have a logic $\mathcal{L}$ and a structure $\mathbb{A}$ sufficient for developing the syntax of $\mathcal{L}$ (this generalizes $\mathbb{N}$). Then either $\mathcal{L}$-entailment is too complicated to define in $\mathbb{A}$, or no good approximation to the $\mathcal{L}$-theory of $\mathbb{A}$ (this generalizes &quot;no consistent completion of $\mathsf{Q}$&quot;) is &quot;nicely definable&quot; in $\mathbb{A}$.
Incidentally, this idea leads to a proof of the usual first incompleteness theorem which is &quot;purely model-theoretic&quot; in a precise sense, see here (although I don't know its exact provenance). And while the added generality seems useless for the most part, I did use the more general version above to prove a small result about infinitary logics in a relatively short way.
If I understand the question correctly, you can always construct a halting problem.  You can make a second-order system first order by importing the second-order concepts as first-order axioms, and then you just have the halting problem with your additional axioms.
For instance, let's say that you have a set of operations A.  You can construct a halting problem based on A.  Now, let's say that you have another set of operations B, which includes all of A plus a halting oracle for A.  This set of operations will then itself be subject to a halting problem.
I think Turing covers this in &quot;Systems of Logic Based on Ordinals&quot;.