Abstract

It is well known that the modal logic S5 can be embedded in the classical predicate logic by interpreting the modal operator in terms of a quantifier. Wajsberg proved this fact in a syntactic way. Mints extended this result to the quantified version of S5; using a purely proof-theoretic method he showed that the quantified S5 corresponds to the classical predicate logic with one-sorted variable. In this paper we extend Mints’ result to the basic modal logic S4; we investigate the correspondence between the quantified versions of S4 and the classical predicate logic. We present a purely proof-theoretic proof-transformation method, reducing an LK-proof of an interpreted formula to a modal proof.