A kappa-denotational semantics for Map Theory in ZFC+SI
Chantal Berline and
Klaus Grue
The paper is available via WWW in PDF, PostScript.gz
and .dvi.gz.
Abstract
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