Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
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?
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).
