О конечной базируемости по допустимости табличных модальных (суперинтуиционистских) логик.

Римацкий В.В.


Пусть заданы табличные модальные (суперинтуиционистские) логики $\lambda_1,\ \lambda_2 \ : \
\lambda_1 \subseteq \lambda_2$.\ Доказана следующая
\begin{teo} \quad
%Пусть заданы табличные модальные (суперинтуиционистские)
% логики $\lambda_1,\ \lambda_2 \ : \
% \lambda_1 \subseteq \lambda_2$.\
Если логика $\lambda_1$ имеет конечный базис для допустимых правил вывода
(ДПВ),\,
то логика $\lambda_2$ также имеет такой базис.\
\end{teo}
Заметим также,\, что из Теоремы 1 следует:\ \
(1) \ логики из верхней части решетки модальных (суперинтуиционистских)
логик конечно базируемы по допустимости;\
(2) \ в верхней части решетки модальных (суперинтуиционистских) логик
существуют максимальные логики без конечного базиса ДПВ (но любое собственное
расширение таких логик уже имеет конечный базис ДПВ).
\bigskip
Используя полученный результат доказан {\it критерий конечной базируемости по
допустимости табличных модальных (суперинтуиционистских) логик}:
\begin{teo}
Пусть задан конечный рефлексивный транзитивный фрейм ${\cal G}$.\
Табличная модальная (суперинтуиционистская) логика $\lambda({\cal G})$
не имеет конечного базиса допустимых правил вывода тогда и только тогда,\
когда фрейм ${\cal G}$ удовлетворяет следующим условиям:\ \
(I)\ существует нетривиальная антицепь ${\cal A}$ сгустков ${\cal G}$ такая что
два ее нетривиальных подмножества имеют R-предшественников (ко-накрытия)
$C_1, C_2$ соответственно;\
(II)\ антицепь $\{ C_1, C_2 \} $ имеет R-предшественника (ко-накрытие) -- сгусток $C_0$.
\end{teo}
%\pagebreak
\smallskip
Литература:
[1] \ В.В.Рыбаков. Базисы допустимых правил вывода S4 и Int.
Алгебра и логика,24,N1(1985),87-107.
[2] \ V.V. Rybakov. \ Admissibility of logical inference rules,\, New-York --
Amsterdam,\, 1997.