The notion of strictly primitive recursive realizability is further investigated, and the realizable prenex sentences, which coincide with primitive recursive truths of classical arithmetic, are characterized as precisely those provable in transfinite progressions over a fragment of intuitionistic arithmetic. The progressions are based on uniform reflection principles of bounded complexity iterated along initial segments of a primitive recursively formulated system of notations for constructive ordinals. A semiformal system closed under a primitive recursively restricted (...) -rule is described and proved equivalent to the transfinite progressions with respect to the prenex sentences. (shrink)

A realizability notion that employs only primitive recursive functions is defined, and, relative to it, the soundness of the fragment of Heyting Arithmetic (HA) in which induction is restricted to Σ 0 1 formulae is proved. A dual concept of falsifiability is proposed and an analogous soundness result is established for a further restricted fragment of HA.

A notion of strictly primitive recursive realizability is introduced by Damnjanovic in 1994. It is a kind of constructive semantics of the arithmetical sentences using primitive recursive functions. It is of interest to study the corresponding predicate logic. It was argued by Park in 2003 that the predicate logic of strictly primitive recursive realizability is not arithmetical. Park’s argument is essentially based on a claim of Damnjanovic that intuitionistic logic is sound with (...) respect to strictly primitive recursive realizability, but that claim was disproved by the author of this article in 2006. The aim of this paper is to present a correct proof of the result of Park. (shrink)

Let the chain antichain principle (CAC) be the statement that each partial order on $\mathbb{N}$ possesses an infinite chain or an infinite antichain. Chong, Slaman, and Yang recently proved using forcing over nonstandard models of arithmetic that CAC is $\Pi^1_1$-conservative over $\text{RCA}_0+\Pi^0_1\text{-CP}$ and so in particular that CAC does not imply $\Sigma^0_2$-induction. We provide here a different purely syntactical and constructive proof of the statement that CAC (even together with WKL) does not imply $\Sigma^0_2$-induction. In detail we show using a (...) refinement of Howard's ordinal analysis of bar recursion that $\text{WKL}_0^\omega+\text{CAC}$ is $\Pi^0_2$-conservative over PRA and that one can extract primitive recursive realizers for such statements. Moreover, our proof is finitary in the sense of Hilbert's program. CAC implies that every sequence of $\mathbb{R}$ has a monotone subsequence. This Bolzano-Weierstraß}-like principle is commonly used in proofs. Our result makes it possible to extract primitive recursive terms from such proofs. We also discuss the Erdős-Moser principle, which—taken together with CAC—is equivalent to $\text{RT}^2_2$. (shrink)

A polynomially bounded recursive realizability, in which the recursive functions used in Kleene's realizability are restricted to polynomially bounded functions, is introduced. It is used to show that provably total functions of Ruitenburg's Basic Arithmetic are polynomially bounded (primitive) recursive functions. This sharpens our earlier result where those functions were proved to be primitive recursive. Also a polynomially bounded schema of Church's Thesis is shown to be polynomially bounded realizable. So the schema (...) is consistent with Basic Arithmetic, whereas it is inconsistent with Heyting Arithmetic. (shrink)

We give a counterexample to the claim that every provably total function of Basic Arithmetic is a polynomially bounded primitive recursive function.

The provability logic of a theory $T$ is the set of modal formulas, which under any arithmetical realization are provable in $T$. We slightly modify this notion by requiring the arithmetical realizations to come from a specified set $\Gamma$. We make an analogous modification for interpretability logics. We first study provability logics with restricted realizations and show that for various natural candidates of $T$ and restriction set $\Gamma$, the result is the logic of linear frames. However, for the theory (...) class='Hi'>Primitive Recursive Arithmetic (PRA), we define a fragment that gives rise to a more interesting provability logic by capitalizing on the well-studied relationship between PRA and I$\Sigma_1$. We then study interpretability logics, obtaining upper bounds for IL(PRA), whose characterization remains a major open question in interpretability logic. Again this upper bound is closely related to linear frames. The technique is also applied to yield the nontrivial result that IL(PRA) $\subset$ ILM. (shrink)

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.

