# Publication details

##
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

Legal notice, Privacy policy