Intuitionistic first-order predicate logic is not decidable for arbitrary formulas.
However, suppose that we are given a formula of first-order predicate logic that is classically valid. Is there a decision procedure that will determine whether it is also valid intuitionistically?
Restricting to classically valid formulas doesn't do anything here. Let $\psi$ be a fixed formula which is classically valid, but not intuitionistically. Now for a given formula $\phi$, consider $\psi \vee \phi$. This formula is classically valid, and it is intuitionistically valid if and only if $\phi$ was.
