One of the central open questions in bounded arithmetic is whether Buss' hierarchy of theories of bounded arithmetic collapses or not. In this paper, we reformulate Buss' theories using free logic and conjecture that such theories are easier to handle. To show this, we first prove that Buss' theories prove consistencies of induction-free fragments of our theories whose formulae have bounded complexity. Next, we prove that although our theories are based on an apparently weaker logic, we can interpret theories in Buss' hierarchy by our theories using a simple translation. Finally, we investigate finitistic Gödel sentences in our systems in the hope of proving that a theory in a lower level of Buss' hierarchy cannot prove consistency of induction-free fragments of our theories whose formulae have higher complexity.
Intuitionistic first-order logic extended with a restricted form of Markov's principle is constructive and admits a Curry-Howard correspondence, as shown by Herbelin. We provide a simpler proof of that result and then we study intuitionistic first-order logic extended with unrestricted Markov's principle. Starting from classical natural deduction, we restrict the excluded middle and we obtain a natural deduction system and a parallel Curry-Howard isomorphism for the logic. We show that proof terms for existentially quantified formulas reduce to a list of individual terms representing all possi…
This paper from 2000 is a presentation of a status quæstionis at that tiime, to wit of the problem of the interpretability logic of {\em all}\/ reasonable arithmetical theories. We present both the arithmetical side and the modal side of the question.
A cyclic proof system gives us another way of representing inductive definitions and efficient proof search. In 2011 Brotherston and Simpson conjectured the equivalence between the provability of the classical cyclic proof system and that of the classical system of Martin-Lof's inductive definitions. This paper studies the conjecture for intuitionistic logic. This paper first points out that the countermodel of FOSSACS 2017 paper by the same authors shows the conjecture for intuitionistic logic is false in general. Then this paper shows the conjecture for intuitionistic logic is true under ari…
We formalize the notion of Herbrand Consistency in an appropriate way for bounded arithmetics, and show the existence of a finite fragment of ${\rm IΔ_0}$ whose Herbrand Consistency is not provable in the thoery ${\rm IΔ_0}$. We also show the existence of an ${\rm IΔ_0}-$derivable $Π_1-$sentence such that ${\rm IΔ_0}$ cannot prove its Herbrand Consistency.
We study the logic obtained by endowing the language of first-order arithmetic with second-order measure quantifiers. This new kind of quantification allows us to express that the argument formula is true in a certain portion of all possible interpretations of the quantified variable. We show that first-order arithmetic with measure quantifiers is capable of formalizing simple results from probability theory and, most importantly, of representing every recursive random function. Moreover, we introduce a realizability interpretation of this logic in which programs have access to an oracle from …
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 $\hatΠ^b_i$ 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^i_2$ and $S^i_2$ 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.
The elementary arithmetic operations $+,\cdot,\le$ on integers are well-known to be computable in the weak complexity class $\mathrm{TC}^0$, and it is a basic question what properties of these operations can be proved using only $\mathrm{TC}^0$-computable objects, i.e., in a theory of bounded arithmetic corresponding to $\mathrm{TC}^0$. We will show that the theory $\mathit{VTC}^0$ extended with an axiom postulating the totality of iterated multiplication (which is computable in $\mathrm{TC}^0$) proves induction for quantifier-free formulas in the language $\langle +,\cdot,\le \rangle$ (IOpen)…
The problem of $Π_1-$separating the hierarchy of bounded arithmetic has been studied in the paper. It is shown that the notion of Herbrand Consistency, in its full generality, cannot $Π_1-$separate the theory ${\rm IΔ_0+\bigwedge_jΩ_j}$ from ${\rm IΔ_0}$; though it can $Π_1-$separate ${\rm IΔ_0+Exp}$ from ${\rm IΔ_0}$. This extends a result of L. A. Kołodziejczyk (2006), by showing the unprovability of the Herbrand Consistency of ${\rm IΔ_0}$ in the theory ${\rm IΔ_0+\bigwedge_jΩ_j}$.
This paper is a continuation of the paper [16]. Namely, in [16] we have introduced, among others, the definition of the atomic entailment and we have constructed the system $\overset\sqcap S$, which is based on the atomic entailment. In this paper we show that the classical Arithmetic can be based on the Atomic Logic (see [17]).
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.
In this paper, we formalize Sprague-Grundy theory for combinatorial games in bounded arithmetic. We show that in the presence of Sprague-Grundy numbers, a fairly weak axioms capture PSPACE.
The interpretability logic of a mathematical theory describes the structural behavior of interpretations over that theory. Different theories have different logics. This paper from 2011 revolves around the question what logic describes the behavior that is present in all theories with a minimum amount of arithmetic; the intersection over all such theories so to say. We denote this target logic by ${\textbf{IL}}({\rm All})$. In this paper we present a new principle $\sf R$ in ${\textbf{IL}}({\rm All})$. We show that $\sf R$ does not follow from the logic ${\textbf{IL}}{\sf P_0W^*}$ that contain…
In this paper we explore the following question: how weak can a logic be for Rosser's essential undecidability result to be provable for a weak arithmetical theory? It is well known that Robinson's Q is essentially undecidable in intuitionistic logic, and P. Hajek proved it in the fuzzy logic BL for Grzegorczyk's variant of Q which interprets the arithmetic operations as non-total non-functional relations. We present a proof of essential undecidability in a much weaker substructural logic and for a much weaker arithmetic theory, a version of Robinson's R (with arithmetic operations also interp…
In 1994 Jech gave a model theoretic proof of Gödel's second incompleteness theorem for Zermelo-Fraenkel set theory in the following form: ZF does not prove that ZF has a model. Kotlarski showed that Jech's proof can be adapted to Peano Arithmetic with the role of models being taken by complete consistent extensions. In this note we take another step in the direction of replacing proof-theoretic by model-theoretic arguments. We show, without passing through the arithmetized completeness theorem, that the existence of a model of PA of complexity $Σ^0_2$ is independent of PA, where a model is ide…
Famous descriptive characterisations of P and PSPACE are restated in terms of the Cook-Nguyen style second order bounded arithmetic. We introduce an axiom of inductive definitions over second order bounded arithmetic. We show that P can be captured by the axiom of inflationary inductive definitions whereas PSPACE can be captured by the axiom of non-inflationary inductive definitions.
Gödel's second incompleteness theorem is proved for Herbrand consistency of some arithmetical theories with bounded induction, by using a technique of logarithmic shrinking the witnesses of bounded formulas, due to Z. Adamowicz [Herbrand consistency and bounded arithmetic, \textit{Fundamenta Mathematicae} 171 (2002) 279--292]. In that paper, it was shown that one cannot always shrink the witness of a bounded formula logarithmically, but in the presence of Herbrand consistency, for theories ${\rm IΔ_0+Ω_m}$ with $m\geqslant 2$, any witness for any bounded formula can be shortened logarithmicall…
A computational flow is a pair consisting of a sequence of computational problems of a certain sort and a sequence of computational reductions among them. In this paper we will develop a theory for these computational flows and we will use it to make a sound and complete interpretation for bounded theories of arithmetic. This property helps us to decompose a first order arithmetical proof to a sequence of computational reductions by which we can extract the computational content of low complexity statements in some bounded theories of arithmetic such as $IΔ_0$, $T^k_n$, $IΔ_0+EXP$ and $PRA$. I…
This paper presents proof that Buss's $S^2_2$ can prove the consistency of a fragment of Cook and Urquhart's $\mathrm{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^1_2$. Our proof relies on the notion of "computation" of the terms of $\mathrm{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 computati…
The provability logic of a theory $T$ captures the structural behavior of formalized provability in $T$ as provable in $T$ itself. Like provability, one can formalize the notion of relative interpretability giving rise to interpretability logics. Where provability logics are the same for all moderately sound theories of some minimal strength, interpretability logics do show variations. The logic IL(All) is defined as the collection of modal principles that are provable in any moderately sound theory of some minimal strength. In this paper we raise the previously known lower bound of IL(All) by…
In this paper, we study the provability logic of intuitionistic theories of arithmetic that prove their own completeness. We prove a completeness theorem for theories equipped with two provability predicates $\Box$ and $\triangle$ that prove the schemes $A\to\triangle A$ and $\Box\triangle S\to\Box S$ for $S\inΣ_1$. Using this theorem, we determine the logic of fast provability for a number of intuitionistic theories. Furthermore, we reprove a theorem previously obtained by M. Ardeshir and S. Mojtaba Mojtahedi determining the $Σ_1$-provability logic of Heyting Arithmetic.
This paper describes an axiomatic theory BT for constructive mathematics. BT has a predicative comprehension axiom for a countable number of set types and usual combinatorial operations. BT has intuitionistic logic, is consistent with classical logic and has such constructive features as consistency with formal Church thesis, and existence and disjunction properties. BT is mutually interpretable with a so called theory of arithmetical truth PATr and with a second-order arithmetic SA that contains infinitely many sorts of sets of natural numbers. We compare BT with some standard second-order ar…
This paper deals with three tools to compare proof-theoretic strength of formal arithmetical theories: interpretability, $Π^0_1$-conservativity and proving restricted consistency. It is well known that under certain conditions these three notions are equivalent and this equivalence is often referred to as the Orey-Hájek characterization of interpretability. In this paper we look with detail at the Orey-Hájek characterization and study what conditions are needed and in what meta-theory the characterizations can be formalized.
Parametric Presburger arithmetic concerns families of sets S_t in Z^d, for t in N, that are defined using addition, inequalities, constants in Z, Boolean operations, multiplication by t, and quantifiers on variables ranging over Z. That is, such families are defined using quantifiers and Boolean combinations of formulas of the form a(t) x <= b(t), where a(t) is in Z[t]^d, b(t) in Z[t]. A function g: N -> Z is a quasi-polynomial if there exists a period m and polynomials f_0, ..., f_{m-1} in Q[t] such that g(t)=f_i(t) for t congruent to i (mod m.) Recent results of Chen, Li, Sam; Calegari, Walk…
Japan Advanced Institute of Science and Technology（日本北陆先端科学技术大学院大学）
Bayesian reasoning plays a significant role both in human rationality and in machine learning. In this paper, we introduce transfinite modal logic, which combines modal logic with ordinal arithmetic, in order to formalize Bayesian reasoning semi-quantitatively. Technically, we first investigate some nontrivial properties of ordinal arithmetic, which then enable us to expand normal modal logic's semantics naturally and elegantly onto the novel transfinite modal logic, while still keeping the ordinary definition of Kripke models totally intact. Despite all the transfinite mathematical definition…
We study Basic Arithmetic, BA introduced by W. Ruitenburg. BA is an arithmetical theory based on basic logic which is weaker than intuitionistic logic. We show that the class of the provably total recursive functions of BA is a proper sub-class of the primitive recursive functions. Three extensions of BA, called BA+U, BA_c and EBA are investigated with relation to their provably total recursive functions. It is shown that the provably total recursive functions of these three extensions of BA are exactly the primitive recursive functions. Moreover, among other things, it is shown that the well-…
We completely characterize the logical hierarchy of various subsystems of weak arithmetic, namely: ZR, ZR + N, ZR + GCD, ZR + Bez, OI + N, OI + GCD, OI + Bez.
We prove that the theory of the extensional compositional truth predicate for the language of arithmetic with $Δ_0$-induction scheme for the truth predicate and the full arithmetical induction scheme is not conservative over Peano Arithmetic. In addition, we show that a slightly modified theory of truth actually proves the global reflection principle over the base theory.
Forcing in bounded arithmetic and set theory: analogies and differences
Charles University, Faculty of Arts（查理大学文学院）；University of Warwick, Department of Computer Science（华威大学计算机科学系）；Charles University, Faculty of Mathematics and Physics（查理大学数学物理学院）
For the Heyting Arithmetic HA, HA* is defined as the theory $\{A\mid {\sf HA}\vdash A^{\Box}\}$, where $A^{\Box}$ is called the box translation of $A$. We characterize the $Σ_1$-provability logic of HA* as a modal theory ${\sf iH}_σ^*$.
We present a bounded modified realisability and a bounded functional interpretation of intuitionistic nonstandard arithmetic with nonstandard principles. The functional interpretation is the intuitionistic counterpart of Ferreira and Gaspar's functional interpretation and has similarities with Van den Berg, Briseid and Safarik's functional interpretation but replacing finiteness by majorisability. We give a threefold contribution: constructive content and proof-theoretical properties of nonstandard arithmetic; filling a gap in the literature; being in line with nonstandard methods to analyse c…
