Maximality in modal logic (Q1092032)

A system FP of propositional logic is maximal for the corresponding system FA of arithmetic if the underivability of \(A(p_ 1,...,p_ n)\) in FP implies underivability in FA of \(A(B_ 1,...,B_ n)\) for some sentences \(B_ 1,...,B_ n\) of FA. The authors prove maximality for Grzegorczyk's modal logic Grz and for S4. For Grz the proof is modelled after \textit{C. Smorynski}'s argument (Applications of Kripke models, in \textit{A. Troelstra}'s volume [Lecture Notes Math. 344 (1973; Zbl 0275.02025)]). Falsifying sentences \(B_ i\) are constructed in rather natural way from \(\Sigma^ 0_ 1\)-sentences completely independent over PA. The proof for S4 is much more complicated and may be even more important than the final result. The main novel feature is verification of the induction axiom in the constructed Kripke model. A version of iterated Ramsey theorem and a translation of modal arithmetic formulas in non-modal ones are developed to achieve this.