arXiv Science⌕ Search

arXiv subjects

Mikhail Rybakov

Publications and source records attributed to Mikhail Rybakov.

12 recordsLinked to original sources
arXiv2026

Semantics for the minimal well-determined logic

The minimal well-determined logic in the language with conjunction and implication is investigated. A calculus for this logic, in which the modus ponens rule is not postulated, is proposed. The main result consists in constructing a semantics for this logic: it is formed by the class of lower semilattices with a greatest element, where the implication is interpreted using a partial function defined via the partial order of the semilattice. This extension of the notion of interpreting logical connectives in a matrix allows for the correct determination of the truth of formulas in the language with conjunction and implication. Soundness and completeness theorems are proved. The proposed semantics creates an opportunity to investigate questions of finite model property for such systems and can also serve as a basis for studying other properties of both the minimal well-determined logic itself and its extensions. As an application of the obtained results, we prove that the set of tautologies of the minimal well-determined logic is decidable in polynomial time and present a corresponding decision algorithm.

math.LO↗
arXiv2025

Modelling of logical systems by means of their fragments

This work investigates the algorithmic complexity of non-classical logics, focusing on superintuitionistic and modal systems. It is shown that propositional logics are usually polynomial-time reducible to their fragments with at most two variables (often to the one-variable or even variable-free fragments). Also, it is proved that predicate logics are usually reducible to their fragments with one or two unary predicate letters and two or three individual variables. The work describes conditions sufficient for such reductions and provides examples where they fail, establishing non-reducibility in those cases. Furthermore, the work provides new complexity bounds for several logics, results on Kripke-incompleteness of predicate calculi, and analogues of the classical theorems of Church and Trakhtenbrot for the logic of quasiary predicates.

cs.LO↗
arXiv2025

Recursive inseparability of classical theories of a binary predicate and non-classical logics of a unary predicate

The paper considers algorithmic properties of classical and non-classical first-order logics and theories in bounded languages. The main idea is to prove the undecidability of various fragments of classical and non-classical first-order logics and theories indirectly, by extracting it as a consequence of the recursive inseparability of special problems associated with them. First, we propose a domino problem, which makes it possible to catch the recursive inseparability of two sets. Second, using this problem, we prove that the classical first-order logic of a binary predicate and the theory of its finite models where the predicate is symmetric and irreflexive are recursively inseparable in a language with a single binary predicate letter and three variables (without constants and equality). Third, we prove, for an infinite class of logics, that the monadic fragment of a modal predicate logic and the logic of the class of its finite Kripke frames are recursively inseparable in languages with a single unary predicate letter and two individual variables; the same result is obtained if we replace the condition of finiteness of frames with the condition of finiteness of domains allowed in frames. Forth, we expand the results to a wide class of superintuitionistic predicate logics. In particular, it is proved that the positive fragments of the intuitionistic predicate logic and the logic of the class of finite intuitionistic Kripke frames are recursively inseparable in the language with a single unary predicate letter and two individual variables. The technique used and the results obtained allow us to answer some additional questions about the decidability of special monadic fragments of some modal and superintuitionistic predicate logics.

math.LO↗
arXiv2025

Superintuitionistic predicate logics of linear frames: undecidability with two individual variables

The paper presents a solution to the long-standing question about the decidability of the two-variable fragment of the superintuitionistic predicate logic $\mathbf{QLC}$ defined by the class of linear Kripke frames, which is also the `superintuitionistic' fragment of the modal predicate logic $\mathbf{QS4.3}$, under the G\"odel translation. We prove that the fragment is undecidable ($\Sigma^0_1$-complete). The result remains true for the positive fragment, even with a single binary predicate letter and an infinite set of unary predicate letters. Also, we prove that the logic defined by ordinal $\omega$ as a Kripke frame is not recursively enumerable (even both $\Sigma^0_1$-hard and $\Pi^0_1$-hard) with the same restrictions on the language. The results remain true if we add also the constant domain condition. The proofs are based on two techniques: a modification of the method proposed by M.Marx and M.Reynolds, which allows us to describe tiling problems using natural numbers rather than pairs of numbers within an enumeration of Cantor's, and an idea of `double labeling' the elements from the domains, which allows us to use only two individual variables in the proof when applying the former method.

math.LO↗
arXiv2021

Algorithmic properties of first-order modal logics of linear Kripke frames in restricted languages

