The Type Base and Undecidability in Type Theory
by Abhishek Anand
Location: 12:05-1:00, 215 Upson Hall
In this talk, I would talk about the new type Base which was introduced to NUPRL a few years ago. This type contains all the terms of the underlying computation system and equality is based on a notion of observational equivalence. Then, I will show how it let's us express undecidablity in an elegant way. This construction is similar to an earlier construction which was based on bar types. These results prevent us from doing classical logic the way we did earlier - by introducing a "magical" decider for the law of excluded middle. I will show how to get around this problem.