Chad E. Brown
Department of Mathematical Sciences
Carnegie Mellon University
Extensionality in Higher-Order Logic
In 1940, Church introduced a formulation of higher-order logic based on simply typed lambda-calculus. Later, Henkin introduced a semantics for Church's type theory and proved completeness. The theorem proving system TPS (under development by Peter Andrews at CMU) is based on a fragment of Church's type theory known as elementary type theory. Church's type theory is extensional, while elementary type theory is not. In my talk, I will describe the difference between Boolean extensionality, eta-conversion, and functional extensionality. Then, I will indicate how Henkin semantics can be generalized to provide a complete semantics for elementary type theory, as well as intermediate fragments with varying degrees of extensionality.