Fact-checked by Grok 2 weeks ago

Primitive recursive arithmetic

Primitive recursive arithmetic (PRA) is a quantifier-free axiomatic theory of the natural numbers that formalizes the primitive recursive functions through defining equations and a schema of quantifier-free induction, providing a finitist foundation for elementary arithmetic without reliance on full second-order logic or impredicative definitions.^[1] Introduced by Norwegian mathematician Thoralf Skolem in his 1923 paper "The Foundations of Elementary Arithmetic Established by Means of the Recursive Mode of Thought, Without the Use of Apparent Variables Ranging Over Infinite Domains," PRA emerged as a response to the logicist program of Russell and Whitehead, emphasizing recursive definitions to avoid quantification over infinite sets while capturing the content of basic arithmetic.^[2] Skolem's system, later formalized more explicitly in works by Goodstein and others, consists of basic axioms for zero, successor, and projection functions, closure under composition and primitive recursion—defined by schemes such as f(0, \vec{z}) = g(\vec{z}) and f(x+1, \vec{z}) = h(x, f(x, \vec{z}), \vec{z})—along with equality axioms and the quantifier-free induction rule: if \phi(0) and \phi(x) \to \phi(S(x)), then \phi(t) for any term t, where \phi is a quantifier-free formula built from primitive recursive predicates.^[2] This framework proves the uniqueness of primitive recursive definitions and derives mathematical induction for primitive recursive properties, establishing PRA as conservatively equivalent to the equational theory of primitive recursive functions. In proof theory, PRA serves as a benchmark for finitist mathematics, aligning with Hilbert's program by enabling the extraction of provably total recursive functions from stronger systems like Peano arithmetic, and it underlies extensions such as Gödel's system T and higher-type functional calculi.^[1] Its weakness—lacking full quantifiers—ensures that all theorems are interpretable in finitary terms, making it a key tool for analyzing the consistency and interpretability of more comprehensive arithmetical theories.

Overview

Definition and motivation

Primitive recursive arithmetic (PRA) is a first-order axiomatic theory that formalizes the natural numbers using a language equipped with symbols for basic arithmetic operations, including zero, successor, addition, and multiplication, along with defining axioms for these and other primitive recursive functions, and a scheme of quantifier-free induction restricted to primitive recursive predicates.^[3] This induction schema allows proofs of properties that hold for zero and are preserved under the successor operation, applied only to formulas without quantifiers, ensuring the theory remains finitistic and avoids higher-order quantification.^[3] In proof theory, PRA serves as a foundational base system for assessing the proof-theoretic strength of more powerful arithmetics, such as Peano arithmetic (PA), through conservation results that demonstrate how stronger theories do not prove additional sentences of certain forms beyond what PRA can establish.^[4] For instance, the theory I\Sigma_1, which extends PRA with induction for \Sigma^0_1 formulas, is \Pi^0_2-conservative over PRA, meaning that any \Pi^0_2 sentence provable in I\Sigma_1 is already provable in PRA.^[4] This conservativity highlights PRA's role in bounding the additional power introduced by extended induction principles. A key distinction from full Peano arithmetic lies in PRA's limited induction: while PA includes the full induction schema applicable to all first-order formulas, PRA restricts itself to \Sigma^0_1-induction, which is equivalent to quantifier-free induction for primitive recursive predicates, thereby excluding proofs that rely on unbounded quantifiers.^[3] PRA's primary goal is to axiomatize precisely those total computable functions definable via primitive recursion—such as addition and exponentiation—without encompassing the full class of total recursive functions, like the Ackermann function, thus providing a strict subsystem of general recursion theory.^[3]

Historical development

