Всеслав Станиславович Секоринул. Желябова, д. 33, г. Тверь, 170100
Vseslav Stanislavovich Sekorin33 Zhelyabova str., Tver, 170100
В данной работе мы исследуем разрешимость расширений логики первого порядка. Например, в работах А. С. Золотова показано, что логика с унарным оператором транзитивного замыкания для теории следования является разрешимой. Мы показываем, что в аналогичной ситуации логика с унарным оператором частичной неподвижной точки разрешимой не является. Для этого мы сводим проблему остановки счетчиковой машины к проблеме истинности формулы. При этом используется только один оператор частичной неподвижной точки, он является унарным, невложенным и применяется к универсальной или экзистенциальной формуле.
We investigate the decidability of first-order logic extensions. For example, it is established in A. S. Zolotov’s works that a logic with a unary transitive closure operator for the one successor theory is decidable. We show that in a similar case, a logic with a unary partial fixed point operator is undecidable. For this purpose, we reduce the halting problem for the counter machine to the problem of truth of the underlying formula. This reduction uses only one unary non-nested partial fixed operator that is applied to a universal or existential formula.
The authors declare that there are no conflicts of interest present.