Phuong Nguyen
Bounded Reverse Mathematics
Download
Graduate Department of Computer Science, University of Toronto 2008
Abstract:
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 S_21 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 NC1)
we prove one such equivalence between the theories associated with ALogTime,
solving a problem that remains open in [Arai 2000, Pitt 2000].
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 V0- 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.
Table of Contents
- Introduction
- Preliminaries
- Theories for Small Classes
- Some Function Algebras
- The RSUV Isomorphism between VNC1 and QALV
- Theories for Relativized Classes
- The Discrete Jordan Curve Theorem
- Distribution of Prime Numbers
- Conclusion