The roots of primitive recursive arithmetic (PRA) trace back to the early 20th century, particularly within David Hilbert's program for the foundations of mathematics, which emphasized finitistic methods to establish the consistency of formal systems during the 1920s. Norwegian mathematician Thoralf Skolem laid crucial groundwork in his 1923 paper, where he introduced a recursive mode of thought for developing elementary arithmetic without apparent variables over infinite domains, effectively outlining the structure of what would later be formalized as PRA.^[5] Although Skolem's presentation lacked a full first-order axiomatization, PRA was formally developed in subsequent works, including Hilbert and Bernays' 1934 Grundlagen der Mathematik (Volume II, Chapter 7) and R. L. Goodstein's 1951 Recursive Number Theory.^[5] Wilhelm Ackermann contributed in 1928 by demonstrating functions that transcend primitive recursion through higher-type definitions, highlighting the boundaries of recursive methods in the context of Hilbert's problems.^[5] Kurt Gödel advanced the concepts significantly in his early work, formalizing primitive recursive functions in his 1931 paper on incompleteness theorems, building on ideas from his 1929 dissertation to define a class of total computable functions closed under composition and primitive recursion.^[5] Gödel employed PRA as the base theory in his 1958 paper "Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes," where it provided a quantifier-free framework for his Dialectica interpretation of intuitionistic arithmetic, drawing on earlier recursive ideas from Skolem and Ackermann and positioning PRA as a conservative subsystem suitable for analyzing stronger arithmetics like Peano arithmetic.^[5] In the 1950s, Georg Kreisel further developed PRA within proof theory, emphasizing its role in extracting constructive content from classical proofs and linking it to intuitionistic logic through unwinding techniques.^[6] During the 1960s and 1970s, Solomon Feferman and others refined PRA for consistency analyses of Peano arithmetic, incorporating it into ordinal-theoretic frameworks and exploring its interpretability results.^[6] By the 1970s, PRA evolved from Skolem's and Gödel's logic-free presentations toward standard first-order formulations, facilitating broader applications in metamathematics while preserving its finitistic core.^[6]

Formal System

Language

The first-order language of primitive recursive arithmetic (PRA) consists of a signature tailored to formalize basic arithmetic operations over the natural numbers. It includes the constant symbol $0, the unary function symbol S denoting the successor operation, the binary function symbols + for addition and \times for multiplication, and equality = as a standard logical predicate. The strict less-than relation < is definable as x < y \leftrightarrow \exists z \, (x + S(z) = y). Variables, denoted by x, y, z, \dots, range over natural numbers, with no higher-type variables permitted.^[7]^[8] Terms in this language are constructed inductively from the signature. Specifically, every variable is a term; the constant $0 is a term; if t is a term, then S(t) is a term; and if t and s are terms, then t + s and t \times s are terms. This inductive definition ensures that all terms represent primitive recursive functions applied to variables or constants, without allowing arbitrary nesting beyond the specified function symbols.^[7]^[8] Formulas are built in the standard way for first-order logic. Atomic formulas are equations t = s, where t and s are terms. Quantifier-free formulas are obtained by combining atomic formulas using the propositional connectives \neg, \land, \lor, and \to. The full set of formulas is generated by applying the universal quantifier \forall and existential quantifier \exists to quantifier-free formulas, yielding a complete first-order language without non-standard symbols or extensions.^[7]^[9] Bounded quantifiers provide a notation for expressing \Sigma_1^0 formulas succinctly within PRA. For a quantifier-free formula \phi(x) and a term t, the bounded universal quantifier is written \forall x \le t \, \phi(x), which abbreviates \forall x (x < t \to \phi(x)) \land \phi(t), and the bounded existential quantifier \exists x \le t \, \phi(x) abbreviates \exists x (x < t \land \phi(x)) \lor \phi(t). These abbreviations facilitate the formulation of induction axioms restricted to bounded quantification.^[7]^[8] Unlike stronger systems such as subsystems of second-order arithmetic, PRA's language is strictly first-order, lacking monadic second-order variables or quantification over sets or functions, which limits its expressive power to primitive recursive predicates.^[9]

Axioms and inference rules