Let ${2-\textsf{RAN}}$ be the statement that for each real X a real 2-random relative to X exists. We apply program extraction techniques we developed in Kreuzer and Kohlenbach (J. Symb. Log. 77(3):853–895, 2012. doi:10.2178/jsl/1344862165), Kreuzer (Notre Dame J. Formal Log. 53(2):245–265, 2012. doi:10.1215/00294527-1715716) to this principle. Let ${{\textsf{WKL}_0^\omega}}$ be the finite type extension of ${\textsf{WKL}_0}$ . We obtain that one can extract primitive recursive realizers from proofs in ${{\textsf{WKL}_0^\omega} + \Pi^0_1-{\textsf{CP}} + 2-\textsf{RAN}}$ , i.e., if ${{\textsf{WKL}_0^\omega} + \Pi^0_1-{\textsf{CP}} (...) + 2-\textsf{RAN} \, {\vdash} \, \forall{f}\, {\exists}{x} A_{qf}(f,x)}$ then one can extract from the proof a primitive recursive term t(f) such that ${A_{qf}(f,t(f))}$ . As a consequence, we obtain that ${{\textsf{WKL}_0}+ \Pi^0_1 - {\textsf{CP}} + 2-\textsf{RAN}}$ is ${\Pi^0_3}$ -conservative over ${\textsf{RCA}_0}$. (shrink)

The complexity of equivalence relations has received much attention in the recent literature. The main tool for such endeavour is the following reducibility: given equivalence relations R and S on natural numbers, R is computably reducible to S if there is a computable function f:ω→ω that induces an injective map from R-equivalence classes to S-equivalence classes. In order to compare the complexity of equivalence relations which are computable, researchers considered also feasible variants of computable reducibility, such as the polynomial-time reducibility. (...) In this work, we explore Peq, the degree structure generated by primitive recursive reducibility on primitive recursive equivalence relations with infinitely many equivalence classes. In contrast with all other known degree structures on equivalence relations, we show that Peq has much more structure: e.g., we show that it is a dense distributive lattice. On the other hand, we also offer evidence of the intricacy of Peq, proving, e.g., that the structure is neither rigid nor homogeneous. (shrink)

In the first part of this paper we investigate the intuitionistic version $iI\!\Sigma_1$ of $I\!\Sigma_1$ (in the language of $PRA$ ), using Kleene's recursive realizability techniques. Our treatment closely parallels the usual one for $HA$ and establishes a number of nice properties for $iI\!\Sigma_1$ , e.g. existence of primitive recursive choice functions (this is established by different means also in [D94]). We then sharpen an unpublished theorem of Visser's to the effect that quantifier alternation alone is (...) much less powerful intuitionistically than classically: $iI\!\Sigma_1$ together with induction over arbitrary prenex formulas is $\Pi_2$ -conservative over $iI\!\Pi_2$ . In the second part of the article we study the relation of $iI\!\Sigma_1$ to $iI\!\Pi_1$ (in the usual arithmetical language). The situation here is markedly different from the classical case in that $iI\!\Pi_1$ and $iI\!\Sigma_1$ are mutually incomparable, while $iI\!\Sigma_1$ is significantly stronger than $iI\!\Pi_1$ as far as provably recursive functions are concerned: All primitive recursive functions can be proved total in $iI\!\Sigma_1$ whereas the provably recursive functions of $iI\!\Pi_1$ are all majorized by polynomials over ${\Bbb N}$ . 0 $iI\!\Pi_1$ is unusual also in that it lacks closure under Markov's Rule $\mbox{MR}_{PR}$. (shrink)

In mathematics, various representations of real numbers have been investigated. All these representations are mathematically equivalent because they lead to the same real structure - Dedekind-complete ordered field. Even the effective versions of these representations are equivalent in the sense that they define the same notion of computable real numbers. Although the computable real numbers can be defined in various equivalent ways, if computable is replaced by primitive recursive (p. r., for short), these definitions lead to a number (...) of different concepts, which we compare in this article. We summarize the known results and add new ones. In particular we show that there is a proper hierarchy among p. r. real numbers by nested interval representation, Cauchy representation, b -adic expansion representation, Dedekind cut representation, and continued fraction expansion representation. Our goal is to clarify systematically how the primitive recursiveness depends on the representations of the real numbers. (shrink)

