|
Труды ордена Ленина Математического института имени В. А. Стеклова, 1972, том 121, страницы 100–108
(Mi tm3113)
|
|
|
|
Неразрешимые классы формул для конструктивного исчисления предикатов. I
В. П. Оревков
Аннотация:
Секвенция называется абсолютной, если в ее сукцеденте не более одной формулы и она
не содержит вхождений знаков $\supset$, $\neg$ и положительных вхождений квантора $\forall$. Показано, что абсолютная секвенция тогда и только тогда выводима в классическом исчислении предикатов, когда она выводима в конструктивном и минимальном исчислениях предикатов. Используя
генценовские методы, доказывается, что класс абсолютных секвенций вида
$$
A\to\exists x_1\dots x_n(P_1(x_2,\dots,x_n)\& P_2(x_1,\dots,x_n)),
$$
где формула $A$ не содержит предикатных переменных, отличных от $P_1$ и $P_2$, является классом
сведения как для классического, так и для конструктивного исчисления предикатов.
Библ. 12 назв.
Образец цитирования:
В. П. Оревков, “Неразрешимые классы формул для конструктивного исчисления предикатов. I”, Логические и логико-математические исчисления. 2, Тр. МИАН СССР, 121, 1972, 100–108; Proc. Steklov Inst. Math., 121 (1972), 111–119
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/tm3113 https://www.mathnet.ru/rus/tm/v121/p100
|
Статистика просмотров: |
Страница аннотации: | 135 | PDF полного текста: | 54 |
|