A NEW COMPUTATION OF THE Σ-ORDINAL OF KPω
Fernando A.F. Ferreira · Journal of Symbolic Logic · 2014
Abstract We define a functional interpretation of KP ω using Howard’s primitive recursive tree functionals of finite type and associated terms. We prove that the Σ-ordinal of KP ω is the least ordinal not given by a closed term of the ground type of the trees (the Bachmann-Howard ordinal). We also extend KP ω to a second-order theory with Δ 1-comprehension and strict- ${\rm{\Pi }}_1^1$ reflection and show that the Σ-ordinal of this theory is still the Bachmann-Howard ordinal. It is also argued that the second-order theory is Σ1-conservative over KPω.