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