Bounded Arithmetic and Formalizing Probabilistic Proof

The first theme of this thesis investigates the complexity class CC and its associated bounded-arithmetic theory. Subramanian defined CC as the class of problems log-space reducible to the comparator circuit value problem (CCV). Using the Cook-Nguyen method we define the two-sorted theory VCC whose provably-total functions are exactly the CC functions. To apply this method, we show CC is the same as the class of problems computed by uniform AC0 circuits with unbounded CCV oracle gates. We prove that VCC lies between VNL and VP, where VNL and VP are theories for the classes NL and P respectively. We strengthen Subramanian's work by showing that the problems in his paper are indeed complete for CC under many-one AC0 reductions. We then prove the correctness of these reductions in VCC.;The second theme of this thesis is formalizing probabilistic proofs in bounded arithmetic. In a series of papers, Jerabek argued that the universal polynomial-time theory VPV augmented with the surjective weak pigeonhole principle WPHP(L FP) for all VPV functions is the 'right' theory for randomized polynomial-time reasoning in bounded arithmetic.;Motivated from the fact that no one had used Jerabek's framework for feasible reasoning about specific interesting randomized algorithms in classes such as RP and RNC2, we formalize in VPV the correctness of two fundamental RNC2 algorithms for testing if a bipartite graph has a perfect matching and for finding a bipartite perfect matching.;Using Moser's recent constructive proof technique for the Lovasz Local Lemma, we show that VPV + WPHP( LFP) proves the existence of a satisfying assignment for every instance of k-SAT in which every clause shares a variable with up to 2k-3 other clauses. This result implies the existence of a randomized polynomial-time algorithm for find satisfying assignments such k-SAT instances.;The remainder of this thesis was motivated by the lack of fundamental probability concepts like random variables, expectation and variance in Jerabek's work, which means basic yet useful theorems like Markov's inequality, Chebyshev's inequality, linearity of expectation, etc were not available in his work. By choosing suitable definitions of random variables, approximate probability and approximate expectation, we are able prove these theorems and utilize them to prove the Goldreich-Levin theorem within the conservative extension HARDA of VPV + WPHP( LFP).