Publication details

Saarland University Computer Science

A Finite Axiomatization of Propositional Type Theory in Pure Lambda Calculus

Mark Kaminski, Gert Smolka

Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, pp. 243-258, College Publications, December 2008

We consider simply typed lambda terms obtained with a single base type B and two constants false and implies, where B is interpreted as the set of the two truth values, false as falsity, and implies as implication. We show that every value of the full set-theoretic type hierarchy can be described by a closed term and that every valid equation can be derived from three axioms with beta and eta. In contrast to the established approach, we employ a pure lambda calculus where constants appear as a derived notion.

Download PDF        Show BibTeX               


Login to edit


Legal notice, Privacy policy