Expressive power of digraph solvability (Q409316)

A directed graph (digraph) is said to be solvable if it has a kernel. A kernel is an independent set of vertices \(K\) such that for every vertex \(v\) not in \(K\) there is an edge from \(v\) to some vertex of \(K\). An overview of kernel theory can be found in the work of \textit{E. Boros} and \textit{V. Gurvich} [Discrete Math. 306, No. 19--20, 2336--2354 (2006; Zbl 1103.05034)]. Solvability of digraphs is related to solvability of systems of Boolean equations. Consequently, the solvability problem for digraphs is closely related to satisfiability in both finite and infinitary propositional logic theories. Capitalizing on this connection, the authors prove that the solvability problem for digraphs is \(\Sigma^1_1\)-complete, and then conclude that the consistency of PL\(^\omega\)-theories is also \(\Sigma^1_1\)-complete. Applying the methods of reverse mathematics, they prove that the solvability of countable, finitely bounded, acyclic digraphs is equivalent to WKL\(_0\) over RCA\(_0\). The authors note that in [``Kernel tower theory. I'', FOM 407 (email list) (2010), \url{http://cs.nyu.edu/pipermail/fom/2010-March/014507.html}] \textit{H. Friedman} states that solvability of well-founded dags is equivalent to ATR\(_0\) over RCA\(_0\). Turning to set theory, they show that ZF proves that every tree is solvable, and that weak forms of AC prove that forests are solvable. The paper concludes with a proof that over ZF, full AC is equivalent to the solvability of disjoint unions of indexed families of solvable digraphs.