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

DOI10.1007/S11225-018-9815-7arXiv1706.05060WikidataQ129560000 ScholiaQ129560000MaRDI QIDQ6287908FDOQ6287908

Publication date: 15 June 2017

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.

Mathematics Subject Classification ID

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

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)