On the Definability Problem of First-Order Sentences by Propositional Intuitionistic Formulas

We consider restricted forms of the algorithmic problem of definability of first-order sentences by propositional formulas with intuitionistic Kripke frames semantics. We demonstrate positive resolutions for classes of intuitionistic Kripke frames based on linear orders and conversely show that a few natural first-order definable classes give rise to undecidable definability problems by applying the model-theoretic in the nature technique of stable classes of Kripke frames.