Second-order logic is the extension of first-order logic obtained by introducing quantification of predicate and function variables. A first-order formula, say Fxy, may be converted to a second-order formula by replacing F with a dyadic relation variable X, obtaining Xxy. Existential quantification yields ∃X Xxy, which may be read "there is a relation that x bears to y." In general relation variables of all adicities are admissible. Similarly, quantifiable function variables may be introduced.

Semantics for the Second-Order Logic

A structure, with non-empty domain D, for a second-order language includes relation domains Rel_n(D) and function domains Func_n(D). In general Rel_n(D) C P(Dⁿ), where P(Dⁿ) is the power set of Dⁿ. Similarly, the function domains Func_n(D) are subsets of the collection of n-place total functions on D. Such second-order structures are...