Search

One of the elegant achievements in the history of proof theory is the characterization of the provably total recursive functions of an arithmetical theory by its proof-theoretic ordinal as a way to measure the time complexity of the functions. Unfortunately, the machinery is not sufficiently fine-grained to be applicable on the weak theories, on the one hand and to capture the bounded functions with bounded definitions of strong theories, on the other. In this paper, we develop such a machinery to address the bounded theorems of both strong and weak theories of arithmetic. In the first part, we provide a refined version of ordinal analysis to capture the feasibly definable and bounded functions that are provably total in $\textrm{PA}+\bigcup _{\beta \prec \alpha } \textrm{TI}({\prec_{\beta}})$ , the extension of Peano arithmetic by transfinite induction up to the ordinals below $\alpha$. Roughly speaking, we identify the functions as the ones that are computable by a sequence of $\textrm{PV}$ -provable polynomial time modifications on an initial polynomial time value, where the computational steps are indexed by the ordinals below $\alpha$ , decreasing by the modifications. In the second part, and choosing $l \leq k$ , we use similar technique to capture the functions with bounded definitions in the theory $T^k_2$ (resp. $S^k_2$) as the functions computable by exponentially (resp. polynomially) long sequence of $\textrm{PV}_{k-l +1}$ -provable reductions between $l$ -turn games starting with an explicit $\textrm{PV}_{k-l +1}$ -provable winning strategy for the first game. [ABSTRACT FROM AUTHOR]

We prove the first unconditional consistency result for superpolynomial circuit lower bounds with a relatively strong theory of bounded arithmetic. Namely, we show that the theory V20 is consistent with the conjecture that NEXP⊈P/poly, i.e. some problem that is solvable in non-deterministic exponential time does not have polynomial size circuits. We suggest this is the best currently available evidence for the truth of the conjecture. The same techniques establish the same results with NEXP replaced by the class of problems decidable in non-deterministic barely superpolynomial time such as NTIME(nO(logloglog n)). Additionally, we establish a magnification result on the hardness of proving circuit lower bounds. [ABSTRACT FROM AUTHOR]

Cook and Reckhow [5] pointed out that $\mathcal {N}\mathcal {P} \neq co\mathcal {N}\mathcal {P}$ iff there is no propositional proof system that admits polynomial size proofs of all tautologies. The theory of proof complexity generators aims at constructing sets of tautologies hard for strong and possibly for all proof systems. We focus on a conjecture from [16] in foundations of the theory that there is a proof complexity generator hard for all proof systems. This can be equivalently formulated (for p-time generators) without a reference to proof complexity notions as follows: • There exists a p-time function g stretching each input by one bit such that its range $rng(g)$ intersects all infinite $\mathcal {N}\mathcal {P}$ sets. We consider several facets of this conjecture, including its links to bounded arithmetic (witnessing and independence results), to time-bounded Kolmogorov complexity, to feasible disjunction property of propositional proof systems and to complexity of proof search. We argue that a specific gadget generator from [18] is a good candidate for g. We define a new hardness property of generators, the $\bigvee $ -hardness, and show that one specific gadget generator is the $\bigvee $ -hardest (w.r.t. any sufficiently strong proof system). We define the class of feasibly infinite $\mathcal {N}\mathcal {P}$ sets and show, assuming a hypothesis from circuit complexity, that the conjecture holds for all feasibly infinite $\mathcal {N}\mathcal {P}$ sets. [ABSTRACT FROM AUTHOR]

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 overGF (2) in Hrubeš-Tzameret [15]. Specifically, we show that the multiplicativity of the determinant function and the Cayley-Hamilton theorem over the integers are provable in the bounded arithmetic theory VNC²; the latter is a first-order theory corresponding to the complexity class NC² consisting of problems solvable by uniform families of polynomial-size circuits and O(log² n)-depth. This also establishes the existence of uniform polynomial-size propositional proofs operating with NC²-circuits of the basic determinant identities over the integers (previous propositional proofs hold only over the two-element field). [ABSTRACT FROM AUTHOR]

