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.