We present several results concerning deductive completeness of the simply typed lambda-calculus with constants and equational axioms.
First, we prove deductive completeness of the calculus with respect to standard semantics for axioms containing neither free nor bound occurrences of higher-order variables. Using this
result, we analyze some fundamental deductive and semantic properties of axiomatic systems without higher-order variables and compare them to those of established logical frameworks like first-order logic and Church's higher-order logic.
Second, we present a finite higher-order equational formulation of Henkin's Propositional Type Theory (PTT) and prove its deductive completeness. We introduce a simple criterion which allows to reduce deductive completeness of
systems with axiomatically defined constants to completeness of simpler axiomatic systems, and present an application of this criterion to our
formulation of PTT.
Third, we prove the simply typed lambda-calculus both with and without eta-conversion complete with respect to general semantics. The result holds for systems with arbitrary axioms and constants.
Master's Thesis, Saarland University, 2006