No label defined (Q3840692)

Second-order arithmetic \(Z_2\) -- the theory of natural numbers and sets of natural numbers, with Peano axioms, complete induction axiom and the comprehension principle \(\text{CA}_2\) for second-order formulas -- is a natural system with a remarkable expressive power. This is illustrated in the paper under review: \(Z_2\) can represent non-trivial graph-theoretic notions and can prove interesting theorems of (algorithmic) graph theory. Indeed, something more is achieved, i.e. an ``exact classification'' in the spirit of the Friedman-Simpson program of reverse mathematics [cf. \textit{S. G. Simpson}, ``Reverse mathematics'', in: A. Nerode et al. (eds.), Recursion theory, Proc. AMS-ASL Summer Inst., Ithaca/NY 1982, Proc. Symp. Pure Math. 42, 461-471 (1985; Zbl 0578.03005) and \textit{S. G. Simpson}, Subsystems of second order arithmetic (Springer, Berlin-Heidelberg) (1999)]: the typical results prove -- modulo recursive comprehension -- that the graph-theoretic statements are equivalent to \(\text{ACA}_0\) or \(\Pi^1_1-\text{CA}_0\), where \(\text{ACA}_0\) is arithmetical comprehension while \(\Pi^1_1-\text{CA}_0\) asserts the existence of sets, which are defined using at most one universal (or existential) quantification on sets of natural numbers. For instance, the following statements capture exactly the strength of \(\text{ACA}_0\): 1. the existence of the reachability matrix for suitable directed graphs (where the reachability matrix is essentially a function on a graph telling us of any given two vertices whether there is a path joining them); 2. the existence for suitable directed graphsof a topological sorting (a map \(sort\) from a graph into the set natural numberssuch that, if there is an edge from \(u\) to \(v\), then \(\text{sort}(u)\) is less than \(\text{sort}(v)\)); 3. the existence of spanning trees for connected graphs (a spanning tree for a graph \(G\) is an acyclic connected subgraph of \(G\) containing each vertex of \(G\)). The authors also show that the following statement is equivalent to \(\Pi^1_1-\text{CA}_0\): given a sequence of (rationally weighted) directed graphs, there is a function testing of each graph whether it has a minimal spanning tree. It is conjectured that this last result also holds for undirected graphs. Recursion-theoretic aspects are also explored. For related results by the second author, see: \textit{J. L. Hirst}, ``Connected components of graphs and reverse mathematics'', Arch. Math. Logic 31, 183-192 (1991; Zbl 0725.03039).