Отмеченное субординатное натуральное исчисление для базовой интуиционистской кондициональной логики

Аннотация

В статье осуществляется презентация и построение отмеченного субординатного натурального исчисления $\mathcal F\mathbf{IntCK}$ для интуиционистской кондициональной логики $\textbf{IntCK}$, предложенной Г.К. Ольховиковым как интуиционистский вариант минимальной нормальной кондициональной логики Б. Челласа $\textbf{CK}$ и полной относительно интуиционистского прочтения метатеории $\textbf{CK}$. Система $\textbf{IntCK}$ задает базовые дедуктивные принципы для формализации конструктивных контекстов, допускающих использование двух независимых контрфактических связок – $\square\mspace{-8mu}\to$ и ◇→. Описываемое в статье натуральное исчисление $\mathcal F\mathbf{IntCK}$ основывается на технике, задействующей метки (labels), реляционные атомы (relational atoms) и отмеченные квазиформулы, фигурирующие в правилах, причем данные правила позволяют метасинтаксически реализовать семантические условия истинности и неистинности формул относительно возможных миров интуиционистской кондициональной биреляционной модели. В рамках статьи предлагается индуктивное определение вывода, для чего применяется подход В.А. Смирнова с дальнейшей модификацией понятия субординатной последовательности на случай с отмеченными квазиформулами и реляционными атомами. Дана идея доказательства метатеорем о слабой полноте исчисления $\mathcal F\mathbf{IntCK}$ по отношению к классу всех интуиционистских кондициональных биреляционных шкал, а также дедуктивной эквивалентности натурального исчисления $\mathcal{F}\mathbf{IntCK}$ и аксиоматического исчисления $\mathbf{IntCK}$.