| Speaker: |
Chad E. Brown Graduate Student Department of Mathematical Sciences Carnegie Mellon University |
|
| Title: |
Extensionality in Higher-Order Logic
|
|
| Abstract: |
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.