A.G. Vladimirov

Effecivity Properties of Intuitionistic Set Theory

Let us consider two-sorted intuitionistic set theory ZFI2 with sort 0 for natural numbers and sort 1 for sets. We shall show that well-known Church rule with parameters of sort 1 is admissible in ZFI2 in some rather strong sense, and get from this point the admissibility of Markov rule with all parameters in ZFI2, and also DP and numerical EP with set parameters for it in the same sense.