We show that every model of IΔ0 has an end extension to a model of a theory where log-space computable function are formalizable. We also show the existence of an isomorphism between models of IΔ0 and models of linear arithmetic LA.

We prove that PTCN cannot be a model of U12. This implies that there exists a first order sentence of bounded arithmetic which is provable in U12 but does not hold in PTCN.

In his paper "Undecidability without arithmetization," Andrzej Grzegorczyk introduces a theory of concatenation $\mathsf{TC}$. We show that pairing is not definable in $\mathsf{TC}$. We determine a reasonable extension of $\mathsf{TC}$ that is sequential, that is, has a good sequence coding.

In this paper we study proofs of some general forms of the Second Incompleteness Theorem. These forms conform to the Feferman format, where the proof predicate is fixed and the representation of the set of axioms varies. We extend the Feferman framework in one important point: we allow the interpretation of number theory to vary.

We investigate the theories of linear algebra, which were originally defined to study the question of whether commutativity of matrix inverses has polysize Frege proofs. We give sentences separating quantified versions of these theories, and define a fragment in which we can interpret a weak theory V 1 of bounded arithmetic and carry out polynomial time reasoning about matrices - for example, we can formalize the Gaussian elimination algorithm. We show that, even if we restrict our language, proves the commutativity (...) of inverses. (shrink)

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. (shrink)

We bring together some facts about the weak pigeonhole principle from bounded arithmetic, complexity theory, cryptography and abstract model theory. We characterize the models of arithmetic in which WPHP fails as those which are determined by an initial segment and prove a conditional separation result in bounded arithmetic, that PV + lies strictly between PV and S21 in strength, assuming that the cryptosystem RSA is secure.

By obtaining several new results on Cook-style two-sorted bounded arithmetic, this paper measures the strengths of the axiom of extensionality and of other weak fundamental set-theoretic axioms in the absence of the axiom of infinity, following the author’s previous work [K. Sato, The strength of extensionality I — weak weak set theories with infinity, Annals of Pure and Applied Logic 157 234–268] which measures them in the presence. These investigations provide a uniform framework in which three different kinds of reverse (...) mathematics–Friedman–Simpson’s “orthodox” reverse mathematics, Cook’s bounded reverse mathematics and large cardinal theory–can be reformulated within one language so that we can compare them more directly. (shrink)

A number of theories have been developed to characterize ALogTime (or uniform NC 1, or just NC 1), the class of languages accepted by alternating logtime Turing machines, in the same way that Buss’s theory ${{\bf S}^{1}_{2}}$ characterizes polytime functions. Among these, ALV′ (by Clote) is particularly interesting because it is developed based on Barrington’s theorem that the word problem for the permutation group S 5 is complete for ALogTime. On the other hand, ALV (by Clote), T 0 NC 0 (...) (by Clote and Takeuti) as well as Arai’s theory ${{\bf AID}+\Sigma_0^B{-}{\bf CA}}$ and its two-sorted version VNC 1 (by Cook and Morioka) are based on the circuit characterization of ALogTime. While the last three theories have been known to be equivalent, their relationship to ALV′ has been an open problem. Here we show that ALV′ is indeed equivalent to the other theories. (shrink)

We define a theory of two-sort bounded arithmetic whose provably total functions are exactly those in ${\mathcal{F}_{LOGCFL}}$ by way of a generalized quantifier that expresses computations of SAC 1 circuits. The proof depends on Kolokolova’s conditions for the connection between the provable capture in two-sort theories and descriptive complexity.

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 V0 it characterizes the consequences of V1 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. (shrink)

We show that the bounded arithmetic theory V0 does not prove that the polynomial time hierarchy collapses to the linear time hierarchy . 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.

In this paper we will state and prove some comparative theorems concerning PRA and IΣ1. We shall provide a characterization of IΣ1 in terms of PRA and iterations of a class of functions. In particular, we prove that for this class of functions the difference between IΣ1 and PRA is exactly that, where PRA is closed under iterations of these functions, IΣ1 is moreover provably closed under iteration. We will formulate a sufficient condition for a model of PRA to be (...) a model of IΣ1. This condition is used to give a model-theoretic proof of Parsons’ theorem, that is, IΣ1 is Π2-conservative over PRA. We shall also give a purely syntactical proof of Parsons’ theorem. Finally, we show that IΣ1 proves the consistency of PRA on a definable IΣ1-cut. This implies that proofs in IΣ1 can have non-elementary speed up over proofs in PRA. (shrink)

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 L-uniform polynomial-size Frege proofs.

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 \ induction schemes, which were so far neglected in the literature. We present inclusions and conservation results between the systems and \ 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.

