Does Taranovsky's system of ordinal notations make sense? Dmytro Taranovsky has a Web page on which he claims to define a system of ordinal notations strong enough to provide an ordinal analysis of full second-order arithmetic.  I think (perhaps unjustly) that this claim is suspicious, since from my passing acquaintance with the subject I seem to understand that the state of the art of ordinal analysis was around $\Pi^1_2$-comprehension (e.g., Jan-Carl Stegert's doctoral dissertation building on work by Michael Rathjen), the ordinal notation systems involved are considerably more complex (reflection instances, collapsing hierarchies), and Taranovsky mentions none of this.  On the other hand, a superficial look at his page does seem to make some kind of sense, and my interest in the subject is to choose the largest possible system of ordinal notations which isn't too fastidious to implement on a computer (i.e., I'm not concerned with the proof-theoretic aspect).
So before I decide to read it in great detail or not, I'd like an expert's opinion: what is to be thought of Taranovsky's ordinal notation systems?  (Might they define an ordinal which is not as large as claimed?  Or perhaps which could be as claimed but would be very difficult to analyse?)
 A: In this section of the paper Taranovsky gave a proof of well-foundedness of the system for the $C_0,C_1$ and $C_2$ subsystems of the version of $C$ defined in "Built-from-below with Passthrough for Lower Levels", and then, using a different approach, does so for $C_i$ for all $i$. The proof for $C_0,C_1,C_2$ is in ZFC, while the proof for $C_i$ is in ZFC + Measurable Cardinal. It's important to note that the system up to $C_\omega$ is (probably) bounded by $C(C(\Omega_2\omega,0),0)$ for the main system. People often confuse $C_i(\alpha,\beta)$ with the $n=i$ system of the main $C$. "Built from below with passthrough" C is believed to be bounded by $C(C(\Omega_2\omega,0),0)$ because for each $i$, the limit of everything constructible in $C_i(\alpha,\beta)$ for $\alpha,\beta$ are standard in the language of $\bigcup C_i$, where all ordinals $\eta$ standard in $C_n$ are built from below with passthrough by $C_{n+1}$ standard ordinals above $\eta$, seems to be $C(C(C^{i+1}(\Omega_2,\Omega_2),0),0)$ in it's standard representation where $C^0(\alpha,\beta)=\beta\land C^{n+1}(\alpha,\beta)=C(\alpha,C^n(\alpha,\beta))$. If this is true, it would imply that the limit of everything constructible in $C_i$ is $C(C(\Omega_2i+\Omega_2,0),0)$. For lower values of $i$, this seems to hold. $C_0$ is only allowed to use ordinals build from below by other ordinals within it, so in can only hold finite expressions and nothing of the form $C(\alpha,\beta)$ for uncountable ordinals $\alpha,\beta$, and is therefore limited by the least $\alpha$ such that $\alpha\mapsto C(\alpha,0)$, which happens to be $\varepsilon_0$. In the main notation, $\varepsilon_0=C(\Omega_1,0)$ which is in its standard representation in the $n=1$ system and is in the standard representation $C(C(\Omega_2,0),0)$ in the $n=2$ system. Simple enough analyses can show that the limit to everything constructible in $C_1$ is $C(C(\Omega_2 2,0),0)$ and Taranovsky showed a brief conjecture and explanation of how $C(C(\Omega_2 3,0),0)$ is possibly the limit to everything expressible in $C_2$, but a full induction for $\sup\{C_i(\alpha,\beta):\alpha,\beta\in \bigcup C_i\cap\text{Stand}\}=C(C(\Omega_2\cdot(i+1),0),0)$ implying the same sentence for $C_{i+1}$ has not been proven yet.
