We introduce a second-order system V_1-Horn of bounded arithmetic
formalizing polynomial-time reasoning, based on Graedel's
second-order Horn characterization of P. Our system has
comprehension over P predicates (defined by Graedel's second-order
Horn formulas), and only finitely many function symbols. Other
systems of polynomial-time reasoning either ... more >>>

The use of Nepomnjascij's Theorem in the proofs of independence results
for bounded arithmetic theories is investigated. Using this result and similar ideas, the following statements are proven: (1) At least one of S_1 or TLS does not prove the Matiyasevich-Davis-Robinson-Putnam Theorem and (2) TLS does not prove Sigma^b_{1,1}=Pi^b_{1,1}. Here ... more >>>

We describe a general method how to construct from
a propositional proof system P a possibly much stronger
proof system iP. The system iP operates with
exponentially long P-proofs described ``implicitly''
by polynomial size circuits.

As an example we prove that proof system iEF, implicit EF,
corresponds to bounded ... more >>>

We introduce ``minimal'' two--sorted first--order theories VL, VSL, VNL and VP
that characterize the classes L, SL, NL and P in the same
way that Buss's $S^i_2$ hierarchy characterizes the polynomial time hierarchy.
Our theories arise from natural combinatorial problems, namely the st-Connectivity
Problem and the Circuit Value Problem.
It ... more >>>

We prove that $T_{NC^1}$, the true universal first-order theory in the language containing names for all uniform $NC^1$ algorithms, cannot prove that for sufficiently large $n$, SAT is not computable by circuits of size $n^{2kc}$ where $k\geq 1, c\geq 4$ unless each function $f\in SIZE(n^k)$ can be approximated by formulas ... more >>>

The relativized weak pigeonhole principle states that if at least $2n$ out of $n^2$ pigeons fly into $n$ holes, then some hole must be doubly occupied. We prove that every DNF-refutation of the CNF encoding of this principle requires size $2^{(\log n)^{3/2-\epsilon}}$ for every $\epsilon > 0$ and every sufficiently ... more >>>

The ordering principle states that every finite linear order has a least element. We show that, in the relativized setting, the surjective weak pigeonhole principle for polynomial time functions does not prove a Herbrandized version of the ordering principle over $\mathrm{T}^1_2$. This answers an open question raised in [Buss, Ko{\l}odziejczyk ... more >>>

We establish unconditionally that for every integer $k \geq 1$ there is a language $L \in P$ such that it is consistent with Cook's theory PV that $L \notin SIZE(n^k)$. Our argument is non-constructive and does not provide an explicit description of this language.

We ask for feasibly constructive proofs of known circuit lower bounds for explicit functions on bit strings of length $n$. In 1995 Razborov showed that many can be proved in Cook’s theory $PV_1$, a bounded arithmetic formalizing polynomial time reasoning. He formalized circuit lower bound statements for small $n$ of ... more >>>

Aiming to provide weak as possible axiomatic assumptions in which one can develop basic linear algebra, we give a uniform and integral version of the short propositional proofs for the determinant identities demonstrated over $GF(2)$ in Hrubes-Tzameret [SICOMP'15]. Specifically, we show that the multiplicativity of the determinant function and the ... more >>>

We investigate randomized LEARN-uniformity, which captures the power of randomness and equivalence queries (EQ) in the construction of Boolean circuits for an explicit problem. This is an intermediate notion between P-uniformity and non-uniformity motivated by connections to learning, complexity, and logic. Building on a number of techniques, we establish the ... more >>>

A map $g:\{0,1\}^n\to\{0,1\}^m$ ($m>n$) is a hard proof complexity generator for a proof system $P$ iff for every string $b\in\{0,1\}^m\setminus Rng(g)$, formula $\tau_b(g)$ naturally expressing $b\not\in Rng(g)$ requires superpolynomial size $P$-proofs. One of the well-studied maps in the theory of proof complexity generators is Nisan--Wigderson generator. Razborov (Annals of Mathematics ... more >>>

A recurring challenge in the theory of pseudorandomness and circuit complexity is the explicit construction of ``incompressible strings,'' i.e. finite objects which lack a specific type of structure or simplicity. In most cases, there is an associated NP search problem which we call the ``compression problem,'' where we are given ... more >>>

For a class of finite graphs, we define a limit object relative to some computationally restricted class of functions. The properties of the limit object then reflect how a computationally restricted viewer "sees" a generic instance from the class. The construction uses Krají?ek's forcing with random variables [7]. We prove ... more >>>

While there has been progress in establishing the unprovability of complexity statements in lower fragments of bounded arithmetic, understanding the limits of Jerabek's theory $\textbf{APC}_1$ (2007) and of higher levels of Buss's hierarchy $\textbf{S}^i_2$ (1986) has been a more elusive task. Even in the more restricted setting of Cook's theory ... more >>>

The range avoidance problem (denoted by Avoid) asks to find a string outside of the range of a given circuit $C:\{0,1\}^n\to\{0,1\}^m$, where $m>n$. Although at least half of the strings of length $m$ are correct answers, it is not clear how to deterministically find one. Recent results of Korten (FOCS'21) ... more >>>

Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are necessary to prove a given theorem. In this work, we systematically explore the reverse mathematics of complexity lower bounds. We explore reversals in the setting of bounded arithmetic, with Cook's theory $\mathbf{PV}_1$ as the base ... more >>>

We show that there is a constant $k$ such that Buss's intuitionistic theory $\mathbf{IS}^1_2$ does not prove that SAT requires co-nondeterministic circuits of size at least $n^k$. To our knowledge, this is the first unconditional unprovability result in bounded arithmetic in the context of worst-case fixed-polynomial size circuit lower bounds. ... more >>>

The Circuit Size Hierarchy CSH$^a_b$ states that if $a > b \geq 1$ then the set of functions on $n$ variables computed by Boolean circuits of size $n^a$ is strictly larger than the set of functions computed by circuits of size $n^b$. This result, which is a cornerstone of circuit ... more >>>

The Schwartz-Zippel Lemma states that if a low-degree multivariate polynomial with coefficients in a field is not zero everywhere in the field, then it has few roots on every finite subcube of the field. This fundamental fact about multivariate polynomials has found many applications in algorithms, complexity theory, coding theory, ... more >>>

This paper studies the \emph{refuter} problems, a family of decision-tree $\mathrm{TFNP}$ problems capturing the metamathematical difficulty of proving proof complexity lower bounds. Suppose $\varphi$ is a hard tautology that does not admit any length-$s$ proof in some proof system $P$. In the corresponding refuter problem, we are given (query ... more >>>

We survey results on the formalization and independence of mathematical statements related to major open problems in computational complexity theory. Our primary focus is on recent findings concerning the (un)provability of complexity bounds within theories of bounded arithmetic. This includes the techniques employed and related open problems, such as the ... more >>>

Let $\mathcal{C}$ be a complexity class and $A$ be a language. The statement ``$A \not\in \mathcal{C}$'' is a separation of $A$ from $\mathcal{C}$. A separation is constructive if there is an efficient algorithm called a refuter that prints counterexamples to the statement ``$M$ decides $A$'' for every $\mathcal{C}$-algorithm $M$. Concretely, ... more >>>