Stephen Cook, Antonina Kolokolova

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 >>>

Chris Pollett

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 >>>

Jan Krajicek

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 >>>

Phong Nguyen

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 >>>

Ján Pich

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 >>>

Albert Atserias, Moritz Müller, Sergi Oliva

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 >>>

Albert Atserias, Neil Thapen

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 >>>

Jan Krajicek, Igor Carboni Oliveira

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.

more >>>Moritz Müller, Ján Pich

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 >>>

Iddo Tzameret, Stephen Cook

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 >>>