Expressive power of digraph solvability

A kernel of a directed graph is a set of vertices without edges between them, such that every other vertex has a directed edge to a vertex in the kernel. A digraph possessing a kernel is called solvable. Solvability of digraphs is equivalent to satisfiability of theories of propositional logic. Based on a new normal form for such theories, this equivalence relates finitely branching digraphs to propositional logic, and arbitrary digraphs to infinitary propositional logic. While the computational complexity of solvability differs between finite dags (trivial, since always solvable) and finite digraphs (NP-complete), this difference disappears in the infinite case. The existence of a kernel for a digraph is equivalent to the existence of a kernel for its lifting to an infinitely-branching dag, and we prove that solvability for recursive dags and digraphs is Σ11-complete. This implies that satisfiability for recursive theories in infinitary propositional logic is also Σ11-complete. We place several variants of the kernel problem in the axiomatic hierarchy and, in particular, prove as the main result that over RCA0, solvability of finitely branching dags is equivalent to Weak König’s Lemma. We then show that ZF proves solvability of trees and that solvability of forests requires at most a weak form of AC. Finally, a new equivalent of the full AC is formulated using solvability of complete digraphs.

► A solvable digraph is a digraph possessing a kernel.
► A kernel is an independent set such that any other vertex has an edge into to kernel.
► Solvability of digraphs is equivalent to (infinitary) propositional satisfiability.
► We study the expressivity of solvability from the standpoint of mathematical logic.
► We prove precise complexity results in recursion theory, reverse mathematics, and set theory.