Map Theory


Map Theory is a foundation of mathematics built on top of untyped lambda calculus rather than first order predicate logic. Map Theory is constructed by taking a simple programming language (essentially untyped lambda calculus) and by adding Hilberts epsilon operator. All constructs of ZFC set theory (membership, negation, implication, and universal quantification) are definable as terms in ZFC, and all theorems of ZFC are provable in Map Theory. Map Theory is suited for reasoning about classical mathematics as well as computer programs. Furthermore, Map Theory is suited for eliminating the barrier between classical mathematics and computer science rather than just supporting the two fields side by side.  

Map Theory est en particulier le premier système consistant répondant à la problématique initiale de Church (1930). C'est à la fois un langage commun pour écrire des mathématiques ou des programmes, ou des mathématiques des programmes, et pour raisonner dessus.

Vient de paraître (Janvier 2016)

« A synthetic axiomatisation of Map Theory », C. Berline et K. Grue, Theor. Comput. Sci. 614, p.1-62,The paper presents a new axiomatization of Map Theory. The axiomatization has substantially simplified axioms and the paper proves the consistency of the axiomatization. Furthermore, the paper gives an enhanced introduction to Map Theory. For ease of reference the paper includes a detailed TOC, an index and several appendices.

DOI number 10.1016/j.tcs.2015.11.028. (Editor version). The published version is available for free in PDF until February 18, 2016. To get it, click http://authors.elsevier.com/a/1SI9u15DaHmBG-

A 5 minutes easy Audio slides presentation of Map Theory (needs loudspeakers !).

Can also be found on Grue's page : www.diku.dk/~grue/synthetic



Et précédemment :


« Map Theory » ( K. Grue , TCS 1992), est l'article fondateur de Map Theory. Il présente la première axiomatisation, précédée

d'une introduction très riche, donnant de nombreuses illustrations de son pouvoir de représentation (qui va en fait bien au-delà de ZFC), et de l'intérêt d' avoir mathématiques et programmation au même niveau. La dernière partie propose une preuve de consistance, mais de de nature très syntaxique et extraordinairement complexe.


« A kappa-denotational semantics for Map Theory » (C. Berline & K. Grue, TCS 1997), donne une preuve de consistance plus simple et plus conceptuelle, dont l'idée de départ est l'utilisation d'une version transfinie de la sémantique de Scott du lambda-calcul.