A STRONG MULTI-TYPED INTUITIONISTIC THEORY OF FUNCTIONALS

FARIDA KACHAPOVA
  • Journal of Symbolic Logic, July 2015, Cambridge University Press
  • DOI: 10.1017/jsl.2015.21

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.

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.

Read Publication

http://dx.doi.org/10.1017/jsl.2015.21

The following have contributed to this page: Dr Farida Kachapova