Bounded Arithmetic and Formalizing Probabilistic Proofs

The first theme of this thesis investigates the complexity class CC\nand its associated bounded-arithmetic theory. Subramanian defined CC\nas the class of problems log-space reducible to the comparator circuit\nvalue problem (CCV). Using the Cook-Nguyen method we define the\ntwo-sorted theory VCC whose provably-total functions are exactly the\nCC functions. To apply this method, we show CC is the same as the\nclass of problems computed by uniform AC^0 circuits with unbounded\nCCV oracle gates. We prove that VCC lies between VNL and VP,\nwhere VNL and VP are theories for the classes NL and P\nrespectively. We strengthen Subramanian's work by showing that the\nproblems in his paper are indeed complete for CC under many-one\nAC^0 reductions. We then prove the correctness of these reductions in\nVCC.\nThe second theme of this thesis is formalizing probabilistic proofs in\nbounded arithmetic. In a series of papers, Jerábek argued that the\nuniversal polynomial-time theory VPV augmented with the surjective\nweak pigeonhole principle WPHP(LFP) for all VPV functions is the\n'right' theory for randomized polynomial-time reasoning in bounded\narithmetic.\nMotivated from the fact that no one had used Jerábek's framework\nfor feasible reasoning about specific interesting randomized algorithms\nin classes such as RP and RNC^2, we formalize in VPV the\ncorrectness of two fundamental RNC^2 algorithms for testing if a\nbipartite graph has a perfect matching and for finding a bipartite\nperfect matching.\nUsing Moser's recent constructive proof technique for the Lovász Local\nLemma, we show that VPV + WPHP(LFP) proves the existence of a\nsatisfying assignment for every instance of k-SAT in which every\nclause shares a variable with up to 2^{k-3} other clauses. This result\nimplies the existence of a randomized polynomial-time algorithm for\nfind satisfying assignments such k-SAT instances.\nThe remainder of this thesis was motivated by the lack of fundamental\nprobability concepts like random variables, expectation and variance in\nJerábek's work, which means basic yet useful theorems like\nMarkov's inequality, Chebyshev's inequality, linearity of expectation,\netc were not available in his work. By choosing suitable definitions of\nrandom variables, approximate probability and approximate expectation,\nwe are able prove these theorems and utilize them to prove the\nGoldreich-Levin theorem within the conservative extension HARD^A of\nVPV + WPHP(LFP).

Fetched live from OpenAlex and de-inverted. Abstracts are not stored in this database: the inverted indexes are 8.6 GB of the frame’s 9.3 GB of text, and the host has 13 GB free.