ON THE ITERATED ω‐RULE

Let Γ n (φ) be a formula of L PA (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 + RFN n ' ( H k ' ) ⊩ RFN n ( H k ). Where H denotes one of the hierarchies ∑ or Π and RFN n ( 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).