Question

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

Answer 1

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 n^th ordinal notation system is between Π¹_n-1-CA and Π¹_n-1-CA₀ (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.