Search

In this note, we investigate iterations of consistency, local and uniform reflection over Heyting arithmetic. For consistency and local reflection, we recover the same results known to hold for Peano arithmetic. In the case of uniform reflection, we present a new, self-contained proof of Dragalin’s extension of Feferman’s completeness theorem, drawing on ideas from Rathjen’s novel proof of Feferman’s classical result (cf. [12]).

We consider fragments of uniform reflection for formulas in the analytic hierarchy over theories of second order arithmetic. The main result is that for any second order arithmetic theory $T_0$ extending $\mathsf {RCA}_0$ and axiomatizable by a $\Pi ^1_{k+2}$ sentence, and for any $n\geq k+1$,