Note: This page is currently under development; It might take me a
couple of weeks
years to get it into a semi-stable state.
Introduction
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.
History
The logic was first published by Klaus Grue in
1992, and is therefore a quite recent, as foundational logics go.
People
Slides