A note on sequent calculi intermediate between LJ and LK (Q1115420): Difference between revisions

We consider some subsystems of Gentzen's sequent calculus LK for classical first-order logic and find that for every first-order logic intermediate between the intuitionistic and the classical one, there exists a corresponding cut-free class of sequent derivations. An immediate consequence of such a consideration is that each decidable intermediate logic has a corresponding cut-free Gentzen-type formulation. This investigation together with the sequence-conclusion approach to natural deduction systems [see the author, J. Philos. Logic 14, 359-377 (1985; Zbl 0572.03033)] make it possible to get the normalizable natural deduction formulations of intermediate logics and provide also an opportunity to treat the problem of separability of intermediate logics [see \textit{T. Hosoi}, J. Tsuda College 6, 23-38 (1974)].