ON DEFINITIONAL TRANSFORMATIONS TO NORMAL FORM FOR INTUITIONISTIC LOGIC

Abstract

In this paper, we examine different definitional transformations into normal form for intuitionistic logic. In contrast to the classical case, “intuitionistic clauses” may contain implications and quantifiers. Usually, such definitional transformations introduce labels defining subfor-mulae. An obvious optimization is the use of implications instead of equivalences whenever possible, which can reduce the size of the resulting normal form. We compare the optimized transformation with the unoptimized transformation with respect to the shortest cut-free LJ-derivation of the resulting normal forms. The comparison is based on a sequence (H_k)_k∈N of formulae for which the following hold: (i) there exist cut-free LJ-proofs of the unoptimized normal form of H_k with length double-exponential in k, and (ii) any cut-free LJ-proof of the optimized normal form of H_k has length non-elementary in k. The reason for the different behaviour is the simulation of analytic cuts by the unoptimized translation, which is not possible when the optimization is applied.