[an error occurred while processing this directive] An error occured whilst processing this directive

LFCS Seminar


Negative Type Theory

Thomas Forster

University of Cambridge

4pm Tuesday 29th April 2008
Room 2511, JCMB, King's Buildings


Abstract

Russellian simple typed set theory, as simplified and modified by Carnap and Quine, is a many-sorted theory with a family of formally disjoint types of sets - indexed by the naturals - with a type of atoms and each subsequent type being formally the power set of its predecessor. A natural extension is the type theory (`TNT') where the types are indexed by the (positive and negative) integers. This theory, although manifestly consistent because of compactness, is highly pathological in various interesting and unexpected ways. It has no standard models. and it is not known whether or not it has omega models. Can it have countable models in which every element is the denotation of a closed term?

This historically motivated survey will attempt to bring the sophisticated beginner up to speed in this interesting backwater.


An error occured whilst processing this directive