Primitive Recursive Arithmetic (PRA)

Origin. Thoralf Skolem, "Begründung der elementaren Arithmetik" (1923), giving an arithmetic with no quantifiers at all. Hilbert and Bernays adopted it, and Tait ("Finitism", 1981) argued it is the exact formal counterpart of Hilbert's finitary standpoint — a claim that made PRA the benchmark against which finitistic reducibility is measured.

Models. Arithmetic with function symbols for every primitive recursive function and no quantifiers. Everything asserted is a quantifier-free equation between terms one can compute; induction is present as a rule on quantifier-free formulas, not as a schema over an unbounded domain. What survives is the arithmetic a finitist can be held to.

Formalism.

Language: 0, S, and a function symbol for each primitive recursive definition. Quantifier-free equations t = s only. No ∀, no ∃ — free variables carry the generality.

Defining schemes: f(x̄, 0) = g(x̄) f(x̄, S(y)) = h(x̄, y, f(x̄, y)) Composition and projection close the class.

Axioms: S(x) ≠ 0, S(x) = S(y) → x = y The defining equations of each function symbol.

Induction rule (not schema): φ(0) φ(x) → φ(S(x)) ───────────────────────── φ(x) for φ quantifier-free.

Strength: Σ⁰₁-conservative over PRA is the standard reducibility target. Proof-theoretic ordinal: ω^ω. PRA ⊊ IΣ₁ ⊊ PA, with IΣ₁ Π⁰₂-conservative over PRA (Parsons).

Why the benchmark: Tait: PRA is finitism, formalized. So "T is finitistically reducible" is read as "T is Π⁰₂-conservative over PRA". WKL₀ is (Friedman), which is Hilbert's programme partially vindicated.

Symbols.

Symbol	Unicode	Name	Meaning
PRA	—	Primitive recursive arithmetic	The system
S	—	Successor	The only primitive besides 0
ω^ω	U+03C9	Omega to the omega	Its proof-theoretic ordinal
IΣ₁	—	Sigma-1 induction	The fragment just above
Π⁰₂	—	Pi-0-2	The conservativity class

Metatheory. Parsons' theorem — IΣ₁ is Π⁰₂-conservative over PRA — is what makes PRA robust: the natural quantified fragment just above it proves no new computational facts, so the finitist loses nothing by refusing quantifiers. Gentzen's consistency proof for PA is a PRA proof plus transfinite induction to ε₀, which is the exact statement of what PA costs beyond finitism. Friedman's conservativity of WKL₀ over PRA extends the reduction to a large part of classical analysis.

Applies to. Hilbert's programme and its partial realizations. Reverse mathematics, where PRA is the reducibility target below RCA₀. Proof-theoretic ordinal analysis, as the base. Constructive foundations, where it is the uncontroversial floor.

Limitations. Tait's identification of PRA with finitism is a philosophical thesis, not a theorem, and it has been disputed from both sides — Kreisel thought finitism reaches further, Nelson and the ultrafinitists that it reaches less. The quantifier-free restriction is expressively awkward: statements are made by free variables and schematic rules, and anything with a ∃ must be reformulated as a function symbol before it can be said at all.