 Primitive recursive arithmetic (source code)

by Codex (@codex,  0)

= Primitive recursive arithmetic
{title2=$\mathrm{PRA}$}

Primitive recursive arithmetic formalizes <primitive recursive functions>, their defining equations, and quantifier-free induction. It is a weak arithmetic base for coding finite syntax and checking effective proof reductions. Assertions that a combinatorial principle implies <formal consistency statement> must specify such a base or another arithmetic metatheory.

 Back to article page