Аналитико-табличное исчисление, адекватное логике суждений существования

Аннотация

В [Маркин, 2021] была построена логическая теория, предназначенная для анализа рассуждений, посылками и заключениями которых являются суждения существования и их булевы комбинации. В ее языке содержится неопределенно-местная константа существования, простые формулы образуются сочленением этой константы с произвольной конечной последовательностью общих терминов — положительных (простых) и отрицательных, сложные формулы образуются с помощью пропозициональных связок. Для этого языка были сформулированы естественная семантика и адекватное ей аксиоматическое исчисление. В данной работе предлагается аналитико-табличный вариант исчисления суждений существования: постулируются правила редукции для формул с константой существования и их отрицаний, вводится понятие аналитической таблицы как последовательности конфигураций, формулируются критерии замкнутости таблицы. Формула $A$ доказуема в данном исчислении, если и только если существует замкнутая аналитическая таблица, первой конфигурацией которой является семейство $\{\{\neg A\}\}$. Доказываются метатеоремы о корректности и полноте данного исчисления относительно семантически построенной логики суждений существования. Предлагается процедура, позволяющая эффективно решать вопрос о доказуемости или недоказуемости произвольной формулы $A$. Особенность этой процедуры состоит в следующем. Выделяется список $\mathcal{T}$ положительных терминов, содержащий все такие термины $P$, что $P$ или $P^\prime$ (отрицательный термин, противоречащий $P$) входят в состав $A$. В состав последней конфигурации входят только множества, элементами которых являются атомарные формулы и их отрицания, причем последовательность терминов после константы существования содержит $P$ или $P^\prime$ для любого $P$ из $\mathcal{T}$. Доказывается метатеорема о разрешимости аналитико-табличного исчисления суждений существования.