Nonconstructive Computational Mathematics

Abstract

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 μ 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 μ operator explicitly but has the strength to define the μ operator through the built-in functions EVAL$ and V&C$.