|
Вестник Московского университета. Серия 1: Математика. Механика, 2009, номер 2, страницы 62–65
(Mi vmumm863)
|
|
|
|
Краткие сообщения
Об исчислении Ламбека с одним делением и одним примитивным типом, допускающем пустые антецеденты
С. Л. Кузнецов Московский государственный университет имени М. В. Ломоносова, механико-математический факультет
Аннотация:
Доказывается следующее утверждение: правило вывода, заданное схемой, допустимо в исчислении Ламбека с одним делением $\mathrm{L}^*(\backslash)$, допускающем пустые антецеденты, тогда и только тогда, когда оно допустимо во фрагменте $\mathrm{L}^*(\backslash)$ с одним примитивным типом $\mathrm{L}^*(\backslash; p_1)$. Для этого применяется подстановка типов, сводящая выводимость в $\mathrm{L}^*(\backslash)$ к выводимости в $\mathrm{L}^*(\backslash;p_1)$.
Ключевые слова:
исчисление Ламбека, допустимые правила, сети доказательства.
Поступила в редакцию: 28.04.2008
Образец цитирования:
С. Л. Кузнецов, “Об исчислении Ламбека с одним делением и одним примитивным типом, допускающем пустые антецеденты”, Вестн. Моск. ун-та. Сер. 1. Матем., мех., 2009, № 2, 62–65
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/vmumm863 https://www.mathnet.ru/rus/vmumm/y2009/i2/p62
|
Статистика просмотров: |
Страница аннотации: | 67 | PDF полного текста: | 31 |
|