Primitive recursive arithmetic (PRA) is formulated as a first-order theory over the natural numbers, featuring the constant symbol $0, the unary [successor function](/page/Successor_function) S, and the binary functions +([addition](/page/Addition)) and\times (multiplication). The logical framework includes the standard axioms and rules of classical [first-order logic](/page/First-order_logic) with equality, where equality satisfies reflexivity (\forall x (x = x)), symmetry (\forall x \forall y (x = y \to y = x)), [transitivity](/page/Transitivity) (\forall x \forall y \forall z (x = y \land y = z \to x = z)), and [congruence](/page/Congruence) (for any terms t, u, vand function symbolsf, if t = uthenf(\dots, t, \dots) = f(\dots, u, \dots)$).^[10] The non-logical axioms consist of those defining the basic arithmetic operations, mirroring the axioms of Robinson arithmetic Q. These include the successor axioms: \forall x \, (S(x) \neq 0) and \forall x \forall y \, (S(x) = S(y) \to x = y), which ensure that the successor function is injective and never yields zero. The addition axioms are \forall x \, (x + 0 = x) and \forall x \forall y \, (x + S(y) = S(x + y)), recursively defining addition via successor. Similarly, the multiplication axioms are \forall x \, (x \times 0 = 0) and \forall x \forall y \, (x \times S(y) = (x \times y) + x), building multiplication from addition. The less-than relation is defined by the axiom schema \forall x \forall y \, (x < y \leftrightarrow \exists z \, (x + S(z) = y)).^[10] An equivalent first-order formulation of PRA incorporates a restricted induction schema, known as \Sigma^0_1-induction (equivalent to quantifier-free induction in the language extended by symbols for all primitive recursive functions), to limit its strength compared to full Peano arithmetic. For any \Sigma^0_1 formula \phi(x) of the form \exists y \, \psi(x, y) where \psi is quantifier-free, the axiom schema provides:

\phi(0) \land \forall x \, (\phi(x) \to \phi(S(x))) \to \forall x \, \phi(x).

This allows induction only on predicates definable by existential quantification over primitive recursive relations, ensuring that all provably total functions in PRA are primitive recursive.^[10] The inference rules are the conventional ones for first-order logic: modus ponens (from \phi and \phi \to \psi, infer \psi), universal generalization (from \phi(t) infer \forall x \, \phi(x) provided x is not free in assumptions), and quantifier instantiation (from \forall x \, \phi(x) infer \phi(t) for any term t). These rules, combined with the axioms, enable derivations within the bounded inductive framework of PRA.^[10] An alternative presentation of PRA avoids explicit quantifiers and first-order logic, instead using axiom schemata directly for each primitive recursive function and relation. In this logic-free variant, the non-logical axioms define basic functions (zero, successor, projections) and closure under composition and primitive recursion without induction, while induction is restricted to quantifier-free formulas in the language extended by all primitive recursive symbols; the \Sigma^0_1-induction is realized as a rule allowing proofs of totality for such predicates. This formulation is equivalent in strength to the first-order version and emphasizes the computational content of primitive recursion.^[10]

Primitive Recursive Functions

Basic functions and closure operations

The primitive recursive functions are generated starting from a set of basic functions and applying closure operations, primarily composition, to build more complex functions. The basic functions consist of three types: the zero function, the successor function, and the projection functions.^[5] The zero function, often denoted Z(x_1, \dots, x_n) = 0, is a constant function that ignores its inputs and returns 0 for any arity n \geq 0. This serves as the base for constructing constants in arithmetic. The successor function, denoted S(x) = x + 1, is a unary function that increments its argument by one, forming the foundation for counting and addition-like operations. The projection functions, denoted I_i^n(x_1, \dots, x_n) = x_i for $1 \leq i \leq n, simply return the i-th input argument, enabling the selection and rearrangement of values in compositions.^[5]^[11] A key closure operation is composition, which allows combining existing primitive recursive functions to form new ones. Formally, if g is an m-ary primitive recursive function and h_1, \dots, h_m are n-ary primitive recursive functions, then the composed function f(x_1, \dots, x_n) = g(h_1(x_1, \dots, x_n), \dots, h_m(x_1, \dots, x_n)) is also primitive recursive. This operation preserves the totality and computability of the functions involved. Through repeated composition, simple functions like constants can be built; for instance, the constant function 1 is S(Z(x)), and higher constants follow by further applications of successor.^[5]^[12] Addition and multiplication exemplify primitive recursive functions constructed from basic functions using closure under both composition and primitive recursion. For instance, addition integrates projections and the successor function via recursion to build the result iteratively, as detailed in the following subsection. Similarly, multiplication is defined recursively using addition along with projections to accumulate products. The class of primitive recursive functions is precisely the smallest class of total functions from natural numbers to natural numbers that contains the basic functions and is closed under composition and primitive recursion.^[5]^[12]

