Minimal from classical proofs
type: Item
instance of: scholarly article
title: Minimal from classical proofs
zbMATH Open document ID: 1263.03053
author: Christoph Senjak
author: Helmut Schwichtenberg
published in: Annals of Pure and Applied Logic
publication date: 2013-04-15T00:00:00Z
review text: 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)].
reviewed by: Gilda Ferreira
Mathematics Subject Classification ID: 03F03
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03F07
zbMATH DE Number: 6154070
zbMATH Keywords: minimal logic
zbMATH Keywords: stability axioms
zbMATH Keywords: Glivenko-style theorems
zbMATH Keywords: Orevkov
zbMATH Keywords: normal derivations
zbMATH Keywords: intuitionistic logic
zbMATH Keywords: natural deduction
MaRDI profile type: Publication
full work available at URL: j.apal.2012.05.009
OpenAlex ID: W2010146589
DOI: 10.1016/J.APAL.2012.05.009
Recommended article: Q4202954
Recommended article: Minimum classical extensions of constructive theories
Recommended article: Q4250564
Recommended article: Short proofs of classical theorems
Recommended article: Q4781214
Recommended article: Q4725777
Recommended article: Artificial Intelligence and Symbolic Computation
Recommended article: Q4855730
Recommended article: Uniform short proofs for classical theorems
Recommended article: A Minimal Proof of a Result of Hardy
description: scientific article; zbMATH DE number 6154070