Talk by Klaus Grue, Edlund A/S, on Wednesday 17 February 2016 14:00-15:00 at DTU Lyngby Campus, Building 101, Room S10.
Map Theory axiomatizes lambda calculus plus Hilbert's epsilon operator. All theorems of ZFC set theory including the axiom of foundation are provable in Map Theory, and if one omits Hilbert's epsilon operator from Map Theory then one is left with a computer programming language.
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.
The talk presents a substantially simplified axiomatization of Map Theory which has been proved consistent in ZFC under the assumption that there exists an inaccessible ordinal (Theoretical Computer Science, Volume 614, 8 February 2016, Pages 1-62). The talk also reflects on how Map Theory may fit into mathematics, computer science and mechanical proof checking.
Elsevier allows free download of the paper until 18 February 2016. If you follow the link, you can also find a 5 minute AudioSlides presentation of Map Theory (to the right, a little down).
Host: Jørgen Villadsen, DTU Compute, AlgoLoG Section
All are welcome.