Данный сайт более не обновляется.
Актуальная информация - по адресу vestnik.math.msu.su

УДК 510.649

Об исчислении Ламбека с одним делением и одним примитивным типом, допускающем пустые антецеденты / С. Л. Кузнецов. // Вестн. Моск. ун-та. Сер. 1, Математика. Механика. 2009. ? 2. С. 62-65.

Доказывается следующее утверждение: правило вывода, заданное схемой, допустимо в исчислении Ламбека с одним делением \mathrm{L}^*(\backslash), допускающем пустые антецеденты, тогда и только тогда, когда оно допустимо во фрагменте \mathrm{L}^*(\backslash) с одним примитивным типом \mathrm{L}^*(\backslash; p_1). Для этого применяется подстановка типов, сводящая выводимость в \mathrm{L}^*(\backslash) к выводимости в \mathrm{L}^*(\backslash;p_1).

Ключевые слова: исчисление Ламбека, допустимые правила, сети доказательства.

Библиогр. 5.