It's interesting that Taranovsky wasn't able to provide a proof for $C_i$ for all $i$ within ZFC and had to resort to assuming the existence of Measurable Cardinals in order to prove well-foundedness for $C_i$. Perhaps such proof doesn't exist, or perhaps it does exist but it's very long and complicated and hard to think of, possibly stretching the limits of ZFC. If a theory $T$ can prove well foundedness of a recursive ordinal notation, then the limit of that notation is an ordinal below the proof-theoretic ordinal of $T$. If ZFC can't prove $C_\omega$ recursive/well-founded and the language of $C_i$ is limited by $C(C(\Omega_2i+\Omega_2,0),0)$ are both correct, then that would imply that $C(C(\Omega_2\omega,0),0)$ is equal to or larger than the proof-theoretic ordinal of ZFC. This is highly unlikely, because a proof in ZFC for $C_i$ most likely exist and not even Taranovsky himself has given such high possible values for $C(C(\Omega_2\omega,0),0)$, which was actually proposed to be the proof-theoretic ordinal of Second Order Arithmetic by the most recent analysis.
Originally, Taranovsky believed that the limit of each $n+1$ system is within the range of $\vert\Pi^1_n-\text{CA}_0\vert_\text{Con}$ and $\vert\Pi^1_{n+1}-\text{CA}_0\vert_\text{Con}$, which is now considered wrong, and the overall system is believed to be much stronger. This is where the position of the "n-shiftedness" property comes in. This is perhaps the most important property when it comes to the strength of Taranovsky's $C$ and is one of the reasons it's so hard to analyse.
Firstly, since the ordinal notation uses a simple comparison algorithm, the strength of the notation depends almost entirely on one factor - how strong "n-built from below" works for sufficiently large ordinals. In basic terms, $\alpha$ is 0-built from below by $\beta$ iff $\alpha<\beta$ and $\alpha$ is $k+1$-built from below by $\beta$ iff the standard representation of $\alpha$ does not use ordinals above $\alpha$, except for ordinals in the scope of an ordinal that is $k$-built from below by $\beta$. We say an ordinal $\alpha$ is in the scope of an ordinal $\beta$ iff $\alpha$ appears somewhere in the standard representation of $\beta$ within the lexicographic string in the language $\{C,0,\Omega_n\}$ that represents precisely $\beta$ within the respective $n$ system.
The main system was intended to be an attempt to extend a notation Taranovsky previously made called "Degrees of Reflection", defined using a similar (but not identical) built-from-below condition, and the $n=2$ system was intended to be identical to it, namely a term in Degrees of Reflection would have roughly the same behavior as that term with all instances of $\Omega$ replaced with $\Omega_2$. But in 2014, Taranovsky discovered the $n=2$ main system is stronger, because of an irregular phenomenon happening as long as the left argument of $C$ is larger than $\Omega_2$: in many cases replacing some of Degrees of Ref.'s $\Omega$ with just $C(\Omega_2,C(\Omega_2 2,0))$ is enough. For example, $C(\Omega^\Omega,0)\, =\, C(\Omega+\Omega^\Omega,0)$ in Degrees of Ref. is expected to have similar behavior to $C(\Omega_2+C(\Omega_2,C(\Omega_2 2,0))^{C(\Omega_2,C(\Omega_2 2,0))},0)$ in the main system. Note that this fails when the left argument of the main system C is less than $\Omega_2$, for example $C(C(\Omega_2,C(\Omega_2 2,0))^{C(\Omega_2,C(\Omega_2 2,0))},0)$ (no leading "$\Omega_2+$") fails the built from below condition - this is because the built from below condition becomes sufficiently lenient enough for this to happen when $\alpha$ is large enough, since we then get subterms $<\Omega_2$ such as $C(\Omega_2,C(\Omega_2 2,0))$ "for free". Also, this phenomenon would repeat itself at higher levels in the system such as for terms like $C(\Omega_2+C(\Omega_2,C(\Omega_2 3,0),0)$. In Taranovsky's words "similar patterns repeat at different levels of the strength hierarchy." And all this is only considering the $n=2$ system!
Overall, as it turned out that n-built from below was actually stronger than expected for ordinals standard in the $n=2$ system, Taranovsky had to form a new approximation method for n-built from below, according to which, the entire notation might reach as far as the proof-theoretic ordinal of $Z_2+\text{PD}$. None of this has been confirmed, and analyses have not gone beyond $C(C(\Omega_2 2+C(\Omega_2+C(\Omega_2,C(\Omega_2 2,0))^{C(\Omega_2,C(\Omega_2 2,0))^\omega},0),0),0)$ due to exhaustion with other ordinal notations not being sufficiently strong to provide ordinals beyond that, in order to be compared further.
Unfortunately, since a couple years ago some unusual behavior that seems to be unique to the main system has been found, which makes it harder to compare with other ordinal notations. Hyp cos, the viewer mentioned a few times on Taranovsky's page, has found what they call an "erratic term" in the main system, due to how it behaves differently from not only other ordinal notations appearing in literature, but also even many of Taranovsky's other systems:

Let $a = C(\Omega_2+C(\Omega_2,\Omega_1),0)$, then $C(a+C(C(\Omega_2+C(a,\Omega_1),0),C(a,\Omega_1)),0)$ is not standard. It's standard in "Main ordinal notation system with passthrough", and "degrees of reflection", "degrees of reflection with passthrough". This is the very first erratic term.

Sadly, other than Taranovsky's notation being hard to compare with, the other reason it has not been done so much is because it hasn't yet gotten much attention from people qualified enough to do so.
A: When Taranovsky announced his system on the Foundations of Mathematics mailing list on March 23, 2012, he wrote:

I discovered a conjectured ordinal notation system that I conjecture 
  reaches full second order arithmetic.

The webpage you linked to has a slightly later date (April 7, 2012) but again, in the section "Ordinal Notation for Second Order Arithmetic," he says:

I conjecture that the strength of the nth ordinal notation system is between Π1n-1-CA and Π1n-1-CA0 (see the previous section for detailed correspondence), and thus the sum of the order types of these ordinal notation systems is the proof-theoretical ordinal of second order arithmetic.

So at the time, his claim was still conjectural.  I do not recall seeing any responses to Taranovsky's FOM post. I'd recommend you contact him directly to learn the current status.
