 Second-order logic is an extension of classical quantificational logic in which we allow for quantification into predicate position. Second-order logic originated with Frege (1879), which developed a formal language equipped with predicate variables of the form \(X^{n}_{i}\). Predicate variables behave syntactically like \(n\)-place predicates of the form \(P^{n}_{i}\). In second-order logic, a predicate variable \(X^{n}_{i}\) followed by \(n\) variables \(X^{n}x_{1}, \ldots, x_{n}\) counts as an atomic formula. We finally let the quantifiers \(\forall\) and \(\exists\) bind predicate variables as in \(\forall X^{n}\, A\) and \(\exists X^{n}\,A\).