Свойства эффективности интуиционистской теории множеств, содержащей арифметику и конструктивнные принципы.

Понедельник, 15 октября, комната 106. Начало в 14:00.

Докладчик: Д.М. Смелянский (Москва).

Тема: Свойства эффективности интуиционистской теории множеств, содержащей арифметику и конструктивнные принципы..

Abstract

Под интуиционистской теорией множеств ZFI понимается система аксиом Цермело-Френкеля ZF, добавленная в качестве нелогической к интуиционистскому исчислению предикатов HPC, в которой, однако, аксиома регулярности - uv x[xv  y(yvyx) ]- заменена аксиомой трансфинитной индукции: x[y(yx(y))  (x))]x(x) - и отсутствует аксиома выбора, в противном случае, как показал Майхилл, получим теорию, формально равнообъемную классической ZF. Основные исследования в этой области ведутся с 70-х гг. прошлого века и касаются в основном совместности этой теории с дополнительными конструктивными принципами, такими как тезис Черча: ab (a,b)  eab((a,b){e}(a) = b), принцип Маркова: a((a) (a))  (x(a)  a(a)), принцип униформизации — при этом рассматривается обычно двусортная теория с интуиционистской арифметикой на первом уровне, а также аксиома двойного дополнения: xy[z (zy  zx)a (ay  ax)], и свойств эффективности теории, прежде всего дизъюнктивности (из   следует  или  ) и экзистенциальности (в случае стандартного языка теории множеств выглядит так: если  yто найдется формула  , свободными переменными которой могут являться только свободные переменные формулы x1,...,xn, и переменная y, такая, что y(yz(zyx1,...,xn, z) ). В 1973г. Майхилл в [2] построил обобщение штрих-реализуемости Клини, позволившее ему доказать ряд свойств эффективности для ZFI. Однако, его реализуемость носит неэффективный характер, что делает ее неприменимой к системам, содержащим тезис Черча. В том же 1973г. Х.Фридман в [1], используя модификацию реализуемости Клини, показал непротиворечивость интуиционистской теории множеств с тезисом Черча и принципами Маркова и униформизации относительно классической теории множеств, но без аксиомы объемности. Затем В.Хаханяну удалось так перестроить эту реализуемость, чтобы реализовать аксиому объемности, а также двойного дополнения, решив таким образом задачу, поставленную А.Г.Драгалиным. Цель настоящей работы - дать такую модификацию реализуемости Майхилла, которая позволит доказать свойства эффективности для интуиционистской теории множеств с тезисом Черча, сохраняя реализуемость аксиомы объемности. Ссылки: 1) Friedman H. Some applications of Kleene's methods for intuitionistic Systems. - Lect. Notes Math., 1973, N 337. 2) Myhill J. Some properties of intuitionistic Zermelo-Frenkel set theory. - Lect. Notes Math., 1973, N337.