# Negative Type Theory

Thomas Forster University of Cambridge 4pm Tuesday 29th April 2008 Room 2511, JCMB, King's Buildings

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.