We prove that (additive) ordered group reducts of nonstandard models of the bounded arithmetical theory are recursively saturated in a rich language with predicates expressing the integers, rationals, and logarithmically bounded numbers. Combined with our previous results on the construction of the real exponential function on completions of models of, we show that every countable model of is an exponential integer part of a real‐closed exponential field.

The elementary arithmetic operations +,·,≤\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${+,\cdot,\le}$$\end{document} on integers are well-known to be computable in the weak complexity class TC0, and it is a basic question what properties of these operations can be proved using only TC0-computable objects, i.e., in a theory of bounded arithmetic corresponding to TC0. We will show that the theory VTC0 extended with an axiom postulating the totality of iterated multiplication proves induction for quantifier-free formulas in the language ⟨+,·,≤⟩\documentclass[12pt]{minimal} (...) \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\langle{+,\cdot,\le}\rangle}$$\end{document}, and more generally, minimization for Σ0b\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\Sigma_{0}^{b}}$$\end{document} formulas in the language of Buss’s S2. (shrink)

Edward Nelson published in 1986 a book defending an extreme formalist view of mathematics according to which there is animpassable barrierin the totality of exponentiation. On the positive side, Nelson embarks on a program of investigating how much mathematics can be interpreted in Raphael Robinson's theory of arithmetic. In the shadow of this program, some very nice logical investigations and results were produced by a number of people, not only regarding what can be interpreted inbut also what cannot be so (...) interpreted. We explain some of these results and rely on them to discuss Nelson's position. (shrink)

Let Iπ2 denote the fragment of Peano Arithmetic obtained by restricting the induction scheme to parameter free Π2Π2 formulas. Answering a question of R. Kaye, L. Beklemishev showed that the provably total computable functions of Iπ2 are, precisely, the primitive recursive ones. In this work we give a new proof of this fact through an analysis of certain local variants of induction principles closely related to Iπ2. In this way, we obtain a more direct answer to Kaye's question, avoiding the (...) metamathematical machinery needed for Beklemishev's original proof.Our methods are model-theoretic and allow for a general study of Iπn+1 for all n≥0n≥0. In particular, we derive a new conservation result for these theories, namely that Iπn+1 is πn+2 -conservative over IΣn for each n≥1n≥1. (shrink)

Let H be a proof system for quantified propositional calculus (QPC). We define the Σqj-witnessing problem for H to be: given a prenex Σqj-formula A, an H-proof of A, and a truth assignment to the free variables in A, find a witness for the outermost existential quantifiers in A. We point out that the Σq1-witnessing problems for the systems G*1and G1 are complete for polynomial time and PLS (polynomial local search), respectively. We introduce and study the systems G*0 and G0, (...) in which cuts are restricted to quantifier-free formulas, and prove that the Σqj-witnessing problem for each is complete for NC1. Our proof involves proving a polynomial time version of Gentzen’s midsequent theorem for G*0 and proving that G0-proofs are TC0-recognizable. We also introduce QPC systems for TC0 and prove witnessing theorems for them. We introduce a finitely axiomatizable second-order system VNC1 of bounded arithmetic which we prove isomorphic to Arai’s first order theory AID + Σb0-CA for uniform NC1. We describe simple translations of VNC1 proofs of all bounded theorems to polynomial size families of G*0 proofs. From this and the above theorem we get alternative proofs of the NC1 witnessing theorems for VNC1 and AID. (shrink)

We introduce a second-order system V1-Horn of bounded arithmetic formalizing polynomial-time reasoning, based on Grädel's 35) second-order Horn characterization of P. Our system has comprehension over P predicates , and only finitely many function symbols. Other systems of polynomial-time reasoning either allow induction on NP predicates , and hence are more powerful than our system , or use Cobham's theorem to introduce function symbols for all polynomial-time functions . We prove that our system is equivalent to QPV and Zambella's P-def. (...) Using our techniques, we also show that V1-Horn is finitely axiomatizable, and, as a corollary, that the class of Σ1b consequences of S21 is finitely axiomatizable as well, thus answering an open question. (shrink)

Using nonstandard methods we construct a model of an induction scheme called inside a "resource" of the form is a Turing machine of code is calculated in less than , where means the length of the binary expansion of and are nonstandard parameters in a model of . As a consequence we obtain a model theoretic proof of a witnessing theorem for this theory by functions computable in time , a result first obtained by Buss, Krajícek, and Takeuti using proof (...) theory. (shrink)

