A unifying principle for extensional higher-order logic

Abstract: "In higher-order automated theorem proving the extensionality of equality has not yet been satisfactorily dealt with. This situation is especially unsatisfying since higher-order logic without extensionality does not admit a natural set-theoretic semantics. In this paper we present a version of Smullyan's Unifying Principle for simple type theory with extensionality. This result can serve as a tool for the development of extensionally complete calculi that are well-suited for mechanization on computers, and furthermore enables us to give an elegant completeness proof for Henkin's original calculus."