Completeness of the primitive recursive $\omega$-rule

Emanuele Frittaion

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$-rul…