The Jordan curve theorem (JCT) states that a simple closed curve divides the plane into exactly two connected regions. We formalize and prove the theorem in the context of grid graphs, under different input settings, in theories of bounded arithmetic that correspond to small complexity classes. The theory V 0 (2) (corresponding to AC 0 (2)) proves that any set of edges that form disjoint cycles divides the grid into at least two regions. The theory V 0 (corresponding to AC 0 ) proves that any sequence of edges that form a simple closed curve divides the grid into exactly two regions. As a consequence, the Hex tautologies and the st-connectivity tautologies have polynomial size AC 0 (2)- Frege -proofs, which improves results of Buss which only apply to the stronger proof system TC 0 - Frege .

The Jordan Curve Theorem (JCT) states that a simple closed curve divides the plane into exactly two connected regions. We formalize and prove the theorem in the context of grid graphs, under different input settings, in theories of bounded arithmetic that correspond to small complexity classes. The theory V0(corresponding to AC0(2)) proves that any set of edges that form disjoint cycles divides the grid into at least two regions. The theory V0(corresponding to AC0) proves that any sequence of edges that form a simple closed curve divides the grid into exactly two regions. As a consequence, the Hex tautologies and the st-Connectivity tautologies have polynomial size AC0(2)-Frege-proofs, which improves results of Buss which only apply to the stronger proof system TC0-Frege.

We present a general method for introducing finitely axiomatizable "minimal" two-sorted theories for various subclasses of P (problems solvable in polynomial time). The two sorts are natural numbers and finite sets of natural numbers. The latter are essentially the finite binary strings, which provide a natural domain for defining the functions and sets in small complexity classes. We concentrate on the complexity class TC^0, whose problems are defined by uniform polynomial-size families of bounded-depth Boolean circuits with majority gates. We present an elegant theory VTC^0 in which the provably-total functions are those associated with TC^0, and then prove that VTC^0 is "isomorphic" to a different-looking single-sorted theory introduced by Johannsen and Pollet. The most technical part of the isomorphism proof is defining binary number multiplication in terms a bit-counting function, and showing how to formalize the proofs of its algebraic properties.

We introduce a finitely axiomatizable second-order theory, which is VTC/sup 0/ associated with the class FO-uniform TC/sup 0/. It consists of the base theory V/sup 0/ for AC/sup 0/ reasoning together with the axiom NUMONES, which states the existence of a "counting array" Y for any string X: the ith row of Y contains only the number of 1 bits up to (excluding) bit i of X. We introduce the notion of "strong /spl Delta//sub 1//sup B/-definability" for relations in a theory, and use a recursive characterization of the TC/sup 0/ relations (rather than functions) to show that the TC/sup 0/ relations are strongly /spl Delta//sub 1//sup B/-definable. It follows that the TC/sup 0/ functions are /spl Sigma//sub 1//sup B/-definable in VTC/sup 0/. We prove a general witnessing theorem for second-order theories and conclude that the/spl Sigma//sub 1//sup B/ theorems of VTC/sup 0/ are witnessed by TC/sup 0/ functions. We prove that VTC/sup 0/ is RSUV isomorphic to the first order theory /spl Delta//sub 1//sup b/-CR of Johannsen and Pollett (the "minimal theory for TC/sup 0/"), /spl Delta//sub 1//sup b/-CR includes the /spl Delta//sub 1//sup b/ comprehension rule, and J and P ask whether there is an upper bound to the nesting depth required for this rule. We answer "yes", because VTC/sup 0/ , and therefore /spl Delta//sub 1//sup b/-CR, are finitely axiomatizable. Finally, we show that /spl Sigma//sub 1//sup B/ theorems of VTC/sup 0/ translate to families of tautologies which have polynomial-size constant-depth TC/sup 0/-Frege proofs. We also show that PHP is a /spl Sigma//sub 0//sup B/ theorem of VTC/sup 0/. These together imply that the family of propositional tautologies associated with PHP has polynomial-size constant-depth TC/sup 0/-Frege proofs.