Note: This page is currently under development; It might take me a couple of weeks years to get it into a semi-stable state.


Map theory is a foundational logic based on the untyped lambda calculus. It is foundational in the sense that it is of strength comprable to ZFC set theory. It is based on the untyped lambda calculus in the sense that it has the untyped lambda caluclus as a syntactic subtheory.

Map theory is also the logic that I have worked with in my doctoral studies, and since it is a very unknown logic, I have often found myself trying to explain it to the uninitiated, and, soon after, defending it too: Why on earth use that, when one can use set theory? Higher order logic? Constructive type theory? And so on. This page is an attempt to collect and comment on the state of map theory. Hopefully, after reading this, it will not seem so outrageous to consider map theory a logic worth studying.


The logic was first published by Klaus Grue in 1992, and is therefore a quite recent, as foundational logics go.