A Note on the Complexity of Classical and Intuitionistic Proofs
Matthias Baaz, Alexander Leitsch, Giselle Reis · 2015
We show an effective cut-free variant of Glivenko's theorem extended to formulas with weak quantifiers: "There is an elementary function f such that if φ is a cut-free LK proof of ⊢ A with symbol complexity ≤ c, then there exists a cut-free LJ proof of ⊢ ⊯ ⊯ A with symbol complexity ≤ f(c)". This follows from the more general result: "There is an elementary function f such that if φ is a cut-free LK proof of A ⊢ with symbol complexity ≤ c, then there exists a cut-free LJ proof of A ⊢ with symbol complexity ≤ f(c)". The result is proved using a suitable variant of cut-elimination by resolution (CERES) and subsumption.