On Different Structure-preserving Translations to Normal Form

In this paper, we compare different definitional transformations into normal form with respect to the Herbrand complexity of the resulting normal forms. Usually, such definitional transformations introduce labels defining subformulae. An obvious optimization is to use implications instead of equivalences, if the subformula occurs in one polarity only, in order to reduce the length of the resulting normal form. We identify a sequence of formulaeH1,H2,..., for which the difference of the Herbrand complexity of the different translations ofHκ is bounded from below by a non-elementary function in κ. If the optimized translation is applied instead of the unoptimized one, the length of any resolution or cut-free LK-proof ofHκ is non-elementary in κ instead of exponential in κ.