Publication details

Saarland University Computer Science

Completeness Results for Higher-Order Equational Logic

Mark Kaminski

Master's Thesis, Saarland University, December 2006

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


Webmaster, Wed Sep 16 10:47:00 2009