Алгоритмические вопросы расширения логик Альберта Виссера

Вестник Санкт-Петербургского университета. Серия 1. Математика. Механика. Астрономия. 2025.

Лукашов С. М.

With the increasing volume of scientific information and the growing complexity of methodological approaches, the development of effective methods for the interpretation, assimilation, and transmission of new knowledge becomes ever more important. Considering the interdisciplinary nature of modern research and the lag of educational systems in adapting to these changes, the accessibility of proofs acquires particular significance.

This article examines a fragment of the basic propositional first-order logic QBL restricted to two variables. The study of this logic is of interest in the context of revisiting intuitionistic perspectives on the nature of proof, particularly regarding the interpretation of implication. By reducing the tiling problem with dominoes, the recursive inseparability of the fragments of QBL and QInt logics in the two-variable language is established. The result demonstrates that even severely restricted fragments of non-classical logics retain high computational complexity and undecidability properties.

The research contributes to a deeper understanding of the algorithmic limits of formal systems and highlights the need for further analysis of weak linguistic fragments in the context of automated theorem proving, formal verification methods, and theoretical computer science.

Keywords: неклассические логики, рекурсивная неотделимость, базисная пропозициональная логика, логика с двумя переменными