# Validity problem of intuitionistic two-variable logic

The two-variable fragment $$\mathrm{FO}^2$$ consist of those sentences of first-order logic $$\mathrm{FO}$$ in which precisely two variables occur (e.g. $$\exists x \exists y \exists z R(x,y,z)$$ is not a sentence of $$\mathrm{FO}^2$$). In  it is proved that the validity problem of $$\mathrm{FO}^2$$ is coNEXPTIME-complete. What about intuitionistic $$\mathrm{FO}^2$$? Does it have the same complexity or is it harder? For comparison, the validity problem of propositional logic is coNP-complete while the validity problem of propositional intuitionistic logic is PSPACE-complete, see .

This question could of course be asked in more general terms by replacing $$\mathrm{FO}^2$$ with any reasonable subset of $$\mathrm{FO}$$. If there is a more general connection between the classical validity problem and the intuitionistic validity problem, then I would be happy to hear about it.

 Grädel, E., Kolaitis, P., & Vardi, M. (1997). On the Decision Problem for Two-Variable First-Order Logic. Bulletin of Symbolic Logic, 3(1), 53-69.

 Statman, R. (1979). Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9(1), 67-72.

• Any reason to think this is decidable even? Note that fragments of IL are a bit harder to characterize: there is no such thing as a prenex-normal form!
– cody
Dec 28, 2021 at 22:58
• Note that intuitionistic modal logics are decidable. There are tons of papers available about them, but let me point out a paper by Alechina and Shkatov sciencedirect.com/science/article/pii/S1570868305000431, where they translated some intuitionistic modal logics into the two-variable non-intuitionistic guarded fragment. This is, however, not applicable to FO2. Yet another related paper on modal logics is the PHD thesis of Tim Lyon, see the following link for a proof-theoretic treatment of MLs: arxiv.org/abs/2107.14487 Dec 29, 2021 at 9:24

• Thanks for the reference; the proof is surprisingly simple. Furthermore, it seems to me that one can use essentially the same argument to prove that the validity problem of intuitionistic fluted logic $\mathrm{FL}$ is undecidable. Dec 29, 2021 at 14:25