announcement: consistence of Map Theory
A simple semantic consistency proof for Map Theory based on
Ch. Berline and K. Grue
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
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 by anonymous ftp or by WWW.
ftp host: boole.logique.jussieu.fr
(to get the .dvi file uncompress by command "gunzip")
ftp host: ftp.diku.dk
filename: consist.ps or .dvi
World Wide Web (WWW):