Completeness of the primitive recursive ω-rule

被引:0
|
作者
Frittaion, Emanuele [1 ]
机构
[1] Univ Leeds, Sch Math, Leeds, W Yorkshire, England
关键词
Shoenfield's completeness theorem; omega-rule; Primitive recursion theorem; Kleene's O; Pi(1)(1) completeness; PROGRESSIONS;
D O I
10.1007/s00153-020-00716-9
中图分类号
O1 [数学];
学科分类号
0701 ; 070101 ;
摘要
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 Pi(1)(1) complete. The same Pi(1)(1) completeness results apply to codes of cut free omega-proofs.
引用
收藏
页码:715 / 731
页数:17
相关论文
共 50 条
  • [41] Punctual Structures and Primitive Recursive Reducibility
    Kalimullin, I. Sh
    LOBACHEVSKII JOURNAL OF MATHEMATICS, 2022, 43 (03) : 582 - 586
  • [42] Deciding DPDA equivalence is primitive recursive
    Stirling, C
    AUTOMATA, LANGUAGES AND PROGRAMMING, 2002, 2380 : 821 - 832
  • [43] DARBOUX PROPERTY AND PRIMITIVE RECURSIVE FUNCTIONS
    CALUDE, C
    REVUE ROUMAINE DE MATHEMATIQUES PURES ET APPLIQUEES, 1981, 26 (09): : 1187 - 1192
  • [44] A Class of Reversible Primitive Recursive Functions
    Paolini, Luca
    Piccolo, Mauro
    Roversi, Luca
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2016, 322 : 227 - 242
  • [45] PRIMITIVE RECURSIVE FUNCTIONALS WITH DEPENDENT TYPES
    NELSON, N
    LECTURE NOTES IN COMPUTER SCIENCE, 1992, 598 : 125 - 143
  • [46] HIERARCHY OF PRIMITIVE RECURSIVE SEQUENCE FUNCTIONS
    FACHINI, E
    MAGGIOLOSCHETTINI, A
    RAIRO-INFORMATIQUE THEORIQUE-THEORETICAL COMPUTER SCIENCE, 1979, 13 (01): : 49 - 67
  • [47] PRIMITIVE RECURSIVE ARITHMETIC WITHOUT INDUCTION
    FRIEDMAN, H
    NOTICES OF THE AMERICAN MATHEMATICAL SOCIETY, 1974, 21 (07): : A595 - A596
  • [48] The Speedup Theorem in a Primitive Recursive Framework
    Asperti, Andrea
    CPP'15: PROCEEDINGS OF THE 2015 ACM CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2015, : 175 - 182
  • [49] Primitive Recursive Dependent Type Theory
    von Branitz, Johannes Schipp
    Buchholtz, Ulrik
    PROCEEDINGS OF THE 39TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, LICS 2024, 2024,
  • [50] PRIMITIVE RECURSIVE WORD-FUNCTIONS
    HENKE, FWV
    INDERMARK, K
    ROSE, G
    WEIHRAUCH, K
    COMPUTING, 1975, 15 (03) : 217 - 234