Recursion schema in PRA

The primitive recursion schema constitutes a core mechanism in primitive recursive arithmetic (PRA) for defining new functions from existing ones, ensuring that all primitive recursive functions can be generated starting from basic functions and composition. Formally, given an n-ary primitive recursive function g and an (n+2)-ary primitive recursive function h, the (n+1)-ary function f is defined as follows:

\begin{align*} f(0, \mathbf{x}) &= g(\mathbf{x}), \\ f(y+1, \mathbf{x}) &= h(y, f(y, \mathbf{x}), \mathbf{x}), \end{align*}

where \mathbf{x} = (x_1, \dots, x_n). This schema encodes iteration over the natural numbers in a bounded manner, with the base case at 0 and each subsequent value depending only on the previous one and the fixed parameters \mathbf{x}.^[5] A simple application yields the predecessor function, which reverses the successor operation S(z) = z+1. It is defined recursively as \operatorname{pred}(0) = 0 and \operatorname{pred}(S(y)) = y, using the constant zero function for the base and a projection function to return the recursion variable for the step.^[5] Addition provides another illustrative example, defined by recursion on the second argument: \operatorname{add}(x, 0) = x (using the projection function) and \operatorname{add}(x, S(y)) = S(\operatorname{add}(x, y)), where the step applies the successor to the recursive call. This builds the sum by successive increments, demonstrating how the schema extends basic projections and successor to arithmetic operations.^[5] While the primitive recursion schema, alongside basic functions and composition, exhausts the class of primitive recursive functions, it inherently limits expressiveness by excluding the minimization operator \mu, which searches for the smallest input satisfying a condition. Consequently, functions like the Ackermann function, defined by nested recursions that outpace any fixed primitive recursive growth rate, cannot be captured within this framework.^[5] Functions arising from the primitive recursion schema are total—defined for all inputs—and computable via finite iterations, making them representable in PRA through explicit terms derived from the system's recursion axioms. A proof sketch of totality proceeds by induction on the recursion parameter y: the base case f(0, \mathbf{x}) = g(\mathbf{x}) holds by assumption on g's totality; assuming totality up to y, the step f(y+1, \mathbf{x}) = h(y, f(y, \mathbf{x}), \mathbf{x}) follows since h is total and the recursive value is defined. In PRA, this ensures definability without requiring full induction or quantifiers, as the recursion unfolds explicitly.^[6]

Properties

Conservation and interpretability

