# name
A Formalization of Kannan’s Circuit Lower Bound in Bounded Arithmetic

# metadata.dc.description[].value
Treballs Finals del Màster de Lògica Pura i Aplicada, Facultat de Filosofia, Universitat de Barcelona. Curs: 2024-2024. Tutor: Albert Atserias

# metadata.dc.description.abstract[].value
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

# metadata.dc.source[].value
Màster Oficial - Pure and Applied Logic / Lògica Pura i aplicada

# metadata.dc.title[].value
A Formalization of Kannan’s Circuit Lower Bound in Bounded Arithmetic