MULTI-TYPED INTUITIONISTIC THEORY OF FUNCTIONALS

What is it about?

We construct a multi-typed intuitionistic theory with lawless functionals and show that it is equiconsistent with a classical typed set theory, where the comprehension axiom for sets of type n is restricted to formulas with no parameters of types > n. Thus, we contribute to the program of justifying classical mathematics from the intuitionistic point of view.

Featured Image

Why is it important?

Previously Beth models were created for languages with only two sorts of objects. Here we constructed Beth model for the language with many types of intuitionistic functionals. This model can have interesting applications, besides the consistency proof for our intuitionistic theory.