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

DOI10.1007/S11225-018-9815-7MaRDI QIDQ6287908arXivWikidataFDO

Publication date 15 June 2017

Modal logic (including the logic of norms) (03B45) Subsystems of classical logic (including intuitionistic logic) (03B20) Decidability of theories and sets of sentences (03B25)

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.

This page was built for publication: Undecidability of first-order modal and intuitionistic logics with two variables and one monadic predicate letter

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6287908)