The complexity of proving the discrete Jordan Curve theorem and related principles
Seminar Room 1, Newton Institute
The Jordan Curve Theorem states that a simple, closed curve divides the plane into exactly two connected components. We consider the ``discrete'' version of this theorem (JCT) where the curve lies in an nxn grid. The Theorem can be formalized as either true statements in Bounded Arithmetic or families of propositional tautologies. Here we show that the formalizations in Bounded Arithmetic are provable in some weak theories (i.e., V^0 and V^0(2)); this implies that the families of tautologies have short proofs in the corresponding propositional proof systems.
First, we formalize the theorem when the simple curve is given as a sequence of edges on the grid. We show that in this case the theorem can be proved in the theory V^0. Next, we consider the case where the input is a set of edges which generally form multiple simple closed curves. The interesting conclusion here is that the set of edges divides the plane into at least two connected components. We show that this is indeed provable in the theory V^0(2).
The related principles include the STCONN on grid graph considered by Buss [Polynomial-size Frege and Resolution Proofs of st-Connectivity and Hex Tautologies] and the nonplanarity of K3,3. STCONN is reducible to JCT, and thus it is provable in V^0(2). This improves Buss's result (that STCONN has polysize proof in TC^0-Frege).