nLab primitive recursive arithmetic







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 06:43:20. See the history of this page for a list of all contributions to it.