Provably recursive functions in fragments of Peano arithmetic
type: Item
instance of: scholarly article
title: Provably recursive functions in fragments of Peano arithmetic
zbMATH Open document ID: 0589.03037
author: Hiroakira Ono
author: Noriya Kadota
published in: Journal of the Mathematical Society of Japan
publication date: 1986-01-01T00:00:00Z
review text: Let PA be Peano's first-order arithmetic and PA* the extension of PA obtained by adding all true \(\Pi_ 1\)-formulas to PA. Moreover, let \(PA_ k\) (or \(PA^*_ k)\) be the fragment of PA (or PA*), with induction restricted to formulas having at most k nested quantifiers. A recursive function f(x) is provably recursive in \(PA^*_ k\), if \(\forall x\exists y\) T(e,x,y) is provable in \(PA^*_ k\) for some Gödel number e of f, where T represents Kleene's T-predicate. The main result of the paper is as follows: The following three conditions are equivalent: (1) f is \(\omega_ n(m)\)-ordinal recursive for some \(m<\omega\). (2) f is provably recursive in \(PA^*_ n\). (3) There exists a \(\Delta_ 1\)-formula S such that \(f(x)=\mu y S(x,y)\) and \(\forall x\exists !y\) S(x,y) is provable in \(PA_ n.\) By using the above result, the authors also get a result related to the Paris-Harrington theorem. Let PH(n) be \(\forall k\forall c\exists m\) ([k,m]\(\to_{*}(n+1)^ n_ c)\) and PH be \(\forall x PH(x)\). Let \(\sigma_{n,c}(k)=\mu m([k,m]\to_{*}(n+1)^ n_ c)\). By using the estimation of \(\sigma_{n,c}\) given by \textit{J. Ketonen} and \textit{R. Solovay} [Ann. Math., II. Ser. 113, 267-314 (1981; Zbl 0494.03027)], the following result by \textit{J. B. Paris} [Lect. Notes Math. 834, 312-337 (1980; Zbl 0448.03054)] can be obtained in a proof-theoretic way: For \(n\geq 2\), PH(n) (in some representation) is provable in \(PA_ n\), but not in \(PA_{n-1}\).
Mathematics Subject Classification ID: 03F30
Mathematics Subject Classification ID: 03D20
zbMATH DE Number: 3946123
zbMATH Keywords: ordinal recursive functions
zbMATH Keywords: rapidly growing functions
zbMATH Keywords: Paris-Harrington theorem
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.2969/jmsj/03840721
OpenAlex ID: W2023421580
DOI: 10.2969/JMSJ/03840721
description: scientific article; zbMATH DE number 3946123