Chantal Berline and Klaus Grue
Note: For the official version, consult Theoretical Computer Science. The pre-release presented here is close to the official version, but the notion of 'self-extensionality' has changed from the pre-release to the official version.
Map theory, or MT for short, has been designed as an ``integrated'' foundation 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-theoretic.
MT was originally introduced in \cite{grue92}. It is based on lambda-calculus 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 predicate calculus. MT also embodies the unrestricted, untyped lambda calculus including unrestricted abstraction and unrestricted use of the fixed point operator. MT is an equational theory.
We present here a semantic 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 behind 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 traditional framework. Furthermore, the proof seems to indicate that all ``big'' models of (a very weak extension of) lambda-calculus can be expanded to models of MT.
From the metamathematical point of view the strength of MT lies somewhere between ZFC and ZFC+SI. The lower bound is proved in \cite{grue92} by means of a syntactical translation of ZFC (including classical propositional and predicate calculus) into map theory, and the upper bound by building an (exceedingly complex) model of map theory within ZFC+SI. The present paper confirms the upper bound by providing much simpler models, the ``canonical models'' of the paper, which are in fact the paradigm of a large class of quite natural models of MT.
That all these models interpret a model of ZFC is a consequence of the syntactic translation, which is a difficult theorem of \cite{grue92}. We can however give here a direct proof of a stronger result, namely that they interpret some $(V_{\sigma},{\in})$, where $\sigma$ is an inaccessible cardinal.
Finally we return to the ``canonical'' models and show that they are adequate for the notion of computation which underlies MT.
Klaus Grue, April 18, 1996