Primitive recursive arithmetic (PRA) exhibits significant conservation properties relative to stronger arithmetical systems, particularly in its handling of certain classes of sentences. A key result is that PRA proves precisely the same \Pi_2^0 sentences as Peano arithmetic (PA). This conservation theorem arises from the fact that PA and the subsystem I\Sigma_1 (induction for \Sigma_1^0 formulas) share the same \Pi_2^0 theorems, while I\Sigma_1 is \Pi_2^0-conservative over PRA, meaning I\Sigma_1 \vdash \phi if and only if PRA \vdash \phi for any \Pi_2^0 sentence \phi. The conservativity of I\Sigma_1 over PRA was established by Parsons using an adaptation of Gödel's Dialectica interpretation from 1958, which provides a functional translation reducing proofs in I\Sigma_1 to primitive recursive witnesses verifiable in PRA.^[13]^[14] Formally, for a \Pi_2^0 sentence \phi (of the form \forall x \exists y \, \psi(x,y) where \psi is \Delta_0^0), if PA \vdash \phi, then PRA \vdash \exists f \, (\text{PR}(f) \land \forall x \, f(x) \text{ witnesses } \exists y \, \psi(x,y)), where PR(f) asserts that f is primitive recursive and the witnessing is bounded by primitive recursive means. This ensures that \Pi_2^0 theorems of PA, which often express totality or existence properties, reduce to finitistic, primitive recursive content without requiring full induction.^[15] Regarding interpretability, PRA fully interprets Robinson arithmetic (Q), the axiom system consisting of the basic axioms of arithmetic without induction; specifically, under the identity translation, every theorem of Q is a theorem of PRA, as PRA extends Q with axioms for primitive recursive functions and quantifier-free induction. However, PRA does not interpret full PA, since the induction schema for arbitrary formulas in PA cannot be uniformly translated into theorems of PRA, which restricts induction to \Delta_0^0 formulas. Additionally, PRA is \Sigma_1^0-sound: every \Sigma_1^0 sentence provable in PRA (of the form \exists x \, \theta(x) with \theta \Delta_0^0) holds in the standard model \mathbb{N}, reflecting the totality of its provably total functions.^[16] A notable application of these properties appears in Gentzen's 1936 consistency proof for PA, which formalizes a cut-elimination procedure on sequent calculus proofs, reducing any derivation to one without cuts. This proof establishes Con(PA) using transfinite induction along ordinals below \varepsilon_0, and the core finitary arguments—such as the termination of reduction steps—can be carried out in PRA, though the full induction requires the extension PRA + TI(<\varepsilon_0). Thus, PRA provides the foundational machinery for Gentzen's finitistic approach, underscoring its adequacy for concrete consistency arguments despite its overall weakness.^[17] As an illustrative example, PRA proves the totality of all primitive recursive functions: for any primitive recursive f, PRA \vdash \forall \vec{x} \exists y \, (f(\vec{x}) = y), since the defining equations and closure operations are directly axiomatized. In contrast, PRA does not prove totality for arbitrary recursive functions, as some (like the Ackermann function) grow faster than any primitive recursive bound and require stronger induction for their totality proofs.^[15]

Limitations and incompleteness

Primitive recursive arithmetic (PRA) is incomplete as a theory of true arithmetic, meaning there exist true statements in the language of arithmetic that cannot be proved within PRA. A prominent example is the totality of the Ackermann function, defined by the equations A(0, n) = n + 1, A(m + 1, 0) = A(m, 1), and A(m + 1, n + 1) = A(m, A(m + 1, n)), which grows faster than any primitive recursive function and thus cannot be proved total in PRA.^[5] This limitation arises because PRA only formalizes primitive recursive functions and lacks the expressive power to capture all computable total functions. The proof-theoretic ordinal of PRA, which measures its strength in terms of the ordinals it can prove well-founded, is \omega^\omega. This result, establishing an upper bound via interpretations in extended systems using functions recursive below \omega^\omega, shows that PRA is significantly weaker than Peano arithmetic (PA), whose proof-theoretic ordinal is \varepsilon_0.^[18] Consequently, PRA cannot prove well-foundedness principles up to higher ordinals that PA can handle, such as those required for certain termination proofs. Gödel's first incompleteness theorem applies to PRA: assuming PRA is consistent, there exists a sentence in its language that is true but unprovable in PRA, such as a suitable Gödel sentence encoding its own unprovability.^[19] The second incompleteness theorem also holds, implying that PRA cannot prove its own consistency if it is consistent. A key structural limitation of PRA stems from its induction schema, which is restricted to quantifier-free formulas, preventing proofs of induction for non-primitive recursive predicates, such as those defined via minimization operators. For example, while PRA can prove simple existential statements like \forall x \exists y (y = S(x)) using its basic axioms and limited induction, it fails to prove the termination of more complex sequences, such as Goodstein sequences, which require transfinite induction up to \varepsilon_0 and are thus unprovable even in the stronger PA.

Applications

In proof theory

