KnowledgeBase » SEMINAR » ID = 699

The Type Base and Undecidability in Type Theory

by Abhishek Anand
2012

Location: 12:05-1:00, 215 Upson Hall

Abstract
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.