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 条