ON THE ITERATED ω‐RULE
Grzegorz Michalski · Mathematical logic quarterly · 1992
Abstract Let Γn(φ) be a formula of LPA (PA = Peano Arithmetic) meaning “there is a proof of φ from PA‐axioms, in which ω‐rule is iterated no more than n times”. We examine relations over pairs of natural numbers of the kind. (n, k) ≦H (n', k') iff PA + RFNn' (Hk') ⊩ RFNn (Hk). Where H denotes one of the hierarchies ∑ or Π and RFNn(C) is the scheme of the reflection principle for Γn restricted to formulas from the class C(Γn(φ) implies “φ is true”, for every φ ∈ C). Our main result is that. (n, k) ≦H (n', k') if n ≦ n' and k ≦ max (k', 2n' + 1).