  Propositional type theory, first studied by Henkin, is the restriction of
simple type theory to a single base type that is interpreted as the set of the
two truth values. We show that two constants (falsity and implication) suffice
for denotational and deductive completeness. Denotational completeness means
that every value of the full set-theoretic type hierarchy can be described by a
closed term. Deductive completeness is shown for a sequent-based proof system
that extends a propositional natural deduction system with lambda conversion
and Boolean replacement.
