А. С. Герасимов (Санкт-Петербург)
Депренексификация в финитарных аналитических исчислениях для первопорядковой бесконечнозначной логики Лукасевича и полнота основанных на них инфинитарных исчислений.
Аннотация
В докладе рассматривается несколько финитарных аналитических гиперсеквенциальных исчислений для первопорядковой бесконечнозначной логики Лукасевича \L$\forall$, включая введённое Баацем (Baaz) и Меткалфом (Metcalfe) исчисление G\L$\forall$. В этих исчислениях правило сечения не допустимо и, вообще говоря, формула и её (определённая чисто синтаксически) пренексная форма не равновыводимы. Однако мы предлагаем метод депренексификации, позволяющий любой вывод любой гиперсеквенции $H$, в которой выделено вхождение любой пренексной формы любой формулы $F$, алгоритмически перестроить в вывод гиперсеквенции, полученной из $H$ заменой этого вхождения на $F$. С помощью этого метода мы устанавливаем полноту инфинитарных аналитических исчислений для \L$\forall$, основанных на вышеупомянутых финитарных исчислениях. В частности, даём первое верное доказательство полноты основанного на G\L$\forall$ инфинитарного аналитического исчисления для \L$\forall$.
Прослушивание доклада, состоявшегося на нашем семинаре 03.06.2025, не обязательно для понимания анонсируемого доклада; последний лишь опирается на основной результат первого.