Alexander SAKHAROV
A b s t r a c t. First-order intuitionistic logic extended with the assumption about decidability of all propositional atoms combines classical and intuitionistic properties. Two classes of formulas on which this extension coincides with classical and intuitionistic logic, respectively, are identified. Constrained Kripke structures are introduced for modeling intuitionistic logic with decidable propositional atoms. The extent of applicability of classical-only laws, the extent of the disjunction and existence properties, decidability issues, and translations are investigated.