Semi-algebraic proof systems such as sum-of-squares (SoS) have attracted a lot of attention due to their relation to approximation algorithms: constant degree semi-algebraic proofs lead to conjecturally optimal polynomial-time approximation algorithms for important NP -hard optimization problems. Motivated by the need to allow a more streamlined and uniform framework for working with SoS proofs than the restrictive propositional level, we initiate a systematic first-order logical investigation into the kinds of reasoning possible in algebraic and semi-algebraic proof systems. Specifically, we develop first-order theories that capture in a precise manner constant degree algebraic and semi-algebraic proof systems: every statement of a certain form that is provable in our theories translates into a family of constant degree polynomial calculus or SoS refutations, respectively; and using a reflection principle, the converse also holds. This places algebraic and semi-algebraic proof systems in the established framework of bounded arithmetic, while providing theories corresponding to systems that vary quite substantially from the usual propositional-logic ones. We give examples of how our semi-algebraic theory proves statements such as the pigeonhole principle, we provide a separation between algebraic and semi-algebraic theories, and we describe initial attempts to go beyond these theories by introducing extensions that use the inequality symbol, identifying along the way which extensions lead outside the scope of constant degree SoS. Moreover, we prove new results for propositional proofs, and specifically extend Berkholz's dynamic-by-static simulation of polynomial calculus (PC) by SoS to PC with the radical rule. [ABSTRACT FROM AUTHOR]

In this paper, we study bounded versions of some model-theoretic notions and results. We apply these results to the context of models of bounded arithmetic theories as well as some related complexity questions. As an example, we show that if the theory \(\rm S_2 ^1(PV)\) has bounded model companion then \(\rm NP=coNP\). We also study bounded versions of some other related notions such as Stone topology.

We study a new class of NP search problems, those which can be proved total using standard combinatorial reasoning based on approximate counting. Our model for this kind of reasoning is the bounded arithmetic theory APC 2 of [E. Jeřábek, Approximate counting by hashing in bounded arithmetic, J. Symb. Log.  74(3) (2009) 829–860]. In particular, the Ramsey and weak pigeonhole search problems lie in the new class. We give a purely computational characterization of this class and show that, relative to an oracle, it does not contain the problem CPLS, a strengthening of PLS. As CPLS is provably total in the theory T 2 2 , this shows that APC 2 does not prove every ∀ Σ 1 b sentence which is provable in bounded arithmetic. This answers the question posed in [S. Buss, L. A. Kołodziejczyk and N. Thapen, Fragments of approximate counting, J. Symb. Log.  79(2) (2014) 496–525] and represents some progress in the program of separating the levels of the bounded arithmetic hierarchy by low-complexity sentences. Our main technical tool is an extension of the "fixing lemma" from [P. Pudlák and N. Thapen, Random resolution refutations, Comput. Complexity, 28(2) (2019) 185–239], a form of switching lemma, which we use to show that a random partial oracle from a certain distribution will, with high probability, determine an entire computation of a P NP oracle machine. The introduction to the paper is intended to make the statements and context of the results accessible to someone unfamiliar with NP search problems or with bounded arithmetic. [ABSTRACT FROM AUTHOR]

We show that V T C 0 , the basic theory of bounded arithmetic corresponding to the complexity class TC 0 , proves the IMUL axiom expressing the totality of iterated multiplication satisfying its recursive definition, by formalizing a suitable version of the TC 0 iterated multiplication algorithm by Hesse, Allender, and Barrington. As a consequence, V T C 0 can also prove the integer division axiom, and (by our previous results) the RSUV -translation of induction and minimization for sharply bounded formulas. Similar consequences hold for the related theories Δ 1 b - C R and C 2 0 . As a side result, we also prove that there is a well-behaved Δ 0 definition of modular powering in I Δ 0 + W P H P (Δ 0) . [ABSTRACT FROM AUTHOR]

In this paper, we study bounded versions of some model-theoretic notions and results. We apply these results to models of bounded arithmetic theories as well as some related complexity questions. As an example, we show that if the theory S2¹(PV) has bounded model companion then NP = coNP. We also study bounded versions of some other related notions such as Stone topology. [ABSTRACT FROM AUTHOR]

We will give a two-sort system which axiomatizes winning strategies for the combinatorial game Node Kayles. It is shown that our system captures alternating polynomial time reasonings in the sense that the provably total functions of the theory corresponds to those computable in APTIME. We will also show that our system is equivalently axiomatized by Sprague–Grundy theorem which states that any Node Kayles position is provably equivalent to some NIM heap. [ABSTRACT FROM AUTHOR]

