We define a fragment of Primitive Recursive Arithmetic by replacing the defining axioms for primitive recursive functions by those for functions in some specific complexity class. In this note we consider such theory for AC0. We present a model-theoretical property of this theory, by means of which we are able to characterize its provably total functions. Next we consider the problem of how strong the induction scheme can be in this theory.

We give a uniform proof of the theorems of Yao and Beigel–Tarui representing ACC predicates as constant depth circuits with MODm\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\hbox {MOD}_{m}$$\end{document} gates and a symmetric gate. The proof is based on a relativized, generalized form of Toda’s theorem expressed in terms of closure properties of formulas under bounded universal, existential and modular counting quantifiers. This allows the main proofs to be expressed in terms of formula classes instead of Boolean circuits. (...) The uniform version of the Beigel–Tarui theorem is then obtained automatically via the Furst–Saxe–Sipser and Paris–Wilkie translations. As a special case, we obtain a uniform version of Razborov and Smolensky’s representation of AC0[p]\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\hbox {AC}^{0}[p]$$\end{document} circuits. The paper is partly expository, but is also motivated by the desire to recast Toda’s theorem, the Beigel–Tarui theorem, and their proofs into the language of bounded arithmetic. However, no knowledge of bounded arithmetic is needed. (shrink)

We extend results of Bonet, Buss and Pitassi on Bondy’s Theorem and of Nozaki, Arai and Arai on Bollobás’ Theorem by proving that Frankl’s Theorem on the trace of sets has quasipolynomial size Frege proofs. For constant values of the parametert, we prove that Frankl’s Theorem has polynomial size AC0-Frege proofs from instances of the pigeonhole principle.

Arithmetical definability has been extensively studied over the natural numbers. In this paper, we take up the study of arithmetical definability over finite structures, motivated by the correspondence between uniform AC0 and FO. We prove finite analogs of three classic results in arithmetical definability, namely that < and TIMES can first-order define PLUS, that < and DIVIDES can first-order define TIMES, and that < and COPRIME can first-order define TIMES. The first result sharpens the equivalence FO =FO to FO = (...) FO, answering a question raised by Barrington et al. about the Crane Beach Conjecture. Together with previous results on the Crane Beach Conjecture, our results imply that FO is strictly less expressive than FO = FO = FO. In more colorful language, one could say that, for parallel computation, multiplication is harder than addition. (shrink)

Every model of IΔ0 is the tally part of a model of the stringlanguage theory Th-FO . We show how to “smoothly” introduce in Th-FO the binary length function, whereby it is possible to make exponential assumptions in models of Th-FO. These considerations entail that every model of IΔ0 + ¬exp is a proper initial segment of a model of Th-FO and that a modicum of bounded collection is true in these models.

Theorems of hyperarithmetic analysis (THAs) occupy an unusual neighborhood in the realms of reverse mathematics and recursion theoretic complexity. They lie above all the fixed (recursive) iterations of the Turing Jump but below ATR $_{0}$ (and so $\Pi _{1}^{1}$ -CA $_{0}$ or the hyperjump). There is a long history of proof theoretic principles which are THAs. Until Barnes, Goh, and Shore [ta] revealed an array of theorems in graph theory living in this neighborhood, there was only one mathematical denizen. In (...) this paper we introduce a new neighborhood of theorems which are almost theorems of hyperarithmetic analysis (ATHAs). When combined with ACA $_{0}$ they are THAs but on their own they are very weak. We generalize several conservativity classes ( $\Pi _{1}^{1}$, r- $\Pi _{2}^{1}$, and Tanaka) and show that all our examples (and many others) are conservative over RCA $_{0}$ in all these senses and weak in other recursion theoretic ways as well. We provide denizens, both mathematical and logical. These results answer a question raised by Hirschfeldt and reported in Montalbán [2011] by providing a long list of pairs of principles one of which is very weak over RCA $_{0}$ but over ACA $_{0}$ is equivalent to the other which may be strong (THA) or very strong going up a standard hierarchy and at the end being stronger than full second order arithmetic. (shrink)