Ernest Schimmerling

Mathematical logic seminar - March 2, 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 II)

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.

To ensure completeness, a higher-order theorem prover must ensure that instantiations for sets definable using logical constants can be discovered. In the presence of extensionality, one can make several restrictions to the set instantiations necessary without sacrificing completeness. For example, one can restrict the logical constants available for set instantiations. Also, one can assume set instantiations are in a prenex conjunctive normal form.

The theorem prover TPS has traditionally been used to search for theorems provable without using extensionality. TPS has now been updated to include search procedures appropriate for extensional type theory. I will describe the search procedure and give examples of theorems of extensional type theory which TPS can now prove.

Organizer's note:     Please bring your lunch.