KnowledgeBase » SEMINAR » ID = 625

Bridges Between Set Theory and Type Theory

by Evan Moran
2003-2004

The main theme will be the interplay between the set-theoretic and the type-theoretic approaches to computer science (and to mathematics, in general), expanding on a few of the more theoretical topics that were introduced in the first segment of last week's seminar.

In particular, I'll take this opportunity to re-acquaint the audience with two constructions, mentioned last week, that connect set theory to type theory. The first of these is Aczel's elegant type-theoretic interpretation of the language of set theory. The second, Howe's (relatively) recent set-theoretic semantics of Martin-Lof-style type theory.

Over the course of the talk, I'll try to make the case that these constructions are more than just means of establishing consistency, that they are, instead, better thought of as bridges that link two rich logical systems, allowing mathematical material to flow in either direction.

[Also, as a way of suggesting that such connections are interesting, I'll offer three examples of fruitful (/ potentially fruitful) interactions between the two systems: (a) an isomorphism that allows axioms (even large-cardinal axioms) to be imported from set theory into type theory, (b) a (candidate for a) derivation of the dependent binary intersection type, and (c) the bidirectional sharing of libraries between HOL and Nuprl (mediated by set theory).]