Minimal from classical proofs (Q1946677)

The paper addresses the issue of finding proofs in minimal logic from proofs in classical logic. More precisely, the authors show that, if there exists a classical proof of \(A\) from \(\Gamma\), where \(A\) is a formula without implications and the formulas in \(\Gamma\) contain only negative occurrences of disjunction and falsity and positive occurrences of implication, then a minimal proof of \(A\) from \(\Gamma\) also exists and can be obtained from the former. Concerning related work, Orevkov in 1968 and Nadathur in 2000 proved that classical derivability, considering the above restriction on formulas, implies intuitionistic derivability. The novelty in the present paper goes beyond the improvement from intuitionistic to minimal derivations. The result is proved not using sequent calculus but considering natural deduction proofs in long normal form, viewed, by the Curry-Howard correspondence, as lambda-terms. This approach can be of interest for computational purposes. The proof itself is then based in the analysis of possible occurrences of stability axioms and a strategy to remove them. A quadratic algorithm to remove the stability axioms can be extracted from the proof. For more on constructive provability from classical provability see [\textit{V. P. Orevkov}, Proc. Steklov Inst. Math. 98, 147--173 (1968; Zbl 0208.01002); \textit{G. Nadathur}, Theor. Comput. Sci. 232, No. 1--2, 273--298 (2000; Zbl 0951.03048); \textit{V. Glivenko}, Bull. Acad. Bruxelles (5) 15, 183--188 (1929; JFM 55.0030.05); \textit{G. Mints}, J. Symb. Log. 56, No. 2, 385--424 (1991; Zbl 0747.03024)].