Agi Kurucz

Undecidability of two-variable intuitionistic and modal predicate logics

Ever since the undecidability of first-order classical logic became known, there has been a continuing interest in establishing the `borderline' between its decidable and undecidable fragments. One approach to this classification problem is to consider fragments with finitely many individual variables. The borderline here goes between two and three: the two-variable fragment of classical first-order logic is decidable, while with three variables it becomes undecidable.

As classical first-order logic can be reduced to intuitionistic first-order logic by Gödel's double negation translation, the three-variable fragment of the latter is also undecidable. We solve a long-standing open problem by showing that, unlike its classical counterpart, already the two-variable fragment of first-order intuitionistic logic is undecidable, even without constants and equality. We also discuss similar questions about modal predicate logics.

This is joint work with Roman Kontchakov and Michael Zakharyaschev.