Search

We connect learning algorithms and algorithms automating proof search in propositional proof systems: for every sufficiently strong, well-behaved propositional proof system P, we prove that the following statements are equivalent, (1) Provable learning. P proves efficiently that p-size circuits are learnable by subexponential-size circuits over the uniform distribution with membership queries. (2) Provable automatability. P proves efficiently that P is automatable by non-uniform circuits on propositional formulas expressing p-size circuit lower bounds.Here, P is sufficiently strong and well-behaved if I.–III. hold: I. P p-simulates Jeřábek’s system WF (which strengthens the Extended Frege system EF by a surjective weak pigeonhole principle); II. P satisfies some basic properties of standard proof systems which p-simulate WF; III. P proves efficiently for some Boolean function h that h is hard on average for circuits of subexponential size. For example, if III. holds for P = WF, then Items 1 and 2 are equivalent for P = WF. We use the following modified notion of automatability in Item 2, the automating circuits output a P-proof of a given formula (expressing a p-size circuit lower bound for a function f) in non-uniform p-time in the length of a shortest P-proof of a closely related but different formula (expressing an average-case subexponential-size circuit lower bound for the same function f).If there is a function h ∈NE ∩coNE which is hard on average for circuits of size 2n/4, for each sufficiently big n, then there is an explicit propositional proof system P satisfying properties I.-III., i.e. the equivalence of Items 1 and 2 holds for P. [ABSTRACT FROM AUTHOR]

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]

Abstract: We show that the least number principle for (strict ) formulas can be characterized by the existence of alternating minima and maxima of length . We show simple prenex forms of these formulas whose herbrandizations (by polynomial time functions) are formulas that characterize theorems of the levels of the Bounded Arithmetic Hierarchy, and we derive from this another characterization, in terms of a search problem about finding pure Nash equilibria in -turn games. [Copyright &y& Elsevier]

Complexity in logic comes in many forms. In finite model theory, it is the complexity of describing properties, whereas in proof complexity it is the complexity of proving properties in a proof system. Here, we consider several notions of complexity in logic, the connections among them and their relationship with computational complexity. In particular, we show how the complexity of logics in the setting of finite model theory is used to obtain results in bounded arithmetic, stating which functions are provably total in certain weak systems of arithmetic. For example, the transitive closure function (testing reachability between two given points in a directed graph) is definable using only NL-concepts (where NL is the non-deterministic logspace complexity class) and its totality (and, thus, the closure of NL under complementation) is provable within NL-reasoning. Lastly, we will touch upon the topic of formalizing complexity theory using logic, and the meta-question of complexity of logical reasoning about complexity-theoretic statements. This is intended to be a high-level overview, suitable for readers who are not familiar with complexity theory and complexity in logic. [ABSTRACT FROM PUBLISHER]

The Jordan curve theorem (JCT) states that a simple closed curve divides the plane into exactly two connected regions. We formalize and prove the theorem in the context of grid graphs, under different input settings, in theories of bounded arithmetic that correspond to small complexity classes. The theory V0(2) (corresponding to AC0(2)) proves that any set of edges that form disjoint cycles divides the grid into at least two regions. The theory V0 (corresponding to AC0) proves that any sequence of edges that form a simple closed curve divides the grid into exactly two regions. As a consequence, the Hex tautologies and the stconnectivity tautologies have polynomial size AC0(2)-Frege-proofs, which improves results of Buss which only apply to the stronger proof system TC0-Frege. [ABSTRACT FROM AUTHOR]

Abstract: The theory , axiomatized by the induction scheme for sharply bounded formulae in Buss’ original language of bounded arithmetic (with but not ), has recently been unconditionally separated from full bounded arithmetic . The method used to prove the separation is reminiscent of those known from the study of open induction. We make the connection to open induction explicit, showing that models of can be built using a “nonstandard variant” of Wilkie’s well-known technique for building models of . This makes it possible to transfer many results and methods from open to sharply bounded induction with relative ease. We provide two applications: (i) the Shepherdson model of can be embedded into a model of , which immediately implies some independence results for ; (ii) extended by an axiom which roughly states that every number has a least 1 bit in its binary notation, while significantly stronger than plain , does not prove the infinity of primes. [Copyright &y& Elsevier]

We give a new characterization of the strict $$\forall {\Sigma^b_j}$$ sentences provable using $${\Sigma^b_k}$$ induction, for 1 ≤ j ≤ k. As a small application we show that, in a certain sense, Buss's witnessing theorem for strict $${\Sigma^b_k}$$ formulas already holds over the relatively weak theory PV. We exhibit a combinatorial principle with the property that a lower bound for it in constant-depth Frege would imply that the narrow CNFs with short depth j Frege refutations form a strict hierarchy with j, and hence that the relativized bounded arithmetic hierarchy can be separated by a family of $$\forall {\Sigma^b_1}$$ sentences. [ABSTRACT FROM AUTHOR]

Abstract: “Clarithmetic” is a generic name for formal number theories similar to Peano arithmetic, but based on computability logic instead of the more traditional classical or intuitionistic logics. Formulas of clarithmetical theories represent interactive computational problems, and their “truth” is understood as existence of an algorithmic solution. Imposing various complexity constraints on such solutions yields various versions of clarithmetic. The present paper introduces a system of clarithmetic for polynomial time computability, which is shown to be sound and complete. Sound in the sense that every theorem T of the system represents an interactive number-theoretic computational problem with a polynomial time solution and, furthermore, such a solution can be efficiently extracted from a proof of T. And complete in the sense that every interactive number-theoretic problem with a polynomial time solution is represented by some theorem T of the system. The paper is written in a semitutorial style and targets readers with no prior familiarity with computability logic. [Copyright &y& Elsevier]

