 The axioms for second-order logic supplement the axioms of classical quantificational logic with distinctive axioms for the second-order quantifiers. Call a predicate variable \(Y^n\) free for \(X^n\) in \(A\) if, and only if, no free occurrences of \(X^n\) lie within the scope of a quantification on \(Y^n\), \(\forall Y^n\) or \(\exists Y^n\):