Nonconstructive computational mathematics

We describe a nonconstructive extension to primitive recursive arithmetic, both abstractly and as implemented on the Boyer-Moore prover. Abstractly, this extension is obtained by adding the unbounded mu operator applied to primitive recursive functions; doing so, one can define the Ackermann function and prove the consistency of primitive recursive arithmetic. The implementation does not mention the mu operator explicitly but has the strength to define the (mu) operator through the built-in functions EVAL$ and V&C$.