 In  Section 1.2.1,  \(\nsim_{({o}{o})}, \lor_{(({o}{o}){o})}\), and the \(\Pi_{({o}({o}\alpha))}\)’s were taken as primitive constants, and the wffs \(\sfQ_{{o}\alpha \alpha}\) which denote equality relations at type α were defined in terms of these. We now present an alternative formulation \(\cQ_0\) of Church’s type theory in which there are primitive constants \(\sfQ_{{o}\alpha \alpha}\) denoting equality, and \(\nsim_{({o}{o})}, \lor_{(({o}{o}){o})}\), and the \(\Pi_{({o}({o}\alpha))}\)’s are defined in terms of the \(\sfQ_{{o}\alpha \alpha}\)’s.