Feasible Proofs of Szpilrajn's Theorem – A Proof-Complexity Framework for Concurrent Automata
Michael J. Soltys · 2011
The aim of this paper is to propose a proof-complexity framework for concurrent automata. Since the behavior of concurrent processes can be described with partial orders, we start by formalizing proofs of Szpilrajn's Theorem. This theorem says that any partial order may be extended to a total order. We give two feasible proofs of the finite case of Szpilrajn's Theorem. The first proof is formalized in the logical theory LA extended to ordered rings; this yields a $\mathsf{TC}^0$ Frege derivation. The second proof is formalized in the logical theory $\exists$LA and yields a P/poly Frege derivation. Although $\mathsf{TC}^0$ is a much smaller complexity class than P/poly, the trade-off is that the P/poly proof is algebraically simpler -- it requires the algebraic theory LA over the simplest of rings: $\mathbb{Z}_2$.