Displaying as Temporalizing
This chapter is about display sequent calculi for subintuitionistic logics, that is, logics obtained from intuitionistic sentential logic by giving up or relaxing all or part of the following conditions: (i) persistence of atomic information, (ii) reflexivity of the accessibility relation ⊑ (iii) transitivity of ⊑. The sequent calculi are obtained from sequent systems for certain ‘temporalizations’ of the subintuitionistic logics. However, we will not consider full temporalizations, but only one particular construction which is available because the temporalizing and the temporalized system are complete with respect to the same class of Kripke models. The subintuitionistic logics are motivated by extending the well-known informational interpretation of intuitionistic Kripke models.
KeywordsKripke Model Structural Rule Sequent Calculus Classical Propositional Logic Kripke Frame
Unable to display preview. Download preview PDF.