<p>The <a href="http://www.cs.utexas.edu/users/moore/acl2/v7-1/acl2-doc.html" rel="nofollow">ACL2</a> theorem prover seems quite close to what you want, though it is hard to know exactly what the strength of the system is.</p>

<p>From the logical description <a href="http://www.cs.utexas.edu/users/moore/publications/km97a.pdf" rel="nofollow">here</a> it looks like the base is a quantifier-free equational logic with induction principles, which include principles allowing the definition of PR functions.</p>

<p>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.</p>

<p>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).</p>

CC BY-SA 3.0
2015-10-08T17:17:08.230Z
2015-10-08T17:17:08.230Z
cody
<p>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.</p>

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

<computability><proof-assistants>
Proof software for Primitive Recursive Arithmetic
Rex Butler
# Proof software for Primitive Recursive Arithmetic

(Asked by: username_0 on 2015-10-08)

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?

**Tags:** computability, proof-assistants

---

## 1 answers

### Answer by username_1 on 2015-10-08. Score: 2 | Accepted answer

The [ACL2](http://www.cs.utexas.edu/users/moore/acl2/v7-1/acl2-doc.html) 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](http://www.cs.utexas.edu/users/moore/publications/km97a.pdf) 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).


---