This paper introduces an extension A of Kleene's axiomatization of Brouwer's intuitionistic analysis, in which the classical arithmetical and analytical hierarchies are faithfully represented as hierarchies of the domains of continuity. A domain of continuity is a relation R(α) on Baire space with the property that every constructive partial functional defined on {α : R(α)} is continuous there. The domains of continuity for A coincide with the stable relations (those equivalent in A to their double negations), while every relation R(α) (...) is equivalent in A to ∃αA(α, β) for some stable A(α, β) (which belongs to the classical analytical hierarchy). The logic of A is intuitionistic. The axioms of A include countable comprehension, bar induction, Troelstra's generalized continuous choice, primitive recursive Markov's Principle and a classical axiom of dependent choices proposed by Krauss. Constructive dependent choices, and constructive and classical countable choice, are theorems, A is maximal with respect to classical Kleene function realizability, which establishes its consistency. The usual disjunction and (recursive) existence properties ensure that A preserves the constructive sense of "or" and "there exists.". (shrink)

Several properties of monotone functionals (MF) and monotone majorizable functionals (MMF) used in the earlier work by the author and van de Pol are proved. It turns out that the terms of the simply typed lambda-calculus define MF, but adding primitive recursion, and even monotonic primitive recursion changes the situation: already Z.Z(1 — sg) is not MMF. It is proved that extensionality is not Dialectica-realizable by MMF, and a simple example of a MF which is not hereditarily majorizable (...) is given. (shrink)

In this article, we study some new characterizations of primitive recursive functions based on restricted forms of primitive recursion, improving the pioneering work of R. M. Robinson and M. D. Gladstone. We reduce certain recursion schemes (mixed/pure iteration without parameters) and we characterize one-argument primitive recursive functions as the closure under substitution and iteration of certain optimal sets.

arbitrary flowchart programs by introducing a new recursive function for each tag point. In the above example, one obtains: int = int1, p..... 1 h ), w...., y2r )_.

The last Episode wasn’t about logic or formal theories at all: it was about common-or-garden arithmetic and the informal notion of computability. We noted that addition can be defined in terms of repeated applications of the successor function. Multiplication can be defined in terms of repeated applications of addition. The exponential and factorial functions can be defined, in different ways, in terms of repeated applications of multiplication. There’s already a pattern emerging here! The main task in the last Episode was (...) to get clear about this pattern. So first we said more about the idea of defining one function in terms of repeated applications of another function. Tidied up, that becomes the idea of defining a function by primitive recursion (Defn. 27). (shrink)

We show that—unlike products of ‘transitive’ modal logics which are usually undecidable—their ‘expanding domain’ relativisations can be decidable, though not in primitive recursive time. In particular, we prove the decidability and the finite expanding product model property of bimodal logics interpreted in two-dimensional structures where one component—call it the ‘flow of time’—is • a finite linear order or a finite transitive tree and the other is composed of structures like • transitive trees/partial orders/quasi-orders/linear orders or only finite such (...) structures expanding over time. The decidability proof is based on Kruskal’s tree theorem, and the proof of non-primitive recursiveness is by reduction of the reachability problem for lossy channel systems. The result is used to show that the dynamic topological logic interpreted in topological spaces with continuous functions is decidable if the number of function iterations is assumed to be finite. (shrink)

In our preamble, it might be helpful this time to give a story about where we are going, rather than (as in previous episodes) review again where we’ve been. So, at the risk of spoiling the excitement, here’s what’s going to happen in this and the following three Episodes.

In mathematics, various representations of real numbers have been investigated. All these representations are mathematically equivalent because they lead to the same real structure – Dedekind-complete ordered field. Even the effective versions of these representations are equivalent in the sense that they define the same notion of computable real numbers. Although the computable real numbers can be defined in various equivalent ways, if “computable” is replaced by “primitive recursive” , these definitions lead to a number of different concepts, (...) which we compare in this article. We summarize the known results and add new ones. In particular we show that there is a proper hierarchy among p. r. real numbers by nested interval representation, Cauchy representation, b -adic expansion representation, Dedekind cut representation, and continued fraction expansion representation. Our goal is to clarify systematically how the primitive recursiveness depends on the representations of the real numbers. (shrink)

