Contents

foundations

# Contents

## Idea

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

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.