Архив публикаций

Тезисы

XIII-ая конференция

Секвенциальное построение теорий первого порядка

Кузичев А.С., Кузичева К.К.

МГУ им. М.В. Ломоносова, механико-математический ф-т, кабинет истории и методологии математики и механики; Россия, 119992, Москва, Ленинские горы; Тел. (095)9393860; e-mail: kuzichev-a.s@rambler.ru

Авторы, следуя идее ступенчатых конструкций А.Н. Колмогорова и А.А. Маркова, строят и исследуют секвенциальные исчисления, имеющие два яруса. Первый ярус задаёт неограниченное теоретико-множественное свёртывание Г. Кантора по А. Чёрчу в алгоритмической (вычислительной) форме исчисления ламбда-конверсии Чёрча; второй ярус задаёт классическую логику (предикатов 1-го порядка) в секвенциальной (без постулируемого логического правила сечения) форме Г. Генцена; связь между ярусами обеспечивают правила ламбда-сечения *ламбда и ламбда* (пишем: *ламбда*).

До 1980 года такие секвенциальные исчисления изучались прежде всего относительно арифметических свойств. В 1980–1987 гг. Колмогоров выделил общность предложенных исчислений как превосходящую теоретико-множественную и рекомендовал использовать аппарат исчислений для формализации и исследования теории множеств. Доклад содержит вариант реализации этой идеи Колмогорова.

В 1932–1933 гг. Чёрч использовал аппарат языка ламбда-конверсии для создания теоретико-множественных исчислений, образующих основания классической теоретико-множественной математики. Однако полученные исчисления гильбертовского (формульного) типа оказались противоречивыми (парадокс Клини–Россера 1935 года, парадокс Карри 1941 года).

После открытия парадокса Клини–Россера Чёрч разочаровался в своей программе в области оснований наук. Все известные попытки перестроить формульные исчисления Чёрча в доказуемо непротиворечивые или найти другой способ реализации программы Чёрча в виде исчислений гильбертовского типа к настоящему времени не привели к результату.

Более того, парадокс Карри, будучи только импликативным с тремя весьма естественными постулатами для импликации и свёртыванием в форме ламбда-конверсии, даже ставит под сомнение само существование таких (по программе Чёрча) исчислений гильбертовского типа.

В данной же работе секвенциальные исчисления (не гильбертовского, а генценовского типа) дают решение задачи Чёрча – доказуемо полную и доказуемо непротиворечивую формализацию канторовской теории множеств. Формулируется и доказывается соответствующая теорема о допустимости правила сечения.

Отметим, что все построения и доказательства проводятся формально по Гильберту.