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

-
 I've analyzed one of Taranovsky's notations (the one currently under "Degrees of Recursive Inaccessibility") and I believe that most of his evaluations of his ordinals are correct; in particular, the notation C(C(2, 0, 0), 0) does seem to be the ordinal for Pi-1-1 transfinite recursion, or psi(Omega_Omega_Omega...). So even this early notation is quite strong. However, it does seem that his notation for second-order arithmetic is simpler than purportedly much weaker notations from Rathjen. So I don't know. My first doubts start to creep in when he talks about Pi-n reflection for n > 3. – Deedlit Mar 12 at 0:52

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.

-