<p>The two-variable fragment of intuitionistic first-order logic is undecidable, as proved in</p>
<p>Roman Kontchakov, Agi Kurucz, and Michael Zakharyaschev: <em>Undecidability of First-Order Intuitionistic and Modal Logics with Two Variables</em>, Bulletin of Symbolic Logic 11 (2005), no. 3, pp. 428–438. <a href="http://www.jstor.org/stable/1578742" rel="noreferrer">http://www.jstor.org/stable/1578742</a>.</p>

CC BY-SA 4.0
2021-12-29T14:25:55.307Z
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.
Reijo Jaakkola
CC BY-SA 4.0
2021-12-29T13:31:26.880Z
2021-12-29T13:31:26.880Z
Emil Jeřábek
<p>The two-variable fragment <span class="math-container">$\mathrm{FO}^2$</span> consist of those sentences of first-order logic <span class="math-container">$\mathrm{FO}$</span> in which precisely two variables occur (e.g. <span class="math-container">$\exists x \exists y \exists z R(x,y,z)$</span> is not a sentence of <span class="math-container">$\mathrm{FO}^2$</span>). In [1] it is proved that the validity problem of <span class="math-container">$\mathrm{FO}^2$</span> is coNEXPTIME-complete. What about <em>intuitionistic</em> <span class="math-container">$\mathrm{FO}^2$</span>? 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].</p>
<p>This question could of course be asked in more general terms by replacing <span class="math-container">$\mathrm{FO}^2$</span> with any reasonable subset of <span class="math-container">$\mathrm{FO}$</span>. 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.</p>
<p>[1] Grädel, E., Kolaitis, P., &amp; Vardi, M. (1997). On the Decision Problem for Two-Variable First-Order Logic. Bulletin of Symbolic Logic, 3(1), 53-69.</p>
<p>[2] Statman, R. (1979). Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9(1), 67-72.</p>

CC BY-SA 4.0
2021-12-28T22:58:36.230Z
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
CC BY-SA 4.0
2021-12-29T09:24:38.150Z
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 https://www.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: https://arxiv.org/abs/2107.14487
Bartosz Bednarczyk
<lo.logic><complexity><first-order-logic>
Validity problem of intuitionistic two-variable logic
Reijo Jaakkola
# Validity problem of intuitionistic two-variable logic

(Asked by: username_0 on 2021-12-28)

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.

**Tags:** lo.logic, complexity, first-order-logic

> **Comments:**
> **username_1**: 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!  
> **username_2**: 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 https://www.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: https://arxiv.org/abs/2107.14487  

---

## 1 answers

### Answer by username_3 on 2021-12-29. Score: 8 | Accepted answer

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>.

> **Comments:**
> **username_0**: 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.  

---

