Completeness of the primitive recursive $\omega$-rule

TL;DR

This paper investigates the completeness of primitive recursive applications of the $\omega$-rule in first-order arithmetic, establishing the $\Pi^1_1$-completeness of the set of such proofs and their encodings.

Contribution

It extends Shoenfield's completeness theorem to cut-free $\omega$-proofs with primitive recursive applications and proves the $\Pi^1_1$-completeness of their encoding sets.

Findings

Shoenfield's completeness theorem applies to primitive recursive $\omega$-proofs.

The set of codes of $\omega$-proofs is $\Pi^1_1$ complete.

The $\Pi^1_1$-completeness also holds for cut free $\omega$-proofs.

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