We study variants of Buss's theories of bounded arithmetic axiomatized by induction schemes disallowing the use of parameters, and closely related induction inference rules. We put particular emphasis on Π ^ i b induction schemes, which were so far neglected in the literature. We present inclusions and conservation results between the systems (including a witnessing theorem for T 2 i and S 2 i of a new form), results on numbers of instances of the axioms or rules, connections to reflection principles for quantified propositional calculi, and separations between the systems. [ABSTRACT FROM AUTHOR]

A polynomial time ultrapower is a structure given by the set of polynomial time computable functions modulo some ultrafilter. They model the universal theory ∀ PV of all polynomial time functions. Generalizing a theorem of Hirschfeld (Israel J Math 20(2):111–126, 1975), we show that every countable model of ∀ PV is isomorphic to an existentially closed substructure of a polynomial time ultrapower. Moreover, one can take a substructure of a special form, namely a limit polynomial time ultrapower in the classical sense of Keisler (in: Bergelson, V., Blass, A., Di Nasso, M., Jin, R. (eds.) Ultrafilters across mathematics, contemporary mathematics vol 530, pp 163–179. AMS, New York, 1963). Using a polynomial time ultrapower over a nonstandard Herbrand saturated model of ∀ PV we show that ∀ PV is consistent with a formal statement of a polynomial size circuit lower bound for a polynomial time computable function. This improves upon a recent result of Krajíček and Oliveira (Logical methods in computer science 13 (1:4), 2017). [ABSTRACT FROM AUTHOR]

This article presents a proof that Buss's $S_2^2$ can prove the consistency of a fragment of Cook and Urquhart's PV from which induction has been removed but substitution has been retained. This result improves Beckmann's result, which proves the consistency of such a system without substitution in bounded arithmetic $S_2^1$. Our proof relies on the notion of "computation" of the terms of PV. In our work, we first prove that, in the system under consideration, if an equation is proved and either its left- or right-hand side is computed, then there is a corresponding computation for its right- or left-hand side, respectively. By carefully computing the bound of the size of the computation, the proof of this theorem inside a bounded arithmetic is obtained, from which the consistency of the system is readily proven. This result apparently implies the separation of bounded arithmetic because Buss and Ignjatović stated that it is not possible to prove the consistency of a fragment of PV without induction but with substitution in Buss's $S_2^1$. However, their proof actually shows that it is not possible to prove the consistency of the system, which is obtained by the addition of propositional logic and other axioms to a system such as ours. On the other hand, the system that we have considered is strictly equational, which is a property on which our proof relies. [ABSTRACT FROM AUTHOR]

This article bears on four topics: observational predicates and phenomenal properties, vagueness, strict finitism as a philosophy of mathematics, and the analysis of feasible computability. It is argued that reactions to strict finitism point towards a semantics for vague predicates in the form of nonstandard models of weak arithmetical theories of the sort originally introduced to characterize the notion of feasibility as understood in computational complexity theory. The approach described eschews the use of nonclassical logic and related devices like degrees of truth or supervaluation. Like epistemic approaches to vagueness, it may thus be smoothly integrated with the use of classical model theory as widely employed in natural language semantics. But unlike epistemicism, the described approach fails to imply either the existence of sharp boundaries or the failure of tolerance for soritical predicates. Applications of measurement theory (in the sense of Krantz, Luce, Suppes, & Tversky (1971)) to vagueness in the nonstandard setting are also explored. [ABSTRACT FROM AUTHOR]

It is known that rational approximations of elementary analytic functions (exp, log, trigonometric, and hyperbolic functions, and their inverse functions) are computable in the weak complexity class TC 0. We show how to formalize the construction and basic properties of these functions in the corresponding theory of bounded arithmetic, VT C 0. [ABSTRACT FROM AUTHOR]