Although Peano arithmetic is necessarily incomplete, Isaacson argued that it is in a sense conceptually complete: proving a statement of the language of PA that is independent of PA will require conceptual resources beyond those needed to understand PA. This paper gives a test of Isaacon’s thesis. Understanding PA requires understanding the functions of addition and multiplication. It is argued that grasping these primitive recursive functions involves grasping the double ancestral, a generalized version of the ancestral operator. Thus, (...) we can test Isaacon’s thesis by seeing whether when we phrase arithmetic in a context with the double ancestral operator, the result is conservative over PA. This is a stronger version of the test given by Smith, who argued that understanding the predicate “natural number” requires understanding the ancestral operator, but did not investigate what is required to understand the arithmetic functions. (shrink)

In this paper, we develop primitive recursive analogues of regular cardinals by using ordinal representation systems for KPi and KPM. We also define primitive recursive analogues of inaccessible and hyperinaccessible cardinals. Moreover, we characterize the primitive recursive analogue of the least (uncountable) regular cardinal.

It has been known for some time that there is a primitive recursive permutation of the nonnegative integers whose inverse is recursive but not primitive recursive. For example one has this result apparently for the first time in Kuznecov [1] and implicitly in Kent [2] or J. Robinson [3], who shows that every singularly recursive function ƒ is representable aswhere A, B, C are primitive recursive and B is a permutation.

The present paper focuses on Graham Priest’s claim that even primitive recursive relations may be inconsistent. Although he carefully presented his claim using the expression “may be,” Priest made a definite claim that even numerical equations can be inconsistent. His argument relies heavily on the fact that there is an inconsistent model for arithmetic. After summarizing Priest’s argument for the inconsistent primitive recursive relation, I first discuss the fact that his argument has a weak foundation to (...) explain that the existence of a model for some relations does not guarantee that they are primitive recursive. Moreover, since his identity relation is a combination of a standard identity and a congruence relation, it does not simply represent the standard identity function. Then, I argue that his identity relation cannot be both inconsistent and primitive recursive. Furthermore, I extend the argument to the general case that there is no inconsistent primitive recursive relation. These arguments show that the standard notions of “function” and “primitive recursive function” do not fit Priest’s inconsistent model. New definitions are necessary to show the existence of a dialetheic primitive recursive relation. (shrink)

Shoenfield’s completeness theorem states that every true first order arithmetical sentence has a recursive \-proof encodable by using recursive applications of the \-rule. For a suitable encoding of Gentzen style \-proofs, we show that Shoenfield’s completeness theorem applies to cut free \-proofs encodable by using primitive recursive applications of the \-rule. We also show that the set of codes of \-proofs, whether it is based on recursive or primitive recursive applications of the \-rule, (...) is \ complete. The same \ completeness results apply to codes of cut free \-proofs. (shrink)

We construct by diagonalization a non-well-founded primitive recursive tree, which is well-founded for co-r.e. sets, provable in Σ1 0. It follows that the supremum of order-types of primitive recursive well-orderings, whose well-foundedness on co-r.e. sets is provable in Σ1 0, equals the limit of all recursive ordinals ω1 ck . RID=""ID="" Mathematics Subject Classification (2000): 03B30, 03F15 RID=""ID="" Supported by the Deutschen Akademie der Naturforscher Leopoldina grant #BMBF-LPD 9801-7 with funds from the Bundesministerium für Bildung, (...) Wissenschaft, Forschung und Technologie. RID=""ID="" I would like to thank A. SETZER for his hospitality during my stay in Uppsala in December 1998 – these investigations are inspired by a discussion with him; S. BUSS for his hospitality during my stay at UCSD and for valuable remarks on a previous version of this paper; and M. MÖLLERFELD for remarks on a previous title. (shrink)

This paper is a companion to work of Feferman, Jäger, Glaß, and Strahm on the proof theory of the type two functionals μ and E1 in the context of Feferman-style applicative theories. In contrast to the previous work, we analyze these two functionals in the context of Schlüter's weakened applicative basis PRON which allows for an interpretation in the primitive recursive indices. The proof-theoretic strength of PRON augmented by μ and E1 is measured in terms of the two (...) subsystems of second order arithmetic, Π10-CA and Π11-CA, respectively. (shrink)

