It is shown that all the provably total functions of Basic Arithmetic BA, a theory introduced by Ruitenburg based on Predicate Basic Calculus, are primitive recursive. Along the proof a new kind of primitive recursive realizability to which BA is sound, is introduced. This realizability is similar to Kleene's recursive realizability, except that recursive functions are restricted to primitive recursives.

Answering a question raised by Shavrukov and Visser :569–582, 2014), we show that the lattice of \-sentences ) over any computable enumerable consistent extension T of \ is uniformly dense. We also show that for every \ and \ refer to the known hierarchies of arithmetical formulas introduced by Burr for intuitionistic arithmetic) the lattices of \-sentences over any c.e. consistent extension T of the intuitionistic version of Robinson Arithmetic \ are uniformly dense. As an immediate consequence of the proof, (...) all these lattices are also locally universal. (shrink)

There is a very simple way in which the safe/normal variable discipline of Bellantoni–Cook recursion [S. Bellantoni, S. Cook, A new recursion theoretic characterization of the polytime functions, Computational Complexity 2 97–110] can be imposed on arithmetical theories like PA: quantify over safes and induct on normals. This weakens the theory severely, so that the provably recursive functions become more realistically computable . Earlier results of D. Leivant [Intrinsic theories and computational complexity, in: D. Leivant , Logic and Computational Complexity, (...) Lecture Notes in Computer Science, vol. 960, Springer-Verlag, 1995, pp. 177–194] are re-worked and extended in this new context, giving proof-theoretic characterizations of complexity classes between Grzegorczyk’s E2 and E3. (shrink)

In this paper, we consider, for a set \ of natural numbers, the following notions of finitenessFIN1:There are a natural number l and a bijection f between \\);FIN5:It is not the case that \\), and infinitenessINF1:There are not a natural number l and a bijection f between \\);INF5:\\). In this paper, we systematically compare them in the method of constructive reverse mathematics. We show that the equivalence among them can be characterized by various combinations of induction axioms and non-constructive principles, (...) including the axiom of bounded comprehension. (shrink)

We investigate which part of Brouwer’s Intuitionistic Mathematics is finitistically justifiable or guaranteed in Hilbert’s Finitism, in the same way as similar investigations on Classical Mathematics already done quite extensively in proof theory and reverse mathematics. While we already knew a contrast from the classical situation concerning the continuity principle, more contrasts turn out: we show that several principles are finitistically justifiable or guaranteed which are classically not. Among them are: fan theorem for decidable fans but arbitrary bars; continuity principle (...) and the axiom of choice both for arbitrary formulae; and $\Sigma _2$ induction and dependent choice. We also show that Markov’s principle MP does not change this situation; that neither does lesser limited principle of omniscience LLPO ; but that limited principle of omniscience LPO makes the situation completely classical. (shrink)

In this paper we prove conservation theorems for theories of classical first-order arithmetic over their intuitionistic version. We also prove generalized conservation results for intuitionistic theories when certain weak forms of the principle of excluded middle are added to them. Members of two families of subsystems of Heyting arithmetic and Buss-Harnik’s theories of intuitionistic bounded arithmetic are the intuitionistic theories we consider. For the first group, we use a method described by Leivant based on the negative translation combined with a (...) variant of Friedman’s translation. For the second group, we use Avigad’s forcing method. (shrink)

This paper proves some independence results for weak fragments of Heyting arithmetic by using Kripke models. We present a necessary condition for linear Kripke models of arithmetical theories which are closed under the negative translation and use it to show that the union of the worlds in any linear Kripke model of HA satisfies PA. We construct a two-node PA-normal Kripke structure which does not force iΣ2. We prove i∀1 ⊬ i∃1, i∃1 ⊬ i∀1, iΠ2 ⊬ iΣ2 and iΣ2 ⊬ (...) iΠ2. We use Smorynski's operation Σ′ to show HA ⊬ lΠ1. (shrink)

In this paper we define a suitable version of the notion of homomorphism for Kripke models of intuitionistic first-order logic and characterize theories that are preserved under images and also those that are preserved under inverse images of homomorphisms. Moreover, we define a notion of union of chain for Kripke models and define a class of formulas that is preserved in unions of chains. We also define similar classes of formulas and investigate their behavior in Kripke models. An application to (...) intuitionistic first-order arithmetic is also given. (shrink)

In "Intuitionistic validity in -normal Kripke structures," Buss asked whether every intuitionistic theory is, for some classical theory , that of all -normal Kripke structures for which he gave an r.e. axiomatization. In the language of arithmetic and denote PA plus Open Induction or Open LNP, and are their intuitionistic deductive closures. We show is recursively axiomatizable and , while . If proves PEM but not totality of a classically provably total Diophantine function of , then and so . A (...) result due to Wehmeier then implies . We prove is not -conservative over . If , then is not closed under MR or Friedman's translation, so range (). Both and are closed under the negative translation. (shrink)

We define classes Φnof formulae of first-order arithmetic with the following properties:(i) Everyφϵ Φnis classically equivalent to a Πn-formula (n≠ 1, Φ1:= Σ1).(ii)(iii)IΠnandiΦn(i.e., Heyting arithmetic with induction schema restricted to Φn-formulae) prove the same Π2-formulae.We further generalize a result by Visser and Wehmeier. namely that prenex induction within intuitionistic arithmetic is rather weak: After closing Φnboth under existential and universal quantification (we call these classes Θn) the corresponding theoriesiΘnstill prove the same Π2-formulae. In a second part we consideriΔ0plus collection-principles. We (...) show that both the provably recursive functions and the provably total functions ofare polynomially bounded. Furthermore we show that the contrapositive of the collection-schema gives rise to instances of the law of excluded middle and hence. (shrink)

In this paper we show that the intuitionistic theory for finitely many iterations of strictly positive operators is a conservative extension of Heyting arithmetic. The proof is inspired by the quick cut-elimination due to G. Mints. This technique is also applied to fragments of Heyting arithmetic.

In the first section of this paper we show that i Π1 ≡ W⌝⌝lΠ1 and that a Kripke model which decides bounded formulas forces iΠ1 if and only if the union of the worlds in any path in it satisflies IΠ1. In particular, the union of the worlds in any path of a Kripke model of HA models IΠ1. In the second section of the paper, we show that for equivalence of forcing and satisfaction of Πm-formulas in a linear Kripke (...) model deciding Δ0-formulas it is necessary and sufficient that the model be Σm-elementary. This implies that if a linear Kripke model forces PEMprenex, then it forces PEM. We also show that, for each n ≥ 1, iΦn does not prove ℋ(IΠn's are Burr's fragments of HA. (shrink)