Document type
Master thesisPublication date
Publication license
Please use this identifier to cite or link to this item: https://hdl.handle.net/2445/215181
A Formalization of Kannan’s Circuit Lower Bound in Bounded Arithmetic
Journal Title
Authors
Director/Tutor
Journal ISSN
Volume Title
Related resource
Abstract
The aim of this work is to formalize the circuit-size lower bound showed by Kannan in 1982
in a weak theory for feasible computations. In particular, we will work with theories of
bounded arithmetic, which are subtheories of Peano Arithmetic that weaken its induction
axiom scheme by restricting it to formulas in which the quantifiers are bounded. Kannan’s
circuit lower bound states that for every fixed polynomial size of circuits, there is a language
in the second level of the polynomial hierarchy that cannot be decided by circuits of that
size. We note that the essential ingredient in this proof is a key use of the weak pigeonhole
principle, which is available in bounded arithmetic. Instrumental in the proof of Kannan’s
Theorem is the celebrated Karp-Lipton’s Theorem, stating that if the satisfiability problem
for propositional formulas can be decided by polynomial-size circuits then the polynomial
hierarchy collapses to its second level, which we also formalize in the same theory
Description
Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona. Curs: 2024-2024. Tutor: Albert Atserias
Subject (English)
Citation
Citation
CANTERO DE ARRIBA, Carlos. A Formalization of Kannan’s Circuit Lower Bound in Bounded Arithmetic. [consulted: 7 of June of 2026]. Available at: https://hdl.handle.net/2445/215181