Неразрешимость одноместных PFP-операторов без вложения в теории одного следования

Аннотация

В данной работе мы исследуем разрешимость расширений логики первого порядка. Например, в работах А. С. Золотова показано, что логика с унарным оператором транзитивного замыкания для теории следования является разрешимой. Мы показываем, что в аналогичной ситуации логика с унарным оператором частичной неподвижной точки разрешимой не является. Для этого мы сводим проблему остановки счетчиковой машины к проблеме истинности формулы. При этом используется только один оператор частичной неподвижной точки, он является унарным, невложенным и применяется к универсальной или экзистенциальной формуле.