We study the algorithmic properties of first-order monomodal logics of frames $\langle \mathbb{N}, \leq \rangle$, $\langle \mathbb{N}, < \rangle$, $\langle \mathbb{Q}, \leq \rangle$, $\langle \mathbb{Q}, < \rangle$, $\langle \mathbb{R}, \leq \rangle$, $\langle \mathbb{R}, < \rangle$, as well as some related logics, in languages with restrictions on the number of individual variables as well as the number and arity of predicate letters. We show that the logics of frames based on $\mathbb{N}$ are $\Pi^1_1$-hard -- thus, not recursively enumerable -- in languages with two individual variables, one monadic predicate letter and one proposition letter. We also show that the logics of frames based on $\mathbb{Q}$ and $\mathbb{R}$ are $\Sigma^0_1$-hard in languages with the same restrictions. Similar results are obtained for a number of related logics.

cs.LO↗
arXiv2019

Recursive enumerability and elementary frame definability in predicate modal logic

We investigate the relationship between recursive enumerability and elementary frame definability in first-order predicate modal logic. On the one hand, it is well-known that every first-order predicate modal logic complete with respect to an elementary class of Kripke frames, i.e., a class of frames definable by a classical first-order formula, is recursively enumerable. On the other, numerous examples are known of predicate modal logics, based on `natural' propositional modal logics with essentially second-order Kripke semantics, that are either not recursively enumerable or Kripke incomplete. This raises the question of whether every Kripke complete, recursively enumerable predicate modal logic can be characterized by an elementary class of Kripke frames. We answer this question in the negative, by constructing a normal predicate modal logic which is Kripke complete, recursively enumerable, but not complete with respect to an elementary class of frames. We also present an example of a normal predicate modal logic that is recursively enumerable, Kripke complete, and not complete with respect to an elementary class of rooted frames, but is complete with respect to an elementary class of frames that are not rooted.

math.LO↗
arXiv2019

Complexity of finite-variable fragments of propositional modal logics of symmetric frames

While finite-variable fragments of the propositional modal logic S5--complete with respect to reflexive, symmetric and transitive frames--are polynomial-time decidable, the restriction to finite-variable formulas for logics of reflexive and transitive frames yields fragments that remain "intractable." The role of the symmetry condition in this context has not been investigated. We show that symmetry either by itself or in combination with reflexivity produces logics that behave just like logics of reflexive and transitive frames, i.e. their finite-variable fragments remain intractable, namely PSPACE-hard. This raises the question of where exactly the borderline lies between modal logics whose finite-variable fragments are tractable and the rest.

math.LO↗
arXiv2019

Complexity and Expressivity of Branching- and Alternating-Time Temporal Logics with Finitely Many Variables

We show that Branching-time temporal logics CTL and CTL*, as well as Alternating-time temporal logics ATL and ATL*, are as semantically expressive in the language with a single propositional variable as they are in the full language, i.e., with an unlimited supply of propositional variables. It follows that satisfiability for CTL, as well as for ATL, with a single variable is EXPTIME-complete, while satisfiability for CTL*, as well as for ATL*, with a single variable is 2EXPTIME-complete,--i.e., for these logics, the satisfiability for formulas with only one variable is as hard as satisfiability for arbitrary formulas.

cs.LO↗
arXiv2019

Complexity and expressivity of propositional dynamic logics with finitely many variables

We investigate the complexity of satisfiability for finite-variable fragments of propositional dynamic logics. We consider three formalisms belonging to three representative complexity classes, broadly understood,---regular PDL, which is EXPTIME-complete, PDL with intersection, which is 2EXPTIME-complete, and PDL with parallel composition, which is undecidable. We show that, for each of these logics, the complexity of satisfiability remains unchanged even if we only allow as inputs formulas built solely out of propositional constants, i.e. without propositional variables. Moreover, we show that this is a consequence of the richness of the expressive power of variable-free fragments: for all the logics we consider, such fragments are as semantically expressive as entire logics. We conjecture that this is representative of PDL-style, as well as closely related, logics.

cs.LO↗
arXiv2018

On complexity of propositional Linear-time Temporal Logic with finitely many variables

It is known [DemriSchnoebelen02] that both satisfiability and model-checking problems for propositional Linear-time Temporal Logic, LTL, with only a single propositional variable in the language are PSPACE-complete, which coincides with the complexity of these problems for LTL with an arbitrary number of propositional variables [SislaClarke85]. In the present paper, we show that the same result can be obtained by modifying the original proof of SPACE-hardness for LTL from [SislaClarke85]; i.e., we show how to modify the construction from [SislaClarke85] to model the computations of polynomially-space bound Turing machines using only formulas of one variable. We believe that our alternative proof of the results from [DemriSchnoebelen02] gives additional insight into the semantic and computational properties of LTL.

cs.LO↗
arXiv2017

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

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.

cs.LO↗