Properly Displayable Logics, Displayable Logics and Strong Cut-Elimination
In the present chapter it is shown that every displayable logic enjoys strong cut-elimination. This result sharpens Belnap’s very general cut-elimination theorem for Display Logic . Moreover, Kracht’s characterization of the properly displayable modal and tense logics is presented, together with complete and cut-free display sequent systems for various axiomatic extensions of the basic intensional systems K and Kt.
Unable to display preview. Download preview PDF.