Provably recursive functions in fragments of Peano arithmetic (Q1073791)

From MaRDI portal





scientific article; zbMATH DE number 3946123
Language Label Description Also known as
English
Provably recursive functions in fragments of Peano arithmetic
scientific article; zbMATH DE number 3946123

    Statements

    Provably recursive functions in fragments of Peano arithmetic (English)
    0 references
    0 references
    0 references
    1986
    0 references
    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}\).
    0 references
    ordinal recursive functions
    0 references
    rapidly growing functions
    0 references
    Paris-Harrington theorem
    0 references

    Identifiers