A Brief Realization History

Proofs of realization for various modal logics have a history of interest, and some discussion and references are pertinent.

As we have already noted, the first realization proof that connected S4 and LP was constructive and made use of a cut-free sequent calculus for S4.

The nonconstructive approach to realization originated in Fitting (2003,2005) with a correction in Fitting (2010). It was extended to a broad range of modal logics, in Fitting (2014a), with these results discussed in the present chapter.

Semantic tableaus were used in Fitting (2013a) to provide a constructive proof of realization for S4 that proceeded step-by-step, making an implemen­tation relatively easy. Such an implementation was given in Prolog.

S5 was a kind of exploration ground for a number of years. A somewhat nonstandard axiomatization was given in Artemov et al. (1999) and Kazakov (1999), and a realization theorem was shown constructively using hyperse- quents. A standard axiomatization provided the basis for a nonconstructive proof of the S5 realization theorem in Rubtsova (2006b) and Pacuit (2005, 2006). In Fitting (2011b), a somewhat peculiar sequent calculus for S5 was used to give a constructive realization proof. This sequent calculus was based on a tableau system given in Fitting (1999) and has no known generalizations to other logics.

A Merging Theorem was stated and proved in Fitting (2009). This gives a constructive algorithm for combining realizations and provides appropriate machinery for handling branching rules in tableau or sequent calculi.

Kuznets and Goetschi (2012) and Borg and Kuznets (2015) used nested se­quent calculi to constructively show realization theorems for all the modal log­ics in the so-called modal cube.

Finally, the Model Existence Theorem for S4 was used in Fitting (2013b) to show realization for S4. Similar proofs could be give for those other modal logics known to have a Model Existence Theorem, but this is a rather small number.