zbMATH — the first resource for mathematics

Theories very close to PA where Kreisel’s conjecture is false. (English) Zbl 1117.03065
Kreisel’s conjecture (KC for short) asserts that, given a universal sentence \(\forall xA(x)\) of first-order arithmetic PA, if there exists a number \(k\in \omega\) such that for each \(n\in \omega\) there exists a formal proof in PA of \(A(\bar{n})\) in at most \(k\) steps, then there exists a formal proof in PA of \(\forall xA(x)\).
After reviewing some positive results on KC (due to Parikh, Myatake, Baaz, Pudlák, Krajiček), the author recalls in §1 an observation on the negative side of KC which can be obtained from previous work of Yukami and hinges upon the Matyasevich theorem: if \(T\) is consistent, recursively axiomatized, contains the language of PA and extends PA, and is such that there exists a finite bound on the number of steps required for formally verifying each single instance of the commutativity law for multiplication, \(\bar{n}\cdot \bar{m}=\bar{m}\cdot \bar{n}\), then \(T\) does not satisfy KC.
He then provides four rather natural counterexamples to KC: (1) the extension of PA, PA\((-)\), with a function symbol for subtraction and its corresponding defining axiom; (2) a suitable version of the theory of integers \(Z\); (3) the system PA\((q)\) obtained by adding to PA a function symbol \(q\) of arity \(\geq 1\); (4) the theory PA\((N)\) which expands PA with a unary predicate symbol for the property \(N\) of being a natural number and whose axioms relativize Peano axioms to \(N\). The proofs are detailed in §§2–5.
This interesting paper is supplemented by a discussion of possible refinements of KC (§6) and by a final discussion (in §7) of the truth of KC for PA with three open problems.

03F30 First-order arithmetic and fragments
03F20 Complexity of proofs
Full Text: DOI
[1] Annals of the Japan Association for Philosophy and Science 6 pp 195–205– (1984)
[2] Tsukuba Journal of Mathematics 7 pp 69–73– (1978)
[3] Transactions of the American Mathematical Society 177 pp 29–36– (1973)
[4] Arithmetic, proof theory, and computation complexity pp 30–60– (1993)
[5] Archive for Mathematical Logic 27 pp 69–84– (1988)
[6] One hundred and two problems in mathematical logic 40 pp 113–129– (1975)
[7] Tsukuba Journal of Mathematics 4 pp 115–125– (1980)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.