 The deductive system of second-order logic, presented first explicitly in Hilbert-Ackermann (Hilbert &amp; Ackermann 1938), is based on the obvious extension of axioms and rules of first order logic together with the Comprehension Axiom Schema, defined as follows: Suppose \(\phi(x_1,\ldots,x_n)\) is a second-order formula with \(x_1,\ldots, x_n\) among its free individual variables and the second-order variable R is not free in \(\phi\). Then the following formula is an instance of the Comprehension Axiom Schema: 