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
Download PDF Show BibTeX
Login to edit