 First, HP is explicitly second order on the right-hand side, involving, as it does, a second-order quantification over relations R; and HP is purely logical on the right-hand side. Here, the notion to be defined (the definiendum) is that of a relation R mapping the Fs 1–1 onto the Gs. This can be spelled out in purely logical terms: every F bears R to exactly one G, and every G is borne R by exactly one F. In symbols, this definiens reads as follows: 