Бесповторное и инфинитарные аналитические исчисления для рациональной логики Павелки первого порядка
Ключевые слова:
многозначная логика, математическая нечёткая логика, бесконечнозначная логика Лукасевича первого порядка, рациональная логика Павелки первого порядка, теория доказательств, гиперсеквенциальное иcчисление, поиск вывода, инфинитарное исчисление.Аннотация
Предлагается аналитическое гиперсеквенциальное исчисление $\textnormal{G}^3\textnormal{\L}\forall$ для бесконечнозначной логики Лукасевича первого порядка $\textnormal{\L}\forall$ и для её расширения-рациональной логики Павелки первого порядка $\textnormal{RPL}\forall$; это исчисление предназначено для поиска вывода снизу вверх. В исчислении $\textnormal{G}^3\textnormal{\L}\forall$ нет структурных правил, все его правила обратимы, и обозначения мультимножеств формул не повторяются ни в какой посылке его правил. В $\textnormal{G}^3\textnormal{\L}\forall$ выводимо любое предложение, которое выводимо хотя бы в одном из ранее известных аналитических исчислений для $\textnormal{\L}\forall$ или $\textnormal{RPL}\forall$, включая введённое Баацем и Меткалфом гиперсеквенциальное исчисление $\textnormal{G}\textnormal{\L}\forall$ для $\textnormal{\L}\forall$. В статье изучаются теоретико-доказательственные свойства $\text{\textnormal{G}}^3\text{\textnormal{\L}}\forall$, чем обеспечиваются основания для алгоритмов поиска вывода. Также даётся первое правильное доказательство полноты основанного на $\textnormal{G}\textnormal{\L}\forall$ инфинитарного исчисления для предварённых $\textnormal{\L}\forall$-предложений, и устанавливается полнота основанного на $\textnormal{G}^3\textnormal{\L}\forall$ инфинитарного исчисления для предварённых $\textnormal{RPL}\forall$-предложений.
