Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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               

@INCOLLECTION{KaminskiSmolka08ptt,
  title = {A Finite Axiomatization of Propositional Type Theory in Pure Lambda Calculus},
  author = {Mark Kaminski and Gert Smolka},
  year = {2008},
  month = {Dec},
  editor = {Christoph Benzm{\"u}ller and Chad E. Brown and J{\"o}rg Siekmann and Richard Statman},
  publisher = {College Publications},
  booktitle = {Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday},
  pages = {243-258},
}

Login to edit