Nonconstructive computational mathematics (Q1272604)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Nonconstructive computational mathematics |
scientific article |
Statements
Nonconstructive computational mathematics (English)
0 references
18 October 1999
0 references
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.
0 references
survey
0 references
proof-theoretic strength of \(\text{PRA}^*\)
0 references
primitive recursive arithmetic
0 references
minimum operator
0 references
Boyer-Moore theorem prover NQTHM
0 references