Let KP- be the theory resulting from Kripke-Platek set theory by restricting Foundation to Set Foundation. Let G: V → V (V:= universe of sets) be a ▵0-definable set function, i.e. there is a ▵0-formula φ(x, y) such that φ(x, G(x)) is true for all sets x, and $V \models \forall x \exists!y\varphi (x, y)$ . In this paper we shall verify (by elementary proof-theoretic methods) that the collection of set functions primitive recursive in G coincides with the (...) collection of those functions which are Σ1-definable in KP- + Σ1-Foundation + ∀ x ∃!yφ (x, y). Moreover, we show that this is still true if one adds Π1-Foundation or a weak version of ▵0-Dependent Choices to the latter theory. (shrink)

The termination of rewrite systems for parameter recursion, simple nested recursion and unnested multiple recursion is shown by using monotone interpretations both on the ordinals below the first primitive recursively closed ordinal and on the natural numbers. We show that the resulting derivation lengths are primitive recursive. As a corollary we obtain transparent and illuminating proofs of the facts that the schemata of parameter recursion, simple nested recursion and unnested multiple recursion lead from primitive recursive (...) functions to primitive recursive functions. (shrink)

The paper builds on both a simply typed term system ${\cal PR}^\omega$ and a computation model on Scott domains via so-called parallel typed while programs (PTWP). The former provides a notion of partial primitive recursive functional on Scott domains $D_\rho$ supporting a suitable concept of parallelism. Computability on Scott domains seems to entail that Kleene's schema of higher type simultaneous course-of-values recursion (scvr) is not reducible to partial primitive recursion. So extensions ${\cal PR}^{\omega e}$ and PTWP $^e$ (...) are studied that are closed under scvr. The twist are certain type 1 Gödel recursors ${\cal R}_k$ for simultaneous partial primitive recursion. Formally, ${\cal R}_k\vec{g}\vec{H}xi$ denotes a function $f_i \in D_{\iota\to\iota}$ , however, ${\cal R}_k$ is modelled such that $f_i$ is finite, or in other words, a partial sequence. As for PTWP $^e$ , the concept of type $\iota\to\iota$ writable variables is introduced, providing the possibility of creating and manipulating partial sequences. It is shown that the PTWP $^e$ -computable functionals coincide with those definable in ${\cal PR}^{\omega e}$ plus a constant for sequential minimisation. In particular, the functionals definable in ${\cal PR}^{\omega e}$ denoted ${\cal R}^{\omega e}$ can be characterised by a subclass of PTWP $^e$ -computable functionals denoted ${\rm PPR}^{\omega e}$ . Moreover, hierarchies of strictly increasing classes ${\cal R}^{\omega e}_n$ in the style of Heinermann and complexity classes ${\rm PPR}^{\omega e}_n$ are introduced such that $\forall n\ge 0. {\cal R}^{\omega e}_n ={\rm PPR}^{\omega e}_n$ . These results extend those for ${\cal PR}^\omega$ and PTWP [Nig94]. Finally, scvr is employed to define for each type $\sigma$ the enumeration functional $E^\sigma$ of all finite elements of $D_\sigma$. (shrink)

The paper builds on a simply typed term system ${\cal PR}^\omega $ providing a notion of partial primitive recursive functional on arbitrary Scott domains $D_\sigma$ that includes a suitable concept of parallelism. Computability on the partial continuous functionals seems to entail that Kleene's schema of higher type simultaneous course-of-values recursion (SCVR) is not reducible to partial primitive recursion. So an extension ${\cal PR}^{\omega e}$ is studied that is closed under SCVR and yet stays within the realm of (...) subrecursiveness. The twist are certain type 1 Gödel recursors ${\cal R}_k$ for simultaneous partial primitive recursion. Formally, the value ${\cal R}_k\vec{g}\vec{H} x i$ is a function $f_i$ of type $\iota \to \iota$ , however, ${\cal R}_k$ is modelled such that $f_i$ is a finite element of $D_{\iota\to\iota}$ or in other words, a partial sequence. It is shown that the Ackermann function is not definable in ${\cal PR}^{\omega e}$. (shrink)

We study the monoid of primitive recursive functions and investigate a onestep construction of a kind of exact completion, which resembles that of the familiar category of modest sets, except that the partial equivalence relations which serve as objects are recursively enumerable. As usual, these constructions involve the splitting of symmetric idempotents.