On the Complexity of Translations from Classical to Intuitionistic Proofs.

We investigate various translations from classical to intuitionistic proofs in Gentzen calculus and analyze their computational complexity. In particular we investigate the Kolmogorov translation, (a new form of) the extended Glivenko translation and the optimized Kolmogorov translation. While the Kolmogorov translation maps cut-free proofs into cut-free proofs this does not hold for the extended Glivenko translation. For analyzing the complexity of translating cutfree proofs into cut-free proofs we use the method CERES (cut-elimination by resolution), a global proof analysis method. We establish an elementary bound on the complexity of translating cut-free classical proofs with only weak quantifiers into cut-free intuitionistic proofs via the Glivenko translation. We even prove a more general result for classical cut-free proofs of sequents of the form A(1),..., A(n) proves with only weak quantifiers, from which the complexity of the extended Glivenko translation for the weak quantifier fragment easily follows.