Speaker: 
Chad E. Brown Graduate Student Department of Mathematical Sciences Carnegie Mellon University 

Title: 
Extensionality in HigherOrder Logic


Abstract: 
In 1940, Church introduced a formulation of higherorder logic based on simply typed lambdacalculus. 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, etaconversion, 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.