A NORMAL-FORM FOR LOGICAL DERIVATIONS IMPLYING ONE FOR ARITHMETIC DERIVATIONS

We describe a short model-theoretic proof of an extended normal form t heorem for derivations in predicate logic which implies in PRA a norma l form theorem for the arithmetic derivations (cf. [8]). Consider the Gentzen-type formulation of predicate logic with invertible rules. A d erivation with proper variables is one where a variable b can occur in the premiss of an inference L but not below this premiss only in the case when L is (double-line arrow pointing right V) or (3 double-line arrow pointing right) and b is its eigenvariable. Free variables of su ch derivation are eigenvariables and free variables of its last sequen t. Then any sequent derivable in predicate logic has a cut-free deriva tion with proper variables where the main formula of any antecedent ru le is underivable. The proof is by a simple modification of the constr uction of a countermodel of the formula from the open branch of its ca nonical proof-search tree. It extends to intuitionistic and higher ord er systems. The proof of the corresponding normalization theorem outli ned in [8] (is more complicated and) uses the passage to the infinitar y derivations enriched by finitary derivations. The normal form after a modification to make it decidable can be considered as a realization of Gentzen's idea stated at the end of [2], that his notion of reduct ion for arithmetic can be extended to other fields of mathematics.