A polynomial time ultrapower is a structure given by the set of polynomial time computable functions modulo some ultrafilter. They model the universal theory \ of all polynomial time functions. Generalizing a theorem of Hirschfeld :111–126, 1975), we show that every countable model of \ 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 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 \ we show that \ 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, 2017). (shrink)

The bounded arithmetic theory S2 is finitely axiomatized if and only if the polynomial hierarchy provably collapses. If T2i equals S2i + 1 then T2i is equal to S2 and proves that the polynomial time hierarchy collapses to ∑i + 3p, and, in fact, to the Boolean hierarchy over ∑i + 2p and to ∑i + 1p/poly.

This paper defines natural hierarchies of function and relation classes □i,kc and Δi,kc, constructed from parallel complexity classes in a manner analogous to the polynomial-time hierarchy. It is easily shown that □i−1,kp □c,kc □i,kp and similarly for the Δ classes. The class □i,3c coincides with the single-valued functions in Buss et al.'s class , and analogously for other growth rates. Furthermore, the class □i,kc comprises exactly the functions Σi,kb-definable in Ski−1, and if Tki−1 is Σi,kb-conservative over Ski−1, then □i,kp is (...) completely parallelizable. All functions in □i,kc are Σi,kb-definable in Rki; this suffices to show that if the known Σi,kb conservativity between R3i and S3i−1 extends to R2i and S2i−1, then NC = NC1 relative to an oracle in PH. We prove a KPT-style witnessing theorem for Ski using constantly many rounds of □i,kc interactive computation, and thus show that if Ski ≡ Rki+1 then the bounded arithmetic hierarchy collapses, provably in Ski. (shrink)

The purpose of this paper is to survey the correspondence between bounded arithmetic and propositional proof systems. In addition, it also contains some new results which have appeared as an extended abstract in the proceedings of the conference TAMC 2008 [11].Bounded arithmetic is closely related to propositional proof systems; this relation has found many fruitful applications. The aim of this paper is to explain and develop the general correspondence between propositional proof systems and arithmetic theories, as introduced by Krajíček and (...) Pudlák [46]. Instead of focusing on the relation between particular proof systems and theories, we favour a general axiomatic approach to this correspondence. In the course of the development we particularly highlight the role played by logical closure properties of propositional proof systems, thereby obtaining a characterization of extensions of EF in terms of a simple combination of these closure properties (© 2009 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim). (shrink)

We define and study a new restricted consistency notion RCon ∗ for bounded arithmetic theories T 2 j . It is the strongest ∀ Π 1 b -statement over S 2 1 provable in T 2 j , similar to Con in Krajíček and Pudlák, 29) or RCon in Krajı́ček and Takeuti 107). The advantage of our notion over the others is that RCon ∗ can directly be used to construct models of T 2 j . We apply this by (...) proving preservation theorems for theories of bounded arithmetic of the following well-known kind: The ∀ Π 1 b -separation of bounded arithmetic theories S 2 i from T 2 j is equivalent to the existence of a model of S 2 i which does not have a Δ 0 b -elementary extension to a model of T 2 j . More specific, let M ⊨ Ω 1 nst denote that there is a nonstandard element c in M such that the function n ↦ 2 log c is total in M . Let BLΣ 1 b be the bounded collection schema for Σ 1 b -formulas. We obtain the following preservation results: the ∀ Π 1 b -separation of S 2 i from T 2 j is equivalent to the existence of 1. a model of S 2 i +Ω 1 nst which is 1 b -closed w.r.t. T 2 j , 2. a countable model of S 2 i + BLΣ 1 b without weak end extensions to models of T 2 j. (shrink)

A notion called Herbrand saturation is shown to provide the model-theoretic analogue of a proof-theoretic method, Herbrand analysis, yielding uniform model-theoretic proofs of a number of important conservation theorems. A constructive, algebraic variation of the method is described, providing yet a third approach, which is finitary but retains the semantic flavor of the model-theoretic version.

The complexity class of [Formula: see text]-polynomial local search problems is introduced and is used to give new witnessing theorems for fragments of bounded arithmetic. For 1 ≤ i ≤ k + 1, the [Formula: see text]-definable functions of [Formula: see text] are characterized in terms of [Formula: see text]-PLS problems. These [Formula: see text]-PLS problems can be defined in a weak base theory such as [Formula: see text], and proved to be total in [Formula: see text]. Furthermore, the [Formula: (...) see text]-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 [Formula: see text]-principle that is conjectured to separate [Formula: see text] and [Formula: see text]. (shrink)

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.