Bounded reverse mathematics
Phuong Nguyen · TSpace (University of Toronto) · 2008
First we provide a unified framework for developing theories of Bounded Arithmetic that are associated with uniform classes inside polytime (P) in the same way that Buss's theory S12 is associated with P. We obtain finitely axiomatized theories many of which turn out to be equivalent to a number of existing systems. By formalizing the proof of Barrington's Theorem (that the functions computable by polynomial-size bounded-width branching programs are precisely functions computable in ALogTime, or equivalently NC 1) we prove one such equivalence between the theories associated with ALogTime, solving a problem that remains open in [Ara00, Pit00]. Our theories demonstrate an advantage of the simplicity of Zambella's two-sorted setting for small theories of Bounded Arithmetic. Then we give the first definitions for the relativizations of small classes such as NC1, L, NL that preserve their inclusion order. Separating these relativized classes is shown to be as hard as separating the corresponding non-relativized classes. Our framework also allows us to obtain relativized theories that characterize the newly defined relativized classes. Finally we formalize and prove a number of mathematical theorems in our theories. In particular, we prove the discrete versions of the Jordan Curve Theorem in the theories V0 and V0 (2), and establish some facts about the distribution of prime numbers in the theory VTC0. Our V 0- and V0(2)-proofs improve a number of existing upper bounds for the propositional complexity of combinatorial principles related to grid graphs. Overall, this thesis is a contribution to Bounded Reverse Mathematics, a theme whose purpose is to formalize and prove (discrete versions of) mathematical theorems in the weakest possible theories of bounded arithmetic.