Conservative subtheories of $${{R}^{1}_{2}}$$ and $${{S}^{1}_{2}}$$ are presented. For $${{S}^{1}_{2}}$$, a slight tightening of Jeřábek's result (Math Logic Q 52(6):613-624, ) that $${T^{0}_{2} \preceq_{\forall \Sigma^{b}_{1}}S^{1}_{2}}$$ is presented: It is shown that $${T^{0}_{2}}$$ can be axiomatised as BASIC together with induction on sharply bounded formulas of one alternation. Within this $${\forall\Sigma^{b}_{1}}$$-theory, we define a $${\forall\Sigma^{b}_{0}}$$-theory, $${T^{-1}_{2}}$$, for the $${\forall\Sigma^{b}_{0}}$$-consequences of $${S^{1}_{2}}$$. We show $${T^{-1}_{2}}$$ is weak by showing it cannot $${\Sigma^{b}_{0}}$$-define division by 3. We then consider what would be the analogous $${\forall\hat\Sigma^{b}_{1}}$$-conservative subtheory of $${R^{1}_{2}}$$ based on Pollett (Ann Pure Appl Logic 100:189-245, . It is shown that this theory, $${{T}^{0,\left\{2^{(||\dot{id}||)}\right\}}_{2}}$$, also cannot $${\Sigma^{b}_{0}}$$-define division by 3. On the other hand, we show that $${{S}^{0}_{2}+open_{\{||id||\}}}$$- COMP is a $${\forall\hat\Sigma^{b}_{1}}$$-conservative subtheory of $${R^{1}_{2}}$$. Finally, we give a refinement of Johannsen and Pollett (Logic Colloquium' 98, 262-279, ) and show that $${\hat{C}^{0}_{2}}$$ is $${\forall\hat\Sigma^{b}_{1}}$$-conservative over a theory based on open-comprehension. [ABSTRACT FROM AUTHOR]

In this note we will introduce a class of search problems, called nested Polynomial Local Search (nPLS) problems, and show that definable NP search problems, i.e., $${\Sigma^{b}_{1}}$$-definable functions in $${T^{2}_{2}}$$ are characterized in terms of the nested PLS. [ABSTRACT FROM AUTHOR]

Abstract: We define a new NP search problem, the “local improvement” principle, about labellings of an acyclic, bounded-degree graph. We show that, provably in , it characterizes the consequences of and that natural restrictions of it characterize the consequences of and of the bounded arithmetic hierarchy. We also show that over it characterizes the consequences of and hence that, in some sense, a miniaturized version of the principle gives a new characterization of the consequences of . Throughout our search problems are “type-2” NP search problems, which take second-order objects as parameters. [Copyright &y& Elsevier]

Abstract: We develop an arithmetical theory and its variant , corresponding to “slightly nonuniform” . Our theories sit between and , and allow evaluation of log-depth bounded fan-in circuits under limited conditions. Propositional translations of -formulas provable in admit -uniform polynomial-size Frege proofs. [Copyright &y& Elsevier]

Abstract: We formalize the construction of Paterson’s variant of the Ajtai–Komlós–Szemerédi sorting network of logarithmic depth in the bounded arithmetical theory (an extension of ), under the assumption of the existence of suitable expander graphs. We derive a conditional p-simulation of the propositional sequent calculus in the monotone sequent calculus . [Copyright &y& Elsevier]

Cook and Krajíček have recently obtained the following Karp-Lipton collapse result in bounded arithmetic: if the theory PV proves NP ⊆ P/poly, then the polynomial hierarchy collapses to the Boolean hierarchy, and this collapse is provable in PV. Here we show the converse implication, thus answering an open question posed by Cook and Krajíček. We obtain this result by formalizing in PV a hard/easy argument of Buhrman et al. [2003]. In addition, we continue the investigation of propositional proof systems using advice, initiated by Cook and Krajíček. In particular, we obtain several optimality results for proof systems using advice. We further show that these optimal systems are equivalent to natural extensions of Frege systems. [ABSTRACT FROM AUTHOR]

We investigate the provability of some properties of abelian groups and quadratic residues in variants of bounded arithmetic. Specifically, we show that the structure theorem for finite abelian groups is provable in S22 + iWPHP(Σ1b), and use it to derive Fermat's little theorem and Euler's criterion for the Legendre symbol in S22 + iWPHP(PV) extended by the pigeonhole principle PHP(PV). We prove the quadratic reciprocity theorem (including the supplementary laws) in the arithmetic theories T20 + Count2(PV) and I Δ0 + Count2(Δ0) with modulo-2 counting principles (© 2010 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

We show that for each n ≥ 1, if T2n does not prove the weak pigeonhole principle for Σbn functions, then the collection scheme B Σ1 is not finitely axiomatizable over T2n. The same result holds with Sn2 in place of T 2n (© 2010 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

Abstract: Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations. Explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way. [Copyright &y& Elsevier]

Abstract: We show that the arithmetical theory -, formalized in the language of Buss, i.e. with but without the function , does not prove that every nontrivial divisor of a power of is even. It follows that this theory proves neither nor . [Copyright &y& Elsevier]

We show that the bounded arithmetic theory V0 does not prove that the polynomial time hierarchy collapses to the linear time hierarchy (without parameters). The result follows from a lower bound for bounded depth circuits computing prefix parity, where the circuits are allowed some auxiliary input; we derive this from a theorem of Ajtai (© 2009 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]

We show that the bounded arithmetic theory V0 does not prove that the polynomial time hierarchy collapses to the linear time hierarchy (without parameters). The result follows from a lower bound for bounded depth circuits computing prefix parity, where the circuits are allowed some auxiliary input; we derive this from a theorem of Ajtai (© 2009 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) [ABSTRACT FROM AUTHOR]