05872261

a

05872261 Kaminski, Mark Smolka, Gert A finite axiomatization of propositional type theory in pure lambda calculus. Benzm\"uller, Christoph (ed.) et al., Reasoning in simple type theory. Festschrift in honor of Peter B. Andrews on his 70th birthday. London: College Publications (ISBN 978-1-904987-70-3/pbk). Studies in Logic (London) 17. Mathematical Logic and Foundations, 243-258 (2008). 2008 London: College Publications EN simply typed lambda terms set-theoretic type hierarchy pure lambda calculus propositional type theory Summary: We consider simply typed lambda terms obtained with a single base type $B$ and two constants $\perp$ and $\to$, where $B$ is interpreted as the set of the two truth values, $\perp$ as falsity, and $\to$ 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.