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 -proof encodable by using recursive applications of the -rule. For a suitable encoding of Gentzen style -proofs, we show that Shoenfield's completeness theorem applies to cut free -proofs encodable by using primitive recursive applications of the -rule. We also show that the set of codes of -proofs, whether it is based on recursive or primitive recursive applications of the -rule, is complete. The same completeness results apply to codes of cut free -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}
}