|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 II)
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.
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.