 Tarski (1923) noted that in the context of higher-order logic, one can define propositional connectives in terms of logical equivalence and quantifiers. Quine (1956) showed how both quantifiers and connectives can be defined in terms of equality and the abstraction operator λ in the context of Church’s type theory. Henkin (1963) rediscovered these definitions, and developed a formulation of Church’s type theory based on equality in which he restricted attention to propositional types. Andrews (1963) simplified the axioms for this system.