Undecidability of modal and superintuitionistic logics of a single unary predicate in languages with two variables

We consider the issues concerning 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. Our results extend to polymodal logics, such as predicate counterparts of CTL$^*$, CTL, LTL, epistemic logics, logics with universal modality, etc.