On Constructive Fragments of Classical Logic

Abstract

In the late twenties and early thirties of the last century several results were obtained concerning relations between classical logic (CL) and intuitionistic logic. Glivenko, Kolmogorov, Gödel, Gentzen and Kuroda, this last appeared in 1950, provided well-known interpretations of classical logic into intuitionistic logic, in this way transferring constructive aspects to the fragments on which these interpretations are based. The aim of the present paper is to investigate the constructive behavior of other fragments of CL and of fragments of classical S4. We shall be mainly concerned with the fragments { ¬, ∧, ⊥, ∀ }, { ¬, ∧, ⊥, ∃ }, { → }, { ¬, ∧, ⊥, ⋄ }, and { ¬, ∧, ⊥, □ }. Our general approach will be exclusively proof-theoretical.