Strictly primitive recursive realizability. II: Completeness with respect to iterated reflection and a primitive recursive \(\omega\)-rule (Q5937826)

In the paper the notion of strictly primitive recursive realizability, introduced by the author in Part I [J. Symb. Log. 59, 1210-1227 (1994; Zbl 0816.03029)] is further investigated. The realizable prenex sentences, which coincide with primitive recursive truths of classical arithmetic, are characterized as precisely those provable in transfinite progressions \(\{ \text{PRA}(b): b \in \underline{O} \}\) over an appropriate fragment of intuitionistic arithmetic. A semiformal system closed under a primitive recursively restricted \(\omega\)-rule is described and proved equivalent to the transfinite progressions with respect to the prenex sentences.