On certain types of binary relations

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 = x₁, x₂,..., x_n = b such that Rx_ix_i+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:

R^*ab ↔ for all R-compatible Q (Qab)
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:

Sab ↔ for all Q (Φ_S(Q) → Qab),

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),

that is,

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.