Clarithmetics are number theories based on computability logic. Formulas of these theories represent interactive computational problems, and their "truth" is under- stood as existence of an algorithmic solution. Various complexity constraints on such solutions induce various versions of clarithmetic. The present paper introduces a param- eterized/schematic version CLA11P1,P2,P3 P4. By tuning the three parameters P1, P2, P3 in an essentially mechanical manner, one automatically obtains sound and complete theories with respect to a wide range of target tricomplexity classes, i.e., combinations of time (set by P3), space (set by P2) and so called amplitude (set by P1) complexities. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a solution from the given tricomplexity class and, further- more, such a solution can be automatically extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a solution from the given tricomplexity class is represented by some theorem of the system. Furthermore, through tuning the 4th parameter P4, at the cost of sacrificing recursive axiomatizability but not simplicity or elegance, the above extensional completeness can be strengthened to intensional completeness, according to which every formula representing a problem with a solution from the given tricomplexity class is a theorem of the system. This article is published in two parts. The previous Part I has introduced the system and proved its completeness, while the present Part II is devoted to proving soundness. [ABSTRACT FROM AUTHOR]

We present two constructions of models of bounded arithmetic, both in the form of a generalization of the ultrapower construction, that yield nonelementary extensions but do not introduce new lengths. As an application we show, assuming the existence of a one-way permutation g hard against polynomial-size circuits, that $$\textit{strict}R^1_2(g)$$ is weaker than $$R^1_2(g)$$ . In particular, if such a permutation can be defined by a term in the language of $$R^1_2$$ , then $$\textit{strict}R^1_2$$ is weaker than $$R^1_2$$ . [ABSTRACT FROM AUTHOR]

The earlier paper “Introduction to clarithmetic I” constructed an axiomatic system of arithmetic based on computability logic, and proved its soundness and extensional completeness with respect to polynomial time computability. The present paper elaborates three additional sound and complete systems in the same style and sense: one for polynomial space computability, one for elementary recursive time (and/or space) computability, and one for primitive recursive time (and/or space) computability. [ABSTRACT FROM AUTHOR]

Buresh-Oppenheim proved that the NP search problem to find nontrivial factors of integers of a special form belongs to Papadimitriou's class PPA, and is probabilistically reducible to a problem in PPP. In this paper, we use ideas from bounded arithmetic to extend these results to arbitrary integers. We show that general integer factoring is reducible in randomized polynomial time to a PPA problem and to the problem WeakPigeon ∈ PPP . Both reductions can be derandomized under the assumption of the generalized Riemann hypothesis. We also show (unconditionally) that PPA contains some related problems, such as square root computation modulo n , and finding quadratic nonresidues modulo n . [ABSTRACT FROM AUTHOR]

The relativized weak pigeonhole principle states that if at least 2n out of n2 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^{\left( {{\rm{log\ }}n} \right)^{3/2 - \varepsilon } } $ for every ε﹥0 and every sufficiently large n. By reducing it to the standard weak pigeonhole principle with 2n pigeons and n holes, we also show that this lower bound is essentially tight in that there exist DNF-refutations of size $2^{\left( {{\rm{log\ }}n} \right)^{O\left( 1 \right)} } $ even in R(log). For the lower bound proof we need to discuss the existence of unbalanced low-degree bipartite expanders satisfying a certain robustness condition. [ABSTRACT FROM PUBLISHER]

We present several known formalizations of theorems from computational complexity in bounded arithmetic and formalize the PCP theorem in the theory PV1 (no formalization of this theorem was known). This includes a formalization of the existence and of some properties of the (n, d, λ)-graphs in PV1. [ABSTRACT FROM AUTHOR]

The elementary arithmetic operations $${+,\cdot,\le}$$ on integers are well-known to be computable in the weak complexity class TC, and it is a basic question what properties of these operations can be proved using only TC-computable objects, i.e., in a theory of bounded arithmetic corresponding to TC. We will show that the theory VTC extended with an axiom postulating the totality of iterated multiplication (which is computable in TC) proves induction for quantifier-free formulas in the language $${\langle{+,\cdot,\le}\rangle}$$ ( IOpen), and more generally, minimization for $${\Sigma_{0}^{b}}$$ formulas in the language of Buss's S. [ABSTRACT FROM AUTHOR]

