Background

Realization theorems connect modal logics and justification logics—at least, some modal logics and some justification logics. It is not known how extensive the phenomenon is, but it has turned out to be much broader than was originally thought.

All constructive proofs are based on some version of cut-free proof system— a realization is not extracted from a modal validity, but from a cut-free proof of that validity. The first and most common cut-free proof system is the sequent calculus, with modal versions deriving from the historic work of Gentzen on intuitionistic and classical systems. Such proofs have two features that are sig­nificant for realization arguments. First, all formulas that enter into sequent proofs are subformulas of the formula being proved. And second, all occur­rences of the “same” formula in a proof have the same polarity, positive or negative. (Loosely, a positive subformula of a formula is one that appears in the scope of an even number of negation signs.) We begin the chapter with a formal presentation of a sequent calculus for the modal logic S4. It was used in the original realization theorem proof, Artemov (1995, 2001), a proof that is presented in Chapter 6.

Sequents and semantic tableaus have a close relationship. Tableaus, and their machinery, have features that make them particularly handy for realiza­tion proofs, both constructive and nonconstructive. In particular, we use signed tableaus, and signed formulas have an existence that breaks them free from se- quents, while carrying with them the key information about where they were in the sequent—on the left or on the right. Much of the present chapter presents what we will need about tableaus, with applications in Chapter 7.

5.2