left and right euclidean;
Given an extensional relation on a set, two elements are equal if they cannot be distinguished by the structure of the set of elements that they are related to, that those elements are related to, and so on forever in one direction. We generally think of as saying that is a ‘member’ of , so that is extensional when “ is determined by its members“ as in the axiom of extensionality for material set theory.
We begin with the historically first definition, which is correct for well-founded relations. We then consider ways to extend this to more general relations, where the last version seems to be most correct.
A relation on a set is weakly extensional if, given any elements and of , whenever (for all ) if and only if .
Interpreting as membership , this corresponds to the axiom of extensionality as usually stated for pure sets. However, it is really only appropriate when is well-founded, just as the usual axiom of extensionality must be strengthened in the absence of the axiom of foundation.
However, when is well-founded, weak extensionality is equivalent to all the stronger notions below; thus in that case it is usually called just extensionality.
with . Note that itself belongs to (through , if in no other way), so we may take it to be a pointed set. Then is Finsler-extensional if it is weakly extensional and, given any elements and of , whenever and are isomorphic as pointed sets equipped with a relation .
Note that this definition includes weak extensionality, which won't follow from the other half unless is well-founded (see the examples below). It is possible to get weak extensionality free by using the transitive closure instead; that is, define with only. But then you need another step; define to be a pointed set with a new point adjoined to ; let if and only if in itself. (For a well-founded relation, ; in general, however, may already belong to , yet in .) Then is Finsler-extensional on if and only if whenever as pointed sets equipped with .
It is immediate that Finsler extensionality implies weak extensionality; the converse may be proved (using induction) for well-founded relations.
Given an element of , let a path to consist of a sequence
for . Then let be the set of paths to ; given paths and in , say that if for some . Then with the relation is the tree to .
Then Scott extensionality implies Finsler extensionality, and the converse holds for well-founded relations.
Let be equipped with a binary relation . A bisimulation on is a binary relation such that whenever , for any there is a with , and conversely for every there is an with again . We then say that is strongly extensional if every bisimulation is contained in the identity relation; i.e., whenever for any bisimulation . In general, this is probably the best situation in which to say that is simply extensional.
Finsler and Scott extensionality may be understood as special cases of this for particular bisimulations . (So can strong extensionality, since any set equipped with a relation has a weakest bisimulation .) This is the approach taken by Aczel to study all the above notions of extensionality together.
In particuar, strong extensionality implies Scott extensionality, and the converse holds for well-founded relations. Thus, all forms of extensionality are equivalent for well-founded relations.
The axiom of extensionality in material set theory states membership is an extensional relation on the class of pure sets. (Note that the axiom of foundation states that membership is a well-founded relation, so one usually doesn't worry about the different notions of extensionality for ill-founded relations.) More generally, the membership relation on the transitive closure or reflexive-transtive closure of a pure set is an extensional relation on a set.
On the set , now let and (but no other relationships). This relation is not weakly extensional, although it does satisfy the other half of Finsler extensionality, since . However, ; this shows the necessity of defining Finsler extensionality as we do.
On the set again, let and (but and ). This relation is weakly extensional but not Finsler-extensional, since . Yet and can hardly be distinguished by when there is an automorphism of that swaps them; this and the other examples below motivate the stronger notions of extensionality.
On the set , let and but all other relationships hold. Then this relation is Finsler-extensional but not Scott-extensional, since .
Finally, on the set again, let but all other relationships hold. Then this relation is Scott-extensional but not strongly extensional, since .
Now suppose that if if and only if for all , then if and only if for all . Then if we define to mean that and , then is an equivalence relation such that descends to a weakly extensional relation on the quotient set .
Strongly extensional quotients are even easier to construct, although they do create additional relationships. It is easy to see that the union of any family of bisimulations is a bisimulation, and therefore there is a largest bisimulation for any binary relation on . Moreover, is an equivalence relation (though not every bisimulation need be so), and descends to a strongly extensional relation on the quotient .
Note that there is at most one simulation from to ; in fact, strong extensionality for is equivalent to saying that any two simulations are equal. Also, any simulation from to must be an injection; in fact, strong extensionality for is equivalent to saying that any simulation is injective.
Thus, we have a (large) poset of sets equipped with extensional relations, and we can consistently interpret the simulations as subset inclusion. This leads to the model of sets equipped with extensional relations as transitive sets.