|
Записки научных семинаров ЛОМИ, 1975, том 49, страницы 67–122
(Mi znsl2794)
|
|
|
|
Эта публикация цитируется в 1 научной статье (всего в 1 статье)
Финитное исследование трансфинитных выводов
Г. Е. Минц
Аннотация:
Рассматриваются $\omega$-выводы арифметических формул. В первой части строится примитивно рекурсивный оператор нормализации $E$. Он устраняет сечение не только из рекурсивно описанных выводов (то есть фундированных фигур), но также из произвольных (не обязательно фундированных) фигур, построенных из аксиом по правилам вывода. Это позволяет применить $E$ в теории моделей. Его применения в теории доказательств основаны на формализуемости основных свойств $E$ в примитивно рекурсивной арифметике.
Во второй части доказывается устранимость сечения в гейтинговской арифметике $HA^{\omega}+AC$ с аксиомой выбора для всех конечных типов. Формулировка, допускающая устранение сечения, использует термы, сопоставляемые выводам по методу Карри, Говарда,Жирара, Мартин–Лефа. Эти термы включаются в сами формулировки правил. В качестве одного из следствий получается консервативность
$HA^{\omega}+AC$ над $HA$. Библ. – 11 назв.
Образец цитирования:
Г. Е. Минц, “Финитное исследование трансфинитных выводов”, Теоретические применения методов математической логики. I, Зап. научн. сем. ЛОМИ, 49, Изд-во «Наука», Ленинград. отд., Л., 1975, 67–122
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/znsl2794 https://www.mathnet.ru/rus/znsl/v49/p67
|
Статистика просмотров: |
Страница аннотации: | 175 | PDF полного текста: | 96 |
|