Primitive recursive arithmetic (PRA) serves as a foundational system in Hilbert's program, providing a finitistic framework for establishing the consistency of stronger arithmetical theories without relying on impredicative methods. Hilbert envisioned consistency proofs that remain within the bounds of concrete, finite reasoning, and PRA formalizes this by restricting induction to atomic formulas and incorporating defining equations for primitive recursive functions, ensuring all proofs are intuitively evident and avoid infinite sets or higher-order concepts. This aligns with Hilbert's emphasis on contentual mathematics, where PRA acts as the base for relative consistency proofs of systems like Peano arithmetic (PA), demonstrating that if PA is inconsistent, then so is PRA—a contradiction given PRA's evident consistency.^[20] A key contribution to this program is Gödel's Dialectica interpretation, which embeds classical PA into a quantifier-free theory of primitive recursive functionals of finite type, augmented with choice principles, yielding a conservation result for \Pi_2^0 sentences over PRA. Developed in 1958, this functional interpretation translates proofs in PA to constructive counterparts in the target theory, showing that PA and its intuitionistic counterpart with Markov's principle are both conservative over PRA for \Pi_2^0 statements, thereby confirming that PA introduces no new finitistically provable truths beyond those in PRA. This method preserves the finitistic spirit of Hilbert's program by extracting primitive recursive bounds from classical proofs, without invoking impredicativity.^[15]^[13] In ordinal analysis, PRA's proof-theoretic ordinal is \omega^\omega, which measures the system's strength by the largest ordinal for which it validates transfinite induction, enabling cut-elimination theorems up to that level. This ordinal indicates that PRA can formalize proofs involving nested recursions up to the growth rate of the Ackermann function, but not beyond, limiting its capacity for higher transfinite inductions. Extensions such as PRA augmented with transfinite induction along ordinals below \omega^\omega allow for analyzing stronger fragments, such as those incorporating limited comprehension principles, while remaining within finitistic bounds.^[18]^[21] Feferman's work in the 1960s on subsystems of arithmetic further elucidates PRA's role, demonstrating that it bounds primitive recursive analysis by providing a finitary base for predicative reductions of systems like \Sigma_1^0-induction arithmetic. In particular, Feferman showed that predicative fragments, such as those avoiding impredicative comprehension up to \Gamma_0, reduce to PRA in strength, conserving \Pi_1^2 formulas and establishing PRA as sufficient for much of elementary number theory without transcending primitive recursive methods. This analysis highlights PRA's adequacy for foundational inquiries into arithmetic subsystems.^[22]^[23] PRA finds applications in proof theory for analyzing fragments of arithmetic, such as proving the consistency of extensions like PRA augmented with the \omega-rule for atomic formulas, which formalizes finitary approximations to transfinite induction. This rule allows deriving universal quantifications from infinitely many instances, and PRA's finitistic machinery suffices to show such extensions remain consistent, aiding in the study of proof strength hierarchies without exceeding primitive recursive bounds. These results underscore PRA's utility in dissecting the logical structure of arithmetical theories.^[21]^[24]

In reverse mathematics

