Journal
ARCHIVE FOR MATHEMATICAL LOGIC
Volume 55, Issue 3-4, Pages 461-473Publisher
SPRINGER HEIDELBERG
DOI: 10.1007/s00153-016-0474-y
Keywords
Sequent calculus; Glivenko classes; Conservativity of classical over intuitionistic theories; Predicate logic with equality and functions; Proof analysis
Categories
Ask authors/readers for more resources
In 1968, Orevkov presented proofs of conservativity of classical over intuitionistic and minimal predicate logic with equality for seven classes of sequents, what are known as Glivenko classes. The proofs of these results, important in the literature on the constructive content of classical theories, have remained somehow cryptic. In this paper, direct proofs for more general extensions are given for each class by exploiting the structural properties of G3 sequent calculi; for five of the seven classes the results are strengthened to height-preserving statements, and it is further shown that the constructive and minimal proofs are identical in structure to the classical proof from which they are obtained.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available