 The alphabet of second-order logic is obtained by including the first-order one-sorted variables and adding relation variables that can be quantified.  As a result, in addition to the formula \(\forall x\varphi\) saying “for all individuals \(\varphi\) holds”, we have formulas \(\forall X\varphi\), \(\forall X^{2}\varphi\), etc. saying “for all properties, \(\varphi\) holds”, “for all binary relations, \(\varphi\) holds”, etc.