Yes, this is easy to do, and you've done it already.
Incidentally, I really think you should look at the first section of Sacks' book, which goes into detail about computable ordinals and which I think will clear up a lot of these issues.
Your guess is already one perfectly formal definition:
The minimal natural number $n$ such that there exists an $n$-state Turing machine that computes any ordinal $\alpha$ such that the proof-theoretical ordinal of $T$ is [smaller than] $\alpha$.
(Once we fix a precise meaning of "proof-theoretic ordinal," of course.) So I don't know what additional formality you want.
I've replaced "is embedded into" with "smaller than" since the former suggests that the embedding itself should be computable, which I'm not sure you want; I think the language I've used is less suggestive.
The key point is that the phrase "computes an ordinal" is perfectly precise: we mean that the Turing machine $\Phi$ in question computes the characteristic function of a binary relation $R$ on $\mathbb{N}$ such that $(\mathbb{N}; R)$ is a well-ordering. There are no additional assumptions on the Turing machine which need to be made in order for this to make sense (although of course not every Turing machine does compute an ordinal, and the set of indices of Turing machines computing ordinals is highly complicated$^1$).
That said, there are many variations you could consider:
You could replace "smaller than" with "actually equal to." That this is different in general shouldn't be surprising: think about how (in the context of $\mathbb{N}$) the Kolmogorove complexity of $a$ can be bigger than that of $b$, even if $a<b$.
You could focus on indices as opposed to states: that is, "... such that the $n$th computable well-ordering is ..."
You could ask for an embedding of the proof-theoretic ordinal into $\alpha$ to be "effective" in some sense. E.g. you could fix a computable copy $S$ of the proof-theoretic ordinal $\theta$ of $T$ (that is, $S$ is a computable binary relation on $\mathbb{N}$ such that $(\mathbb{N}; S)$ is isomorphic to the proof-theoretic ordinal of $T$), and then look for a pair of Turing machines, one of which computes a copy of some ordinal $\ge\theta$ and the other of which computes an embedding of $S$ into that copy.
And so forth.
However, all of these approaches merely "rename" the proof-theoretic ordinal; although natural numbers are simpler than ordinals, they're not any simpler (in this context) than computable ordinals, so it's not clear that this shift gains anything.
EDIT: This part is in response to Andres' comments below.
It's worth noting that the claim "the proof-theoretic ordinal of $T$ measures the strength of $T$" has problematic aspects.
(For simplicity, let's define the proof-theoretic ordinal of $T$, $pto(T)$, as the least ordinal having no "$T$-provable" computable copy; that is, the least ordinal $\alpha$ such that there is no $e$ such that $(i)$ the $e$th Turing machine computes a copy of $\alpha$ and $(ii)$ $T$ proves that the $e$th Turing machine computes a well-ordering. As long as $T$ is $\Pi^1_1$-sound, overspill implies that $pto(T)<\omega_1^{CK}$; conversely, it's not hard to show that if $T$ is not $\Pi^1_1$-sound then $pto(T)=\omega_1^{CK}$.)
The issue is:
What information does $pto(T)$ actually give us?
Remember that the proof-theoretic ordinal lives in a broader proof-theoretic context; "measuring the strength of $T$" is generally taken to mean much more than just having some "concrete" description of $pto(T)$ (whatever that means; note that we can trivially cook up a computable copy of $pto(T)$ - namely, $$\sum_{\mbox{$T\vdash$ "$\Phi_e$ is a well-ordering"}}\Phi_e$$ - so "concrete" here is a very loaded word!). For example, we want:
A good understanding of the computable functions which $T$ proves are total (e.g. for RCA$_0$ these are exactly the primitive recursive functions).
A natural system of notations leading up to $pto(T)$ (this is arguably folded into the word "concrete" above), together with a connection between these notations and proofs from $T$ (this is the new bit).
Some fixed notation for $pto(T)$ together with a proof from a very weak theory that the well-foundedness of the ordering corresponding to this notation implies the consistency of $T$ (this is closely related to the previous bulletpoint, and really should fall out of it directly).
And probably a bunch of other things proof theorists know about but I don't.
All of this goes beyond just finding a "concrete description" for $pto(T)$. (For example, how would we figure out anything about what computable functions PA proves are total just by being told out of thin air that $pto(PA)=\epsilon_0$?) So we have to be careful: especially when talking about strong theories (like ZF), we don't want to assume out of hand that $pto(T)$ is necessarily measuring as much as we want it to.
That said, I would say that $pto(T)$ measures the strength of $T$ (at least to some extent), and in this I might disagree with Andres below. But it is important (as he pointed out) to make this issue clear; $pto(T)$ isn't some magic box which tells us everything about the strength of $T$, and divorcing it from these ambient assumptions may make it (and by extension, questions like this) less mysterious.
$^1$I've linked to Kleene's $\mathcal{O}$ here; this isn't literally the set of indices of Turing machines computing ordinals, but it is in fact "equivalent" to that set (precisely: the two sets are Turing equivalent, indeed $1$-equivalent). The general theory of Kleene's $\mathcal{O}$, and of computable ordinals in general, is developed in the first part of Sacks' book.
The recursive definition of $\eta$-unbounded elementary which you propose cannot actually be carried out in ZFC. Recall that the way recursive definitions work is that you prove by induction on $\eta$ that there is a unique function $F_\eta$ defined on $\eta$ which takes each $\alpha<\eta$ to the $\alpha$th stage of your definition. This only works if the $\alpha$th stage of your definition is a set, so that this function $F_\eta$ actually is a set (so you can quantify over such functions). In your case, you would want to be defining the class of all $\alpha$-unbounded elementary ordinals as the $\alpha$th stage, which you cannot do. (Note that for variant notions like that of $\eta$-inaccessibility, you can define the set of $\eta$-inaccessible cardinals less than $\kappa$ for any fixed $\kappa$ recursively, since $\eta$-inaccessibility of a cardinal depends only on the cardinals smaller than it. This doesn't work for $\eta$-unbounded elementary ordinals, though, since to determine whether an ordinal is $\eta$-unbounded elementary, you need to know the entire proper class of $\beta$-unbounded elementary ordinals for each $\beta<\eta$.)
Incidentally, you can carry out this definition in MK, where class quantification is allowed (and can be used in Separation, and thus in proofs by induction where you want to define "the set of counterexamples" to prove it is empty). However, your $\Sigma_4$-correctness statement then only works for statements using set quantifiers, and the recursive definition of $2$-unboundedly elementary would need to use class quantifiers (or, if you did it with set quantifiers by brute force instead of by recursion, it would need to have higher complexity, as described in Noah's answer).
Best Answer
I'll assume that $\mathsf{ZFC}$ is at least $\Pi^1_1\vee\Sigma^1_1$-sound, and use the following definition of the proof-theoretic ordinal:
Here $T$ is an "appropriate" theory - for simplicity, let's say it's a computably axiomatizable $(\Pi^1_1\vee\Sigma^1_1)$-sound extension of $\mathsf{ZFC}$.
Then we can produce a uniformly primitive recursive family of theories $(T_i)_{i\in I}$ which provably in $\mathsf{ZFC}$ has the following nice properties:
Each $T_a$ is a consistent extension of $\mathsf{ZFC}$ by a single additional axiom.
$I$ is a linear order, and the $T_i$s are ordered by strength appropriately: if $a<_Ib$ then $T_b$ proves every axiom of $T_a$.
For each $\alpha<\omega_1^{CK}$ there is some $a\in I$ such that $T_a$ is $\Pi^1_1\vee\Sigma^1_1$-sound and proves the well-foundedness of some primitive recursive ordering of type $\alpha$.
This uses a couple tricks. First, we apply Barwise-Kreisel Compactness to get a primitive recursive linear ordering $(I,<_I)$ with no hyperarithmetic descending sequences whose well-founded part has type $\omega_1^{CK}$ (these are called Harrison orders). Now for $a\in I$ let $T_a$ be $\mathsf{ZFC}$ + "The initial segment of $I$ up to $a$ is well-founded." The only way $T_a$ could be inconsistent is if $\mathsf{ZFC}$ disproves the well-foundedness of $I_{<a}$. Since $\mathsf{ZFC}$ is $\Pi^1_1$-sound, this can only happen if $a$ is in the illfounded part of $I$; since $I$ has no hyperarithmetic descending sequences, there must be some $b$ in the illfounded part of $I$ such that $T_b$ is consistent (and hence each $T_c$ is consistent for $c<_Ib$). WLOG then $T_a$ is consistent for each $a\in I$ (otherwise replace $I$ with $I_{<b}$).
The only nontrivial point now is to prove that if $a$ is in the well-founded part of $I$ (and remember that has ordertype $\omega_1^{CK}$) then $T_a$ is $\Pi^1_1\vee\Sigma^1_1$-sound. To see this, suppose $T_a$ proves some false $\Pi^1_1\vee\Sigma^1_1$ sentence $\varphi$. Then $\mathsf{ZFC}$ proves the sentence "If $I_{<a}$ is well-founded then $\varphi$," which is a false $\Sigma^1_1\vee(\Pi^1_1\vee\Sigma_1^1)$-sentence, or a false $\Pi^1_1\vee\Sigma^1_1$-sentence. But this contradicts the $\Pi^1_1\vee\Sigma^1_1$-soundness of $\mathsf{ZFC}$.
This is an old argument, but I don't know who it's due to - it may well be folklore.