|Time:|| 12 - 1:30 p.m.
Wean Hall 7220
|Speaker:|| Chad Brown
Department of Mathematical Sciences
Carnegie Mellon University
Set Comprehension in Church's Type Theory (Part I)
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
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.