Normal derivability and first-order arithmetic.
Piero Tosi · Notre Dame Journal of Formal Logic · 1980
Jervell [3] proved a normal form for derivations in a first-order formal system of arithmetic (say HA, Heyting's arithmetic) in the following way: from every formal derivation in HA a possibly infinite structure is generated (included in the relations that defines the structure is some form of the ω-rule) and shown to be well founded.From the properties of such infinite structures, one goes back to HA and proves a normal form.From such a normal form many proof theoretical applications relative to HA can be given, among them consistency.Two remarks can be made.First, the normal form for HA is not provable in a complete sense; hence the significance given to the normalization theorem by Prawitz ([8], III,2), (the operational interpretation of the logical constants), is weakened in the case of HA.Second, the proof theoretical applications relative to HA do not need normal form for HA, in the sense that they are already possible from the normal form for the induced infinite derivations.Moreover, that something is lost in going back to the normal form of HA can be deduced from the proof of the uniform reflection principle for HA, which is possible by the normal form of the infinite derivations, but not possible by Jervell's normal form.In the present work we will follow a different way.We will start from the same HA (Section 1), and generate infinite derivations (also by some form of the ω-rule); but, at this point, we do not aim to establish a normal form for HA.Instead, we will study the infinite derivations as a sui generis infinitary system, which we call ω-HA (Section 2).We will establish the normal form for co-HA (Section 5) and, after that, go back to HA for applications (Sections 6 and 7).The separate treatment of ω-HA is simply a matter of convenience, to make clear the object to be studied: it is not, properly speaking, a system of independent interest.Section 3 is the step required for extending to HA the proof theoretical properties of ω-HA.Section 4 is given because, in proving theorems, we find it preferable to make use of an assignment of ordinals to derivations instead of simply using bar induction.In fact, in this way we have a sharper measure for the