Information Modeling and Relational Databases, 2nd Edition

10.7. Higher-Order Types

This section evaluates the advisability of using higher order types in information models. We first review some basic concepts from logic. First-order logic quantifies over individuals only, not predicates. For example, the constraint “Each Person was born on at most one Date” may be formalized in first-order typed logic thus:

∀x:Person ∃^0..1y:Date x was born on y

Here the types Person and Date appear as unary predicates, “∀” is the universal quantifier (“for each”), and “∃^0..1” is the “there exists at most one” quantifier. The quantification is over individual people and individual dates. First-order predicates may be instantiated only by individuals. Second-order logic allows quantification over first-order predicates ...