Nonconstructive computational mathematics (Q1272604)

This paper is in the nature of a survey, and has two aspects. The first is about the proof-theoretic strength of \(\text{PRA}^*\), primitive recursive arithmetic strengthened by application of the minimum operator at most once. The second aspect is a comparison of \(\text{PRA}^*\) and the Boyer-Moore theorem prover NQTHM. It is stated, sometimes with indications of proofs, that \(\text{PRA}^*\vdash\text{CON}(\text{PRA})\), \(\text{PA}\vdash \text{CON}(\text{PRA}^*)\), and \(\text{PRA}^*\) and PRA+ (induction up to \(\varepsilon_0\)) are of non-comparable strengths. On the comparison side, the author exhibits mathematical analogues of non-constructive EVAL\$ and V\&C\$ of NQTHM, via the Kleene \(T\)-predicate. He indicates that \(\text{PRA}^*\) and NQTHM are of the same strength. (Proving it is impossible, because NQTHM is not precisely delineated.) The author starts from basics in some aspects: computation, recursion theorems, and salient features of NQTHM are explained, and the system PRA is displayed. He also shows how to handle double recursion, the Ackermann function, and the \(\mu\)-operator in NQTHM.