Undecidability of First-Order Intuitionistic and Modal Logics with Two variables

We prove that the two-variable fragment of first-order intuitionistic logic is undecidable, even without constants and equality. We also show that the two-variable fragment of a quantified modal logic L with expanding first-order domains is undecidable whenever there is a Kripke frame for L with a point having infinitely many successors (such are, in particular, the first-order extensions of practically all standard modal logics like K, K4, GL, S4, S5, K4.1, S4.2, GL.3 , etc.). For many quantified modal logics, including those in the standard nomenclature above, even the monadic two-variable fragments turn out to be undecidable.