A STRONG MULTI-TYPED INTUITIONISTIC THEORY OF FUNCTIONALS

作者：Kachapova Farida^*

来源：Journal of Symbolic Logic, 2015, 80(3): 1035-1065.

DOI：10.1017/jsl.2015.21

• Intuitionistic theory
• lawless sequence
• creating subject
• Kripke schema
• Beth model
• forcing
• consistency
• truth predicate

In this paper we describe an intuitionistic theory SLP. It is a relatively strong theory containing intuitionistic principles for functionals of many types, in particular, the theory of the "creating subject", axioms for lawless functionals and some versions of choice axioms. We construct a Beth model for the language of intuitionistic functionals of high types and use it to prove the consistency of SLP.
We also prove that the intuitionistic theory SLP is equiconsistent with a classical theory TI. TI is a typed set theory, where the comprehension axiom for sets of type n is restricted to formulas with no parameters of types > n. We show that each fragment of SLP with types <= s is equiconsistent with the corresponding fragment of TI and that it is stronger than the previous fragment of SLP. Thus, both SLP and TI are much stronger than the second order arithmetic. By constructing the intuitionistic theory SLP and interpreting in it the classical set theory TI, we contribute to the program of justifying classical mathematics from the intuitionistic point of view.

• 出版日期2015-9