Given a binary relation R, the ancestral of R, denoted by R*, is the binary relation which holds between objects a and b iff there is a chain a = x1, x2,..., xn = b such that Rxixi+1 for i = 1,..., n − 1. The following is Frege's celebrated definition of the ancestral relation in second-order logic:
R*ab ↔ for every R-hereditary P (for all x (Rax → Px) → Pb),
P is R-hereditary ↔ for all x, y (Px and Rxy → Py).
A unary predicate P is R-hereditary if it is "transmitted" from a given object to its children. a is then an ancestor of b iff every R-hereditary property of the children of a is also a property of b. An interesting aspect of this clever definition is its apparent circularity: the property of being a descendent of a, which is represented by R*a, the unary predicate obtained from R* by fixing the first argument to a, is R-hereditary and true of a's children. The following exposes even more clearly the relationship between R* and its definition clause:
Q is R-compatible ↔ for all x, y, z ((Rxy → Qxy) and (Qxy and Ryz → Qxz)).
Again, R* is R-compatible, and any R-compatible relation must hold for at least the pairs xy for which R* holds; this is a particular example of the following definition schema for some binary relation S:
where ΦS is a formula with a binary relation free variable. We might call ΦS a core formula for S; in a sense, S is the "miminum" relation satisfying ΦS. For instance, a core formula for the equality relation is
Φ=(Q) := for all x (Qxx),
a = b ↔ for all Q (for all x (Qxx) → Qab),
which can be interpreted as the statement that = is the minimum reflexive relation; this definition looks more conservative than the customary Leibniz's Law used to define equality in second-order logic.
Any binary relation definable in first-order logic, i.e. for which there is a first-order definition formula φ(x,y) such that
Sab ↔ φ(a,b),
has a core formula: take ΦS(Q) := for all x,y (Qxy ↔ φ(x,y)). The converse, however, is not true: for instance, neither R* nor = are definable via first-order formulas.