3.9 Article

Glivenko sequent classes in the light of structural proof theory

Journal

ARCHIVE FOR MATHEMATICAL LOGIC
Volume 55, Issue 3-4, Pages 461-473

Publisher

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

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

Primary Rating

3.9
Not enough ratings

Secondary Ratings

Novelty
-
Significance
-
Scientific rigor
-
Rate this paper

Recommended

No Data Available
No Data Available