[Prev][Next][Index][Thread]
A kappa-denotational semantics of Map Theory.
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
The following paper is now available by ftp and by WWW :
"A kappa-denotational semantics for Map Theory in ZFC+SI"
by Chantal Berline and Klaus Grue
It is a revised and considerably augmented version of a preprint which
circulated previously and was entitled "A simple consistency proof for
Map Theory, based on xsi-denotational semantics".
This has been added in the new paper :
A presentation of Map Theory and many motivations and intuitions ;
comprehensive treatment of the set-theoretic properties of the models
The proof of the computational adequacy of the canonical models ;
A comparison with Flagg-Myhill's system.
Furthermore, the consistency proof, which formerly followed a bottom-up
approach, has been considerably restructured.
The paper is available in .ps and .dvi versions on both of the
following sites :
1) WWW page (at DIKU in Denmark) :
http://www.diku.dk/research-groups/topps/personal/grue/consis960415.html
2) by ftp (in Paris)
site: ftp.logique.jussieu.fr
dir: pub/distrib/berline
file: MT-consist96.dvi.gz or MT-consist96.ps.gz
(get, then decompress with " gunzip filename.gz ").
berline@logique.jussieu.fr
grue@diku.dk
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}(= TCS 102). 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.