We describe a method of forcing against weak theories of arithmetic and its applications in propositional proof complexity. [ABSTRACT FROM AUTHOR]

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 4 k c where k ≥ 1 , c ≥ 2 unless each function f ∈ SIZE ( n k ) can be approximated by formulas { F n } n = 1 ∞ of subexponential size 2 O ( n 1 / c ) with subexponential advantage: P x ∈ { 0 , 1 } n [ F n ( x ) = f ( x ) ] ≥ 1 / 2 + 1 / 2 O ( n 1 / c ) . Unconditionally, V 0 cannot prove that for sufficiently large n , SAT does not have circuits of size n log ⁡ n . The proof is based on an interpretation of Krajíček's proof (Krajíček, 2011 [15] ) that certain NW-generators are hard for T PV , the true universal theory in the language containing names for all p-time algorithms. [ABSTRACT FROM AUTHOR]

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 T2¹. This answers an open question raised in Buss et al. [2012] and completes their program to compare the strength of Jeřábek's bounded arithmetic theory for approximate counting with weakened versions of it. [ABSTRACT FROM AUTHOR]

We study the long-standing open problem of giving ∀Σ1b separations for fragments of bounded arithmetic in the relativized setting. Rather than considering the usual fragments defined by the amount of induction they allow, we study Jerábek's theories for approximate counting and their subtheories. We show that the ∀Σ1b Herbrandized ordering principle is unprovable in a fragment of bounded arithmetic that includes the injective weak pigeonhole principle for polynomial time functions, and also in a fragment that includes the surjective weak pigeonhole principle for FPNP functions. We further give new propositional translations, in terms of random resolution refutations, for the consequences of T2¹ augmented with the surjective weak pigeonhole principle for polynomial time functions. [ABSTRACT FROM AUTHOR]

A propositional proof system is weakly automatizable if there is a polynomial time algorithm that separates satisfiable formulas from formulas that have a short refutation in the system, with respect to a given length bound. We show that if the resolution proof system is weakly automatizable, then parity games can be decided in polynomial time. We give simple proofs that the same holds for depth-1 propositional calculus (where resolution has depth 0) with respect to mean payoff and simple stochastic games. We define a new type of combinatorial game and prove that resolution is weakly automatizable if and only if one can separate, by a set decidable in polynomial time, the games in which the first player has a positional winning strategy from the games in which the second player has a positional winning strategy. Our main technique is to show that a suitable weak bounded arithmetic theory proves that both players in a game cannot simultaneously have a winning strategy, and then to translate this proof into propositional form. [ABSTRACT FROM AUTHOR]

This article concerns the second-order systems U1/2 and V1/2 of bounded arithmetic, which have proof-theoretic strengths corresponding to polynomial-space and exponential-time computation. We formulate improved witnessing theorems for these two theories by using S1/2 as a base theory for proving the correctness of the polynomial-space or exponential-time witnessing functions. We develop the theory of nondeterministic polynomial-space computation, including Savitch's theorem, in U1/2 . Kołodziejczyk et al. [2011] have introduced local improvement properties to characterize the provably total NP functions of these second-order theories. We show that the strengths of their local improvement principles over U1/2 and V1/2 depend primarily on the topology of the underlying graph, not the number of rounds in the local improvement games. The theory U1/2 proves the local improvement principle for linear graphs even without restricting to logarithmically many rounds. The local improvement principle for grid graphs with only logarithmically-many rounds is complete for the provably total NP search problems of V1/2. Related results are obtained for local improvement principles with one improvement round and for local improvement over rectangular grids. [ABSTRACT FROM AUTHOR]

We formalize the notion of Herbrand Consistency in an appropriate way for bounded arithmetics, and show the existence of a finite fragment of IΔ whose Herbrand Consistency is not provable in IΔ. We also show the existence of an IΔ-derivable Π-sentence such that IΔ cannot prove its Herbrand Consistency. [ABSTRACT FROM AUTHOR]

D'Aquino et al. (J Symb Log 75(1):1-11, ) have recently shown that every real-closed field with an integer part satisfying the arithmetic theory IΣ is recursively saturated, and that this theorem fails if IΣ is replaced by IΔ. We prove that the theorem holds if IΣ is replaced by weak subtheories of Buss' bounded arithmetic: PV or $${\Sigma^b_1-IND^{|x|_k}}$$. It also holds for IΔ (and even its subtheory IE) under a rather mild assumption on cofinality. On the other hand, it fails for the extension of IOpen by an axiom expressing the Bézout property, even under the same assumption on cofinality. [ABSTRACT FROM AUTHOR]