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 [1] 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 [2].

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.

[1] 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.

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

  • 2
    $\begingroup$ 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! $\endgroup$
    – cody
    Commented Dec 28, 2021 at 22:58
  • 2
    $\begingroup$ 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 $\endgroup$ Commented Dec 29, 2021 at 9:24

1 Answer 1


The two-variable fragment of intuitionistic first-order logic is undecidable, as proved in

Roman Kontchakov, Agi Kurucz, and Michael Zakharyaschev: Undecidability of First-Order Intuitionistic and Modal Logics with Two Variables, Bulletin of Symbolic Logic 11 (2005), no. 3, pp. 428–438. http://www.jstor.org/stable/1578742.

  • 1
    $\begingroup$ 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. $\endgroup$ Commented Dec 29, 2021 at 14:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.