FLAP Journal 2017 Journal Article
Classical and Intuitionistic Geometric Logic.
- Grigori Mints
Geometric sequents “A implies C” where all axioms A and conclusion C are universal closures of implications of positive formulas play distinguished role in several areas including category theory and (recently) logical analysis of Kant’s theory of cognition. They are known to form a Glivenko class: existence of a classical proof implies existence of an intuitionistic proof. Existing effective proofs of this fact involve superexponential blow-up, but it is not known whether such increase in size is necessary. We show that any classical proof of such a sequent can be polynomially transformed into an intuitionistic geometric proof of (classically equivalent but intuitionistically) weaker geometric sequent.