Primitive Recursive Arithmetic is a critical foundational system in mathematics at large, and all the more so in areas studying constructive reasoning and/or computability such as Theoretical Computer Science.

Is there any proof software that deals with Primitive Recursive Arithmetic... or equivalent systems?


1 Answer 1


The ACL2 theorem prover seems quite close to what you want, though it is hard to know exactly what the strength of the system is.

From the logical description here it looks like the base is a quantifier-free equational logic with induction principles, which include principles allowing the definition of PR functions.

This gives exactly PRA, but in addition, the standard library defines induction up to $\varepsilon_0$, which brings the strength up to full Peano Arithmetic.

You might therefore want to work in ACL2 with a restricted version of the standard induction principle (I don't know how hard that is).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.