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

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

Под интуиционистской теорией множеств ZFI понимается система аксиом Цермело-Френкеля ZF, добавленная в качестве нелогической к интуиционистскому исчислению предикатов HPC, в которой, однако, аксиома регулярности - uÎv ®$x[xÎv Ù "y(yÎv®ØyÎx) ]- заменена аксиомой трансфинитной индукции: "x["y(yÎx®j(y)) ® j(x))]®"xj(x) - и отсутствует аксиома выбора, в противном случае, как показал Майхилл, получим теорию, формально равнообъемную классической ZF. Основные исследования в этой области ведутся с 70-х гг. прошлого века и касаются в основном совместности этой теории с дополнительными конструктивными принципами, такими как тезис Черча: "a$b j(a,b) ® $e"a$b(j(a,b)Ù{e}(a) = b), принцип Маркова: "a(j(a)ÚØ j(a)) ® (Ø"xj(a) ® $aØj(a)), принцип униформизации — при этом рассматривается обычно двусортная теория с интуиционистской арифметикой на первом уровне, а также аксиома двойного дополнения: "x$y["z (zÎy «ØØ zÎx)Ù"a (aÎy «ØØ aÎx)], и свойств эффективности теории, прежде всего дизъюнктивности (из  j Ú y следует  j или  y) и экзистенциальности (в случае стандартного языка теории множеств выглядит так: если  $yj, то найдется формула y, свободными переменными которой могут являться только свободные переменные формулы j - x1,...,xn, и переменная y, такая, что $y(j(y)Ù"z(zÎy®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.

Effectivity properties of intuitionistic set theory with arithmetic and constructive principles.

Intuitionistic set theory ZFI is the Zermelo-Frenkel axioms' system based on intuitionistic predicate calculus, with changing regularity axiom - uÎv ®$x[xÎv Ù "y(yÎv®ØyÎx)] for transfinite induction axiom - "x["y(yÎx®j(y)) ® j(x))]®"xj(x), and without axiom of the choice, against according Myhill we will have classic ZF. The main researches of this subject have been holding from 70s last century and generally are devoted to consistency this theory with the constructive principles, such as Church's thesis: "a$b j(a,b) ® $e"a$b(j(a,b)Ù{e}(a) = b), Markov's principle: "a(j(a)ÚØ j(a)) ® (Ø"xj(a) ® $aØj(a)), uniformization principle – in this case usually two-sorts theory with intuitionistic arithmetic on a first level is considered, also double completeness axiom"x$y["z (zÎy «ØØ zÎx)Ù"a (aÎy «ØØ aÎx)], and effectivity properties too, first of all disjunction property (if  j Ú y then  j or  y) and existentional property (for standart set theory language: if  $yj then there is a formula y, free variables of which can be free variables of j - x1,...,xn, or y, such as $y[j(y)Ù"z(zÎy®y(x1,...,xn, z))] ). In 1973 J. Myhill created a generalization of Kleene's realizability for proving some effectivity properties of ZFI. But his construction has uneffective character, hence it's unapplied for systems with Church's thesis. Also in 1973 H. Friedman using a modification of Kleene's realizability proved consistency intuitionistic set theory with Church's thesis, Markov's principle and uniformization principle, but without extentionality axiom. Then V. Khakhanian so changed this realizability, that extentionality axiom became realizable. Now we offer such variant of realizability that it will be able to prove the effectivity properties of intuitionistic set theory with Church's thesis and extentionality axiom too.

References:

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.