A KAPPA-DENOTATIONAL SEMANTICS FOR MAP THEORY IN ZFC PLUS SI

Map theory, or MT for short, has been designed as an ''integrated'' fo undation for mathematics, logic and computer science. By this we mean that most primitives and tools are designed from the beginning to bear the three intended meanings: logical, computational, and set-theoreti c. MT was originally introduced in [17]. It is based on lambda-calculu s instead of logic and sets, and it fulfills Church's original aim of introducing lambda-calculus. In particular, it embodies all of ZFC set theory, including classical propositional and classical first order p redicate calculus. MT also embodies the unrestricted, untyped lambda c alculus including unrestricted abstraction and unrestricted use of the fixed point operator. MT is an equational theory. We present here a s emantic proof of the consistency of map theory within ZFC + SI, where SI asserts the existence of an inaccessible cardinal. The proof is in the spirit of denotational semantics and relies on mathematical tools which reflect faithfully, and in a transparent way, the intuitions beh ind map theory. This gives a consistency proof, but also for the first time gives a clear presentation of the semantics of map theory in a t raditional framework. From the metamathematical point of view the stre ngth of MT lies somewhere between ZFC and ZFC + SI. The lower bound is proved in [17] by means of a syntactical translation of ZFC (includin g classical propositional and predicate calculus) into map theory, and the upper bound by building an (exceedingly complex) model of map the ory within ZFC + SI. The present paper confirms the upper bound by pro viding much simpler models, the ''canonical models'' of the paper, whi ch are in fact the paradigm of a large class of quite natural models o f MT. That all these models interpret a model of ZFC is a consequence of the syntactic translation, which is a difficult theorem of [17]. We can however give here a direct proof of a stronger result, namely tha t they interpret some (V-sigma, epsilon), where sigma is an inaccessib le cardinal. Finally we return to the ''canonical'' models and show th at they are adequate for the notion of computation which underlies MT.