In reverse mathematics, primitive recursive arithmetic (PRA) provides a foundational framework for assessing the axiomatic strength required to prove ordinary mathematical theorems, particularly through its second-order extension known as PRA². This system, introduced as an analogy to PRA in the second-order setting, formalizes recursive comprehension axiom for Δ⁰₁ formulas and Σ⁰₁ induction, enabling the analysis of theorems in countable combinatorics and algebra below the standard base system RCA₀. Over PRA², many classical results that are equivalent to RCA₀ over the empty base theory become equivalent to weaker principles, such as bounded choice or primitive recursive versions of König's lemma.^[25] PRA itself aligns closely with the first-order subsystem IΣ₁ of Peano arithmetic, where the provably total functions are precisely the primitive recursive ones, and PRA extends IΣ₁ conservatively for Π₂ sentences while incorporating full primitive recursion schemas. In the context of Stephen Simpson's subsystems of second-order arithmetic, PRA captures the inductive strength for Σ⁰₁ formulas, allowing proofs of basic Ramsey theorems, such as RT¹₂ (Ramsey's theorem for singletons with two colors), when restricted to primitive recursive colorings. This correspondence highlights PRA's role in interpreting recursive comprehension principles, where sets are formed via primitive recursive definitions rather than full Σ⁰₁ comprehension as in RCA₀.^[10]^[26] Specific theorems in analysis, such as the Bolzano-Weierstrass theorem, can be reverse-engineered over PRA to require only primitive recursive uniformity in the choice of subsequences, ensuring convergence for bounded sequences defined by primitive recursive moduli. In applications to theorem classification, PRA suffices to formalize countable choice principles in the arithmetic hierarchy (AC_ω^N), enabling selections from countable families of natural numbers via primitive recursive functions, but it falls short of supporting full arithmetic comprehension (ACA₀), which demands existential quantification over sets.^[27] A notable example is the Paris-Harrington theorem, a strengthened finite form of Ramsey's theorem, which Kirby and Paris showed is true but unprovable in Peano arithmetic; since PRA is a weaker subsystem lacking the full induction needed for such combinatorial statements, the theorem exceeds PRA's strength yet remains provable in stronger reverse mathematics subsystems like ACA₀.^[28]

References

[1]
[PDF] Weak theories of nonstandard arithmetic and analysis
Primitive recursive arithmetic is an axiomatic theory, with. • defining equations for the primitive recursive functions. • quantifier-free induction. PRA can ...
[2]
[PDF] Proof Theory and Proof Mining II: Formal Theories of Analysis
IΣ1 is the restriction of PA with induction for only Σ1 formulas. This theory suffices to define the primitive recursive functions, and hence interpret PRA.
[3]
[PDF] Comparing IΣ1 and PRA - Joost Joosten
This condition is used to give a model-theoretic proof of Parsons' theorem, that is, IΣ1 is Π2-conservative over PRA. ... Primitive recursive arithmetic, PRA for ...
[4]
Recursive Functions - Stanford Encyclopedia of Philosophy
Apr 23, 2020 · It is thus not difficult to discern in Skolem (1923) the kernel of the system we now know as Primitive Recursive Arithmetic (as later ...Historical Background · The Early History of Recursive... · The Origins of Primitive...
[5]
(PDF) Primitive Recursive Arithmetic and Its Role in the Foundations ...
Jan 7, 2016 · We discuss both the historical roots of Skolem's primitive recursive arithmetic, its essential role in the foundations of arithmetic, ...
[6]
[PDF] Primitive recursive reverse mathematics.
The finitist's first-order system PRA. 29. Definition 2.1. The induction axiom for Σn-formulae, IΣn, is the following schema of axioms.
[7]
[PDF] A Hierarchy of Ramified Theories Below Primitive Recursive Arithmetic
Define a structure M with signature the non-logical symbols of EA(I;O). Allow it to have a domain consisting of an infinite set |O| intended to interpret output ...
[8]
[PDF] First- and Second-Order Models of Recursive Arithmetics - arXiv
in our reformulation of primitive recursive arithmetic PRA and the two above weaker ... The first-order language ... mula in L2 with no free first-order variables, ...
[9]
[PDF] First-Order Proof Theory of Arithmetic - UCSD Math
A predicate is primitive recursive if its characteristic function is primitive recur- sive. Page 19. Proof Theory of Arithmetic. 97. Theorem. IΣ1 can Σ1 ...Missing: PRA | Show results with:PRA
[10]
[PDF] Lecture 4: The Primitive Recursive Functions - Michael Beeson's
(ii) The successor function f(x) = x/, the next integer after x, is primitive recursive. (iii) The projection function In,i(x1,...,xn) = xi is primitive.
[11]
[PDF] 1 Primitive Recursive Functions
f(x,0) = 0 f(x, y +1) = f(x, y) + x. Now that we have multiplication is primitive recursive, we use it to define powers. Example 1.5 f(x, y) = xy is ...
[12]
[PDF] Gödel's Dialectica interpretation and its two-way stretch* - Mathematics
Oct 6, 1997 · IR of PA are both conservative over PRA (Primitive Recursive Arithmetic) for Π. ◦. 2 statements, and hence have exactly the primitive ...Missing: Π⁰₂ | Show results with:Π⁰₂
[13]
[PDF] Two Proofs of Parsons' Theorem
Jan 19, 2004 · In many accounts Herbrand's theorem plays a central role in providing primitive recursive Skolem functions for Π2-statements provable in IΣ1. ( ...
[14]
[PDF] Gödel's Functional (“Dialectica”) Interpretation - andrew.cmu.ed
The Dialectica interpretation reduces HA to a theory T which axiomatizes a class of functionals that Gödel called the “primitive recursive functionals of finite.Missing: Π⁰₂ | Show results with:Π⁰₂
[15]
[PDF] Arithmetical classification of the set of all provably recursive functions
A theory. T is Σ1-sound if all Σ1-sentences provable in T hold in N. For the rest of the paper a theory means a recursively axiomatizable Σ1-sound theory ...
[16]
[PDF] The Consistency of Arithmetic - Timothy Y. Chow
The fact that PRA plus Theorem 2 implies that PA is consistent is only implicit and not explicit in Gentzen's original proof. I have chosen this way of ...
[17]
[PDF] Ordinal analysis without proofs - andrew.cmu.ed
Ordinal analysis without proofs focuses on the semantic content of theories, rather than the syntactic structure of proofs, and is finitary.<|control11|><|separator|>
[18]
Gödel's Incompleteness Theorems
Nov 11, 2013 · Gödel's two incompleteness theorems are among the most important results in modern logic, and have deep implications for various issues.
[19]
Hilbert's Program - Stanford Encyclopedia of Philosophy
Jul 31, 2003 · It calls for a formalization of all of mathematics in axiomatic form, together with a proof that this axiomatization of mathematics is consistent.Historical development of... · Hilbert's Program and Gödel's...
[20]
Proof Theory - Stanford Encyclopedia of Philosophy
Aug 13, 2018 · Gentzen's consistency proof for PA employs a reduction procedure R on proofs ... consistency proof à la Gentzen the means of PRA are exceeded.Development of · Appendix D · Provably computable functions<|control11|><|separator|>
[21]
[PDF] WHAT RESTS ON WHAT? THE PROOF-THEORETIC ANALYSIS OF ...
The language of PRA (Primitive Recursive Arithmetic) is just the quantifier-free part of. L0. In place of IA it uses an Induction Rule: IR φ(0), φ(x) → φ(x. ).
[22]
[PDF] Predicative foundations of arithmetic - Mathematics
Question 2: What is a nice axiomatization of a subsystem of EFSC (i) in which categoricity is provable, and (ii) which is equivalent in strength to PRA?
[23]
[PDF] Hilbert's Program and The Omega-Rule - Carnegie Mellon University
If we turn it into a first order theory by adding the first order logic we get a conservative extension of (PRA), usually denoted¹ by (QF - IA). Since there is ...
[24]
[2210.13080] Primitive recursive reverse mathematics - arXiv
Oct 24, 2022 · Abstract:We use a second-order analogy \mathsf{PRA}^2 of \mathsf{PRA} to investigate the proof-theoretic strength of theorems in countable ...Missing: arithmetic | Show results with:arithmetic
[25]
[PDF] Subsystems of Second Order Arithmetic - Stephen Simpson
Feb 7, 2006 · This book will be largely concerned with certain specific subsystems of second order arithmetic and the formalization of ordinary mathematics.
[26]
ON ROBUST THEOREMS DUE TO BOLZANO, WEIERSTRASS ...
Oct 3, 2022 · We obtain two new and long series of equivalences based on theorems due to Bolzano, Weierstrass, Jordan, and Cantor; these equivalences are extremely robust.
[27]
[PDF] A Mathematical Incompleteness in Peano Arithmetic
The incompleteness is that a theorem, a simple extension of the Finite Ramsey Theorem, is true but not provable in Peano arithmetic.