A simple semantic consistency proof for Map Theory
based on $\xi$-denotational semantics
by Ch. Berline and K. Grue
berline@logique.jussieu.fr
grue@diku.dk
Map theory, which is a foundation of mathematics based on lambda-calculus instead of logic and sets, has been introduced in [Grue, TCS 102(1), 1992].
Map theory is an equational theory which embodies predicate calculus; from the metamathematical point of view its strength lies somewhere between ZFC and ZFC+SI , where SI asserts the existence of an inaccessible cardinal.
The first result is proved in [G] by means of a syntactical translation of ZFC (including classical predicate calculus) within map theory, and the second by building a model of map theory within ZFC+SI. This latter construction is however highly technical, though the starting intuitions are quite natural.
We present here a semantic proof of the consistency of map theory within ZFC+SI, which 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 paper (submitted) is now available on the WWW . and by anonymous ftp, either in GNU-compressed form . or as a non-compressed dvi or Postscript file.