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 (with and without the Barcan formula) and the classical
predicate logic (with one-sorted variable). We present a purely
proof-theoretic proof-transformation method, reducing an
LK-proof of an interpreted formula to a modal proof.