No speedup for geometric theories

TL;DR

This paper demonstrates that transforming classical proofs of geometric implications into intuitionistic proofs can be done efficiently, challenging the belief that such transformations necessarily cause superexponential proof length increases.

Contribution

It provides a feasible method for converting classical proofs into intuitionistic ones for geometric theories, improving upon the traditional understanding based on cut elimination.

Findings

Transformation can be achieved in feasibly many steps

Classical and intuitionistic geometric theories are conservative over each other

Proof length does not necessarily grow superexponentially during transformation

Abstract

Geometric theories based on classical logic are conservative over their intuitionistic counterparts for geometric implications. The latter result (sometimes referred to as Barr's theorem) is squarely a consequence of Gentzen's Hauptsatz. Prima facie though, cut elimination can result in superexponentially longer proofs. In this paper it is shown that the transformation of a classical proof of a geometric implication in a geometric theory into an intuitionistic proof can be achieved in feasibly many steps.