Skip to main content
SpringerLink
Log in

Completeness of the primitive recursive \(\omega \)-rule

  • Published:
Archive for Mathematical Logic Aims and scope Submit manuscript

Abstract

Shoenfield’s completeness theorem (1959) states that every true first order arithmetical sentence has a recursive \(\omega \)-proof encodable by using recursive applications of the \(\omega \)-rule. For a suitable encoding of Gentzen style \(\omega \)-proofs, we show that Shoenfield’s completeness theorem applies to cut free \(\omega \)-proofs encodable by using primitive recursive applications of the \(\omega \)-rule. We also show that the set of codes of \(\omega \)-proofs, whether it is based on recursive or primitive recursive applications of the \(\omega \)-rule, is \(\varPi ^1_1\) complete. The same \(\varPi ^1_1\) completeness results apply to codes of cut free \(\omega \)-proofs.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Notes

  1. Kleene in [6, p. 75] states the primitive recursion theorem with respect to a standard numbering \(\{[e]:e\in \omega \}\) of all primitive recursive functions. That is, for every primitive recursive function \(g(x,x_1,\ldots ,x_n)\) there is an index e such that for all \(x_1,\ldots ,x_n\)

    $$\begin{aligned}{}[e](x_1,\ldots ,x_n)=g(e,x_1,\ldots ,x_n). \end{aligned}$$

  2. Cf. Feferman [2, Definition 5.7, p. 302], where codes are based on a Hilbert style presentation of first order \(\omega \)-arithmetic.

  3. Strictly speaking, the Schütte tree consists of ordered sequents. Clearly, one can primitive recursively in the function \(\psi (\varGamma )\) forget the order and hence obtain a primitive recursive tree of (unordered) sequents.

  4. Cf. Feferman [2, Theorem 5.13]. Every true sentence is provable in some \(\textsf {PA}_d\) with \(d\in {\mathcal {O}}\) and \(|d|<\omega ^{\omega ^\omega }\). Fenstad [3] improves Feferman’s bound to \(\omega ^\omega \).

  5. Note by contrast that the intuitionistic case is another matter altogether. In fact, primitive recursive cut free \(\omega \)-proofs based on Gentzen two-sided intuitionistic sequent calculus (\({\textsf {LJ}}\)) are not even complete for Heyting arithmetic \({\textsf {HA}}\). This is well known (cf. [7]). In fact, consider a provably recursive function of \({\textsf {HA}}\) (equivalently \(\textsf {PA}\)) which is not primitive recursive, and note that from any primitive recursive intuitionistic cut free \(\omega \)-proof of \(\forall x\exists yA(x,y)\) one can extract a primitive recursive function f such that \(\forall xA(x,f(x))\) is true. In particular, cut elimination does not hold unless we include vacuous rules such as, e.g., the repetition rule.

References

  1. Buchholz, W.: Notation systems for infinitary derivations. Arch. Math. Log. 30(5), 277–296 (1991)

    Article  MathSciNet  Google Scholar 

  2. Feferman, S.: Transfinite recursive progressions of axiomatic theories. J. Symb. Log. 27(3), 259–316 (1962)

    Article  MathSciNet  Google Scholar 

  3. Fenstad, J.E.: On the completeness of some transfinite recursive progressions of axiomatic theories. J. Symb. Log. 33(1), 69–76 (1968)

    Article  MathSciNet  Google Scholar 

  4. Franzén, T.: Transfinite progressions: a second look at completeness. Bull. Symb. Log. 10(3), 367–389 (2004)

    Article  MathSciNet  Google Scholar 

  5. Girard, J.Y.: Proof theory and logical complexity. In: Studies in Proof Theory. Monographs, vol. 1, Bibliopolis, Naples (1987)

  6. Kleene, S.C.: Extension of an effectively generated class of functions by enumeration. In: Colloquium Mathematicum, vol. 6, pp. 67–78. Instytut Matematyczny Polskiej Akademii Nauk (1958)

  7. Lopez-Escobar, E.: On an extremely restricted \(\omega \)-rule. Fundam. Math. 2(90), 159–172 (1976)

    Article  MathSciNet  Google Scholar 

  8. Mints, G.: Finite investigations of transfinite derivations. J. Sov. Math. 10(4), 548–596 (1978)

    Article  Google Scholar 

  9. Schütte, K.: Beweistheoretische erfassung der unendlichen induktion in der zahlentheorie. Math. Ann. 122(5), 369–389 (1950)

    Article  Google Scholar 

  10. Schütte, K.: Proof theory. Springer, Berlin (1977). Translated from the revised German edition by J. N. Crossley, Grundlehren der Mathematischen Wissenschaften, Band 225

  11. Shoenfield, J.R.: On a restricted \(\omega \)-rule. Bull. Acad. Polon. Sci. Sér. Sci. Math. Astr. Phys. 7, 405–407 (1959). (unbound insert)

    MathSciNet  MATH  Google Scholar 

  12. Sundholm, B.G.: Proof theory: a survey of the \(\omega \)-rule. Ph.D. thesis, University of Oxford (1983)

Download references

Author information

Authors and Affiliations

  1. School of Mathematics, University of Leeds, Leeds, UK

    Emanuele Frittaion

Authors
  1. Emanuele Frittaion
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Emanuele Frittaion.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

The author was supported by John Templeton Foundation (“A new dawn of Intuitionism: Mathematical and Philosophical advances”, Grant ID 60842).

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Frittaion, E. Completeness of the primitive recursive \(\omega \)-rule. Arch. Math. Logic 59, 715–731 (2020). https://doi.org/10.1007/s00153-020-00716-9

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00153-020-00716-9

Keywords

Mathematics Subject Classification

Search

Navigation