|
Записки научных семинаров ЛОМИ, 1979, том 88, страницы 163–175
(Mi znsl3110)
|
|
|
|
Эта публикация цитируется в 1 научной статье (всего в 1 статье)
Три способа выявления несущественных формул в секвенциях
В. П. Оревков
Аннотация:
Первый способ основан на известном приеме спуска утончений вниз и является дальнейшим развитием лемм о “прополке” работы [1]. Второй способ основан на использовании достаточно широких классов секвенций, для которых выводимость в интуиционистском исчислении предикатов совпадает с выводимостью в классическом исчислении предикатов и верно известное свойство дизъюнкции. Этим способом можно получить, например, синтаксическое доказательство следующего утверждения.
Если положительная формула $A$ выводима в теории групп при дополнительных предположениях вида
$$
\rceil\forall x_1\dots x_n\bigvee_{i<j}x_i=x_j\quad\text{или}\quad\rceil\forall x(x^n=e)\quad\text{или}\quad\rceil\forall x\exists y(y^n=x),
$$
то $A$ выводима в теории групп и без этих предположений. В качестве третьего способа предложен синтаксически формулируемый критерий консервативности расширений интуиционистских аксиоматических теорий. С помощью этого критерия может быть получено, например, синтаксическое доказательство наследственной неразрешимости интуиционистской теории равенства, дополнительными аксиомами которой являются формула $\rceil\rceil\forall xy(x=y)$, все формулы вида $\rceil A\vee\rceil\rceil A$ и все отрицания формул, выводимых в классическом исчислении предикатов. Библ. – 12 назв.
Образец цитирования:
В. П. Оревков, “Три способа выявления несущественных формул в секвенциях”, Исследования по конструктивной математике и математической логике. VIII, Зап. научн. сем. ЛОМИ, 88, Изд-во «Наука», Ленинград. отд., Л., 1979, 163–175; J. Soviet Math., 20:4 (1982), 2351–2357
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/znsl3110 https://www.mathnet.ru/rus/znsl/v88/p163
|
Статистика просмотров: |
Страница аннотации: | 219 | PDF полного текста: | 254 |
|