Narrow Results

We link the Dehn function of finitely presented groups to the length-of-proofs function in propositional proof complexity.

We use results from the theory of algebras with polynomial identities (PI-algebras) to study the witness complexity of matrix identities. A matrix identity of $d\times d$ matrices over a field $𝔽$is a non-commutative polynomial (f(x₁, …, x_n)) over $𝔽$, such that $f$ vanishes on every $d\times d$ matrix assignment to its variables. For every field $𝔽$of characteristic 0, every $d>2$ and every finite basis of $d\times d$ matrix identities over $𝔽$, we show there exists a family of matrix identities ${(f_n)}_{n\in \mathbb{N}}$, such that each $f_n$ has $2n$ variables and requires at least $\mathrm{\Omega }(n^{2d})$ many generators to generate, where the generators are substitution instances of elements from the basis. The lower bound argument uses fundamental results from PI-algebras together with a generalization of the arguments in [P. Hrubeš, How much commutativity is needed to prove polynomial identities? Electronic colloquium on computational complexity, ECCC, Report No.: TR11-088, June 2011].

We apply this result in algebraic proof complexity, focusing on proof systems for polynomial identities (PI proofs) which operate with algebraic circuits and whose axioms are the polynomial-ring axioms [P. Hrubeš and I. Tzameret, The proof complexity of polynomial identities, in Proc. 24th Annual IEEE Conf. Computational Complexity, CCC 2009, 15–18 July 2009, Paris, France (2009), pp. 41–51; Short proofs for the determinant identities, SIAM J. Comput.44(2) (2015) 340–383], and their subsystems. We identify a decrease in strength hierarchy of subsystems of PI proofs, in which the $d$th level is a sound and complete proof system for proving $d\times d$ matrix identities (over a given field). For each level $d>2$ in the hierarchy, we establish an $\mathrm{\Omega }(n^{2d})$ lower bound on the number of proof-steps needed to prove certain identities.

Finally, we present several concrete open problems about non-commutative algebraic circuits and speed-ups in proof complexity, whose solution would establish stronger size lower bounds on PI proofs of matrix identities, and beyond.

The complexity class of -polynomial local search (PLS) problems is introduced and is used to give new witnessing theorems for fragments of bounded arithmetic. For 1 ≤ i ≤ k + 1, the -definable functions of are characterized in terms of -PLS problems. These -PLS problems can be defined in a weak base theory such as , and proved to be total in . Furthermore, the -PLS definitions can be skolemized with simple polynomial time functions, and the witnessing theorem itself can be formalized, and skolemized, in a weak base theory. We introduce a new -principle that is conjectured to separate and .

Let g be a map defined as the Nisan–Wigderson generator but based on an NP ∩ coNP-function f. Any string b outside the range of g determines a propositional tautology τ(g)_b expressing this fact. Razborov [27] has conjectured that if f is hard on average for P/poly then these tautologies have no polynomial size proofs in the Extended Frege system EF.

We consider a more general Statement (S) that the tautologies have no polynomial size proofs in any propositional proof system. This is equivalent to the statement that the complement of the range of g contains no infinite NP set.

We prove that Statement (S) is consistent with Cook' s theory PV and, in fact, with the true universal theory T_PV in the language of PV. If PV in this consistency statement could be extended to "a bit" stronger theory (properly included in Buss's theory ) then Razborov's conjecture would follow, and if T_PV could be added too then Statement (S) would follow.

We discuss this problem in some detail, pointing out a certain form of reflection principle for propositional logic, and we introduce a related feasible disjunction property of proof systems.

The feasible interpolation theorem for semantic derivations from [J. Krajíček, Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. Symbolic Logic62(2) (1997) 457–486] allows to derive from some short semantic derivations (e.g. in resolution) of the disjointness of two $\mathrm{\text{NP}}$ sets $U$ and $V$ a small communication protocol (a general dag-like protocol in the sense of Krajíček (1997) computing the Karchmer–Wigderson multi-function $KW[U,V]$ associated with the sets, and such a protocol further yields a small circuit separating $U$ from $V$. When $U$ is closed upwards, the protocol computes the monotone Karchmer–Wigderson multi-function $K{W}^m[U,V]$ and the resulting circuit is monotone. Krajíček [Interpolation by a game, Math. Logic Quart.44(4) (1998) 450–458] extended the feasible interpolation theorem to a larger class of semantic derivations using the notion of a real communication complexity (e.g. to the cutting planes proof system CP). In this paper, we generalize the method to a still larger class of semantic derivations by allowing randomized protocols. We also introduce an extension of the monotone circuit model, monotone circuits with a local oracle (CLOs), that does correspond to communication protocols for $K{W}^m[U,V]$ making errors. The new randomized feasible interpolation thus shows that a short semantic derivation (from a certain class of derivations larger than in the original method) of the disjointness of $U,V$, $U$ closed upwards, yields a small randomized protocol for $K{W}^m[U,V]$ and hence a small monotone CLO separating the two sets. This research is motivated by the open problem to establish a lower bound for proof system $\mathrm{\text{R(LIN}}/{\mathrm{\text{F}}}_2)$ operating with clauses formed by linear Boolean functions over ${\mathrm{\text{F}}}_2$. The new randomized feasible interpolation applies to this proof system and also to (the semantic versions of) cutting planes CP, to small width resolution over CP of Krajíček [Discretely ordered modules as a first-order extension of the cutting planes proof system, J. Symbolic Logic63(4) (1998) 1582–1596] (system R(CP)) and to random resolution RR of Buss, Kolodziejczyk and Thapen [Fragments of approximate counting, J. Symbolic Logic79(2) (2014) 496–525]. The method does not yield yet lengths-of-proofs lower bounds; for this it is necessary to establish lower bounds for randomized protocols or for monotone CLOs.

Cirquent calculus and calculus of structures are two approaches to proof theory. Both of them apply deep inference which modifies objects at any level rather than only around the root as is the case in sequent calculus. In this paper we compare the proof complexity of the cirquent calculus system CL8S and the calculus of structures system SKSg at the classical propositional level, and show that CL8S polynomially simulates SKSg.