English

Completeness of the primitive recursive $\omega$-rule

Logic 2021-10-05 v1

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 Π11\Pi^1_1 complete. The same Π11\Pi^1_1 completeness results apply to codes of cut free ω\omega-proofs.

Cite

@article{arxiv.2110.01270,
  title  = {Completeness of the primitive recursive $\omega$-rule},
  author = {Emanuele Frittaion},
  journal= {arXiv preprint arXiv:2110.01270},
  year   = {2021}
}
R2 v1 2026-06-24T06:35:55.136Z