Ernest Schimmerling

Mathematical logic seminar - February 24, 2004

Time: 12 - 1:30 p.m.

Room: Wean Hall 7220

Speaker: Chad Brown
Graduate student
Department of Mathematical Sciences
Carnegie Mellon University

Title: Set Comprehension in Church's Type Theory (Part I)

Slides:

http://www.andrew.cmu.edu/~cebrown/papers/indep-mod-talk.pdf
Abstract: In order to prove theorems involving sets and functions, one often uses comprehension principles asserting the existence of certain sets. We explore the consequences of restricting which logical constants are allowed in these comprehension principles in the context of Church's type theory.

Church's type theory is a formulation of higher-order logic that allows quantification over sets and functions. In this logic, any set definable by an expression of the language can be proved to exist. This expressive power allows a natural formalization of much of mathematics.

The logical constants we consider are propositional connectives, equality and quantifiers over various types. For example, we consider fragments of Church's type theory which satisfy comprehension with respect to quantifiers over individuals, but not over sets of individuals. There are natural sequent calculi and corresponding semantics for any given signature. In some cases, adding logical constants to a signature does not increase the set of theorems (giving conservation results). In other cases, adding logical constants does increase the set of theorems (giving independence results). We establish these results using models of fragments of type theory.

For example, the usual proof of Cantor's theorem that there is no surjection from a set $S$ onto its power set $\pw(S)$ uses a diagonal set whose definition involves a negation. We construct a model showing that this theorem cannot be proven in a fragment of Church's type theory which lacks comprehension principles involving negation. To prove the version of Cantor's theorem that there is no injection from $\pw(S)$ into $S$ requires comprehension principles involving quantifiers over sets in $\pw(S)$ and equality of objects in $S$ as well as negation.

Organizer's note:     Please bring your lunch.