basic constructions:
strong axioms
further
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.
Let be a Lawvere theory, i.e., a category with finite products equipped with a bijective-on-objects product-preserving functor where is the category of finite cardinals and functions. Recall that a Skolem theory? is a Lawvere theory in which carries a structure of parametrized natural numbers object in .
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.