Computational complexity of non-classical logics of an unary predicate

We consider the algorithmic complexity of non-classical predicate logics in restricted languages. In 1962, S.Kripke suggested how to simulate a binary predicate letter of a classical first-order formula with a modal first-order formula containing two unary letters. Building on Kripke's idea, we simulate a binary precidate letter with a single unary letter in modal formulas and with two unary letters in superintuitionistic formulas. This immediately gives us the undecidability of numerous modal logics in languages with one unary letter, and superintuitionistic logics with two unary letters, and three variables, since the classical logic of a binary predicate is undecidable with three variables. In addition, we show how to simulate any number of unary letters with a single unary letter (both in modal and intuitionistic languages). Due to the well-known results on the undecidability of many non-classical logics in languages with two variables (D.Gabbay, V.Shehtman (1993), R.Konchakov, A.Kurucz, M.Zakharyaschev (2005)), we obtain the undecidability of many modal and superintuitionistic predicate logics in languages with a single unary predicate letter and two variables. The proposed encoding enables us to obtain the non-enumerability and even non-arithmeticity of the corresponding fragments of a number of logics of Kripke frames. We shall prove in detail that the following logics are not recursively enumerable in languages with a single unary predicate letter and three individual variables: modal predicate logics of natural classes of finite (in terms of the number of worlds) Kripke frames and the positive fragment of intuitionistic predicate logic of finite Kripke frames.