A normal form for logical derivations implying one for arithmetic derivations (Q2367413)

The main result of this paper is a refined normal form theorem: a provable sequent has a cut-free derivation with the proper variable condition (i.e. a variable in the derivation is either an eigenvariable or occurs in the last sequent) and with the main formula restriction (i.e., no main formula of the antecedent is derivable). The author first proves the existence of such a derivation model-theoretically, and then the normalization theorem (that giving a procedure for converting a given derivation into a normal one) via an infinitary calculus. The results and methods are applied to systems of arithmetic. One result is that a derivation in arithmetic can be replaced by one that satisfies the proper variable and the constant normal condition (i.e., in each induction rule the induction term contains a variable). As a consequence, an existential statement is provable without induction, if it is provable at all. A normal form theorem of a more elaborate kind is proved; and the extendability of these results to the intuitionistic and the higher-order system is explained.