Reverse mathematics and rank functions for directed graphs (Q1590191)

This paper is part of the program of reverse mathematics [see \textit{S. G. Simpson}, Subsystems of second order arithmetic (Springer, Berlin) (1999; Zbl 0909.03048) for an introduction to this subject] and deals with existence and uniqueness of rank functions for directed graphs. Over the weak base theory \(\text{RCA}_0\) the system \(\text{ATR}_0\) is shown to be equivalent to the existence of a rank function for every countable well-founded directed graph. To prove uniqueness of the rank function \(\text{RCA}_0\) suffices. If the notion of rank is extended to non-well-founded graphs by assigning \(\infty\) to the vertices in the non-well-founded part of the graph then \(\Pi^1_1-\text{CA}_0\) turns out to be necessary and sufficient for the proof. Finally, \(\text{ACA}_0\) is the precise measure of the strength of the fact that a path bounded graph has a rank bounded by \(\omega\).