# Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter

## TL;DR

This paper proves the undecidability of the positive fragment of certain first-order intuitionistic and modal logics with two variables and one monadic predicate, regardless of domain semantics, extending to various logical systems.

## Contribution

It establishes the undecidability of the two-variable fragment of multiple first-order intuitionistic and modal logics, including their semantics with expanding or constant domains.

## Key findings

- Positive fragment of intuitionistic logic with two variables is undecidable.
- Most natural first-order modal logics with two variables are undecidable.
- Results hold for both expanding and constant domain semantics.

## Abstract

We prove that the positive fragment of first-order intuitionistic logic in the language with two variables and a single monadic predicate letter, without constants and equality, is undecidable. This holds true regardless of whether we consider semantics with expanding or constant domains. We then generalise this result to intervals [QBL, QKC] and [QBL, QFL], where QKC is the logic of the weak law of the excluded middle and QBL and QFL are first-order counterparts of Visser's basic and formal logics, respectively. We also show that, for most "natural" first-order modal logics, the two-variable fragment with a single monadic predicate letter, without constants and equality, is undecidable, regardless of whether we consider semantics with expanding or constant domains. These include all sublogics of QKTB, QGL, and QGrz -- among them, QK, QT, QKB, QD, QK4, and QS4.