In Ch. 19 of the 4th edition of Methods of Logic, Quine gives a decision procedure for classical monadic first order logic (technically it's a decision procedure for what he calls "Boolean statement schemata", which are identical to first order sentences containing no universal quantifiers or relational predicates, and with every existential quantifier in prenex position modulo negations. Every monadic first order sentence can be translated into such a form.)
The procedure requires translating the "Boolean term schema" (e.g. $P \to Q$ is the term schema of $\exists x (Px \to Qx)$) to conjunctive normal form. Because the CNF form of a sentence in classical logic is not (necessarily) equivalent to the CNF form of the same sentence in intuitionist logic due to the lack of an equivalency rule for double-negation in intuitionist logic, I'm not sure if the procedure can be adapted. I don't think it can be straightforwardly adapted at least.
I'm doing some dependently typed programming and knowledge of a decision procedure for monadic intuitionist/constructivist logic would be immensely helpful if it exists. Does it? If so, could someone point me to a reference?
Best Answer
Tl;dr -- the answer is "no", and you can find a proof in Undecidability of First-Order Modal and Intuitionistic Logics with Two Variables and One Predicate Letter, by Ryabakov and Shkatov, available here. Precisely:
Notice this is consistent with Pilcrow's answer, since we can faithfully translate intuitionistic single-variable monadic formulas into the (decidable) modal logic $\mathsf{MIPC}$.
Now, to explain where my initial (and incorrect) comment came from:
The usual proof of the corresponding fact for classical logic is a "filtration argument". We first prove
Then all that's left is to say that, by the completeness theorem, $\varphi$ is provable if and only if $\lnot \varphi$ is not satisfiable. But by the above theorem it suffices to check if any models of size $\leq m 2^n$ satisfy $\lnot \varphi$, and this is a finite check (albeit a large one).
Now, the hiccup comes when we pass to the intuitionistic setting. Now our models are more involved. In particular, while classical models can all be taken to have truth values in $\{0,1\}$, intuitionistic models need to take values in arbitrary heyting algebras. The "$2$" in $2^n$ comes from enumerating every possible assignment of truth values to the $P_1, \ldots P_n$, but now there might be more than two possible truth values. The natural idea is to try and prove a theorem of the form
Then we would have a larger check to go through, but it would still be finite. When writing my comment, I was remembering a result that intuitionistic propositional logic is decidable because we can bound the size of the heyting algebras of interest (albeit double exponentially), see MJD's answer here for example. I thought we could use this to also bound the size of a heyting algebra involved in the semantics of IPC, but it looks like we can't.
Again, you can find a proof of the undecidability in the linked paper by Ryabakov and Shkatov. For an older, and less sharp account (it puts no bound on the necessary number of variables, but the corresponding proof is easier), you can see Chapter $14$ of Semantical Investigations of Heyting's Intuitionistic Logic by Gabbay.
I hope this helps ^_^