nLab primitive recursive arithmetic





The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms




In proof theory, primitive recursive arithmetic, or PRA, is a finitist, quantifier-free formalization of the natural numbers.

PRA can express arithmetic propositions involving natural numbers and any primitive recursive function, including the operations of addition, multiplication, and exponentiation.

As a Skolem theory

Let TT be a Lawvere theory, i.e., a category with finite products TT equipped with a bijective-on-objects product-preserving functor X:Fin opTX: Fin^{op} \to T where FinFin is the category of finite cardinals and functions. Recall that a Skolem theory? is a Lawvere theory (T,X:Fin opT)(T, X: Fin^{op} \to T) in which N=X(1)N = X(1) carries a structure of parametrized natural numbers object in TT.

Abstractly, PRA can be described as the initial Skolem theory. Precise statements to this effect are difficult to pin down in the literature. (More later)

Last revised on April 24, 2020 at 10:43:20. See the history of this page for a list of all contributions to it.