A Day of Bounded Arithmetic

Slides: Model-theoretic proofs of witnessing

Abstract:

There is a model-theoretic proof of the witnessing theorem for S^1_2 due to [Zambella'96]. His approach was later generalized by [Avigad'01] who uses the notion of Herbrand-saturated models to prove several conservation results. One drawback of this framework is that it only works for universal theories. Although this issue was resolved by [CFL'07], their generalization is not particularly suitable for proving witnessing theorems.
I will introduce a framework tailored for proving witnessing theorems for \forall\Sigma^b_1-formulas and show how it is applied to obtain the witnessing theorem for T^1_2.

Slides: Separations in Bounded Arithmetic via Real Closed Fields

Abstract:

This talk provides an introduction to the use of real closed fields in bounded arithmetic, with a particular focus on separating weak theories within Buss’s hierarchy. We begin by discussing Shepherdson’s model and the independence of the statement “√2 is irrational” on IOpen. We then present the separation of Σ^b_0−IND from the rest of Buss’s hierarchy, highlighting the role played by real closed fields in the construction. Finally, we describe a particular open problem and suggest a possible approach to its resolution.

Slides: Proof complexity of non-classical systems

Abstract:

One of the fundamental challenges in proof complexity is to establish lower bounds on the size of proofs in various propositional proof systems. While this goal remains elusive for strong systems like classical Frege, the past two decades have seen significant progress by turning to non-classical logics. This line of research has produced exponential lower bounds on proof size and/or number of lines for a diverse range of systems, including Frege systems for intuitionistic and modal logics (Hrubes '07, '09), superintuitionistic and modal logics of infinite branching (Jerabek '11), propositional default logic (Beyersdorff et al. '11), and intuitionistic substructural logics (J.'21).

In this talk, we will provide an introduction to this field, focusing on a result that provides a unified framework for many of these lower bounds. We will present the construction of the hard tautologies (a negation-free adaptation of Hrubes's formulas due to Jerabek) and sketch the proof technique. This line of work has recently been extended to the classical substructural logics, which had resisted the usual techniques due to their classical character (Akbar Tabatabai, J. '26).

Slides: On the Power of Structural Rules in Frege Systems

Abstract:

Proving proof-size lower bounds for the Frege system, or equivalently for the sequent calculus LK, remains a major open problem in proof complexity. We shed new light on this challenge by isolating the power of the structural rules, namely weakening and contraction in LK, and showing that the combination of both rules is significantly stronger than either rule alone. More precisely, we establish exponential (resp. sub-exponential) proof-size lower bounds for LK without contraction (resp. weakening) for formulas that admit short LK proofs. We also show that the power of the cut rule alone goes far beyond the combination of the two structural rules. To this end, we exhibit formulas with polynomial-size proofs using cut but not the structural rules, which nevertheless require exponential-size proofs in cut-free LK where both structural rules are present but cut is absent.

It is based on a joint work with Raheleh Jalali.

Slides: A Theory for Probabilistic Polynomial-Time Reasoning

Abstract:

In this work, we propose a new bounded arithmetic theory, denoted APX1, designed to formalize a broad class of probabilistic arguments commonly used in theoretical computer science. Under plausible assumptions, APX1 is strictly weaker than previously proposed frameworks, such as the theory APC1 introduced in the seminal work of Je?ábek (2007). From a computational standpoint, APX1 is closely tied to approximate counting and to the central question in derandomization, the prBPP versus prP problem, whereas APC1 is linked to the dual weak pigeonhole principle and to the existence of Boolean functions with exponential circuit complexity.

A key motivation for introducing APX1 is that its weaker axioms expose finer proof-theoretic structure, making it a natural setting for several lines of research, including unprovability of complexity conjectures and reverse mathematics of randomized lower bounds. In particular, the framework we develop for APX1 enables the formulation of precise questions concerning the provability of prBPP=prP in deterministic feasible mathematics. Since the (un)provability of P versus NP in bounded arithmetic has long served as a central theme in the field, we expect this line of investigation to be of particular interest.

Our technical contributions include developing a comprehensive foundation for probabilistic reasoning from weaker axioms, formalizing non-trivial results from theoretical computer science in APX1, and establishing a tailored witnessing theorem for its provably total TFNP problems. As a byproduct of our analysis of the minimal proof-theoretic strength required to formalize statements arising in theoretical computer science, we resolve an open problem regarding the provability of AC0 lower bounds in PV1, which was considered in earlier works by Razborov (1995), Krají?ek (1995), and Müller and Pich (2020).

Slides: Meta-mathematics of Algebraic Circuit Lower Bounds

Abstract: 

We initiate the study of the meta-mathematics of algebraic circuit lower bounds, aiming both to gain insight into the methods sufficient and necessary to prove algebraic circuit lower bounds, and to contribute to the study of bounded arithmetic as a logical foundation for complexity lower bounds. In particular, we focus on the question of which formal theories and proof systems can efficiently prove algebraic circuit lower bounds, as follows.

\item[Formalization of Rank Method] Typically, algebraic circuit lower bounds are shown using the ``rank method", i.e., by exploiting non-trivial upper bounds on the rank of matrices derived from the monomial coefficients of polynomials computable by small algebraic circuits.  A recent prominent application of this method is in the constant-depth algebraic circuit lower bounds by Limaye, Srinivasan and Tavenas~\cite{LST25} for the determinant and iterated matrix multiplication over fields of characteristic zero, and the finite field analogue of these results by Forbes~\cite{For24}. We show that these rank-based arguments can be formalized in the bounded arithmetic theory $\VNCTwo$, which captures ``reasoning with \NCTwo~concepts''. This complements the work of Tzameret and Cook \cite{TC21}, who showed that basic structural \emph{upper} bounds in algebraic circuit complexity can be formalized   in \VNCTwo. Moreover, it offers a unified proof-theoretic framework in which to formulate and study barriers for current algebraic complexity methods (complementing specific barriers discovered by Efremenko, Garg, Oliveira, and Wigderson~\cite{EGOW18} and Garg, Makam, Oliveira, and Wigderson~\cite{GMOW19}).

\item[Unconditional \PCR\ lower bounds] We show that Polynomial Calculus Resolution (\PCR) cannot efficiently prove superpolynomial algebraic circuit lower bounds for any family of polynomials. Moreover, \PCR\ cannot efficiently prove exponential constant-depth circuit lower bounds for any family of polynomials.

\item[Conditional constant-depth \IPS\ lower bounds] We introduce the Tensor Rank Principle and demonstrate it is hard for PCR. We show that if this principle is hard against constant-depth Ideal Proof System (\IPS) then constant-depth  \IPS\ cannot efficiently prove constant-depth algebraic circuit lower bounds.