ZF can be viewed as theory that possess a uniform representation of relations,
i.e. for each relation R either all classes of ordered pairs representing it are
sets or all of them are non sets.
In order to understand this principle we'll work within a theory that defines
classes, for example a fragment Z* of NBG that is a conservative extension of Z.
For example one having all axioms of NBG except "limitation of size axiom" or
in recent formulations except "Replacement scheme over sets", and then we add
Separation schema over sets.
Sets are defined as:
Q is a set<-> Exist x For all m (m in x <-> m in Q)
Now we come to define the predicate "is an ordered pair function" as:
Definition: F is an ordered pair function <->
For all m in F Exist a,b,c (m=(a,b,c)) ^
For all a,b Exist c ((a,b,c) in F) ^
For all (a,b,c),(d,e,f) in F [c=f <-> a=d ^ b=e]
where (a,b,c) is some specific ordered triplet, like for example
(a,b,c)={{1,{a}},{2,{b}},{3,{c}}} where 1 is the empty set, 2={1,{1}} and
3={1,{{1}}}.
Define: c is an ordered pair <->
Exist F,a,b (F is an ordered pair function ^ (a,b,c) in F)
Define: c is an F_ordered pair <->
F is an ordered pair function ^ Exist a,b ((a,b,c) in F)
Define: a is the 1st F_projection of c <->
F is an ordered pair function ^ Exist b ((a,b,c) in F)
Define: b is the 2nd F_projection of c <->
F is an ordered pair function ^ Exist a ((a,b,c) in F)
Definition: Any two ordered pairs p,q as said to be (F,G)_equivalent,
if and only if p is an F_ordered pair ^ q is a G_ordered pair ^
for all a (a is the 1st F_projection of p <-> a is the 1st G_projection of q) ^
for all b (b is the 2nd F_projection of p <-> b is the 2nd G_projection of q)
Define (relational class): R is a relational class <->
Exist F [F is an ordered pair function ^ For all m in R (Exist a,b ((a,b,m) in F))]
Define: R is F_relational class <->
F is an ordered pair function ^ For all m in R (Exist a,b ((a,b,m) in F))
Definition: Two relational classes R,S are said to be equivalent, denoted by R==S,
if and only if Exist F,G (R is F_relational class ^ S is G_relational class ^
For all r in R Exist s in S (r,s are (F,G)_equivalent) ^
For all s in S Exist r in R (s,r are (G,F)_equivalent).
Informally two equivalent relational classes are taken to constitute
representations of the same relation.
Are we justified in using images of any ordered pair function as defined above to
implement relations in the above manner?
The answer is yes, because it can be proven in Z* that for any classes A,B and any
formula R(x,y) having x and y free, then there exist a class of all F ordered pairs
(x,y) such that x R y. Not only that we can also prove in Z* that for any relational
class R there is a domain of R class and a codomain of R class; all those are
straightforward consequences of the axiom schema of class comprehension of Z*, and
that's all what is needed in order to justify the use of any ordered pair function in
implementing relations.
Axiom of uniformity of relations:
For all relational classes R,S [R==S -> (R is a set -> S is a set)]
This axiom when added to Z*, then the result is NBG.
This clearly motivates Mathias's argument about abstractness of the ordered pair
data type implying replacement, in other words that the internal implementation
dependent properties of ordered pairs must not affect set implementations of relations
after using them. Since if for example there could exist two relational classes R,S
that are equivalent (i.e. both represent the same relation) but one is a set while the
other is not a set, then this mean that the internal implementation dependent detail of
the pairs used did matter! since it affected the set implementation of relations using
them, which is undesirable.
The whole story began with Adrian Mathias's amusing observation, He says:
"Of course, we all know the abstract specification of a pair.
A pair is a binary operator P such that for any x; y; z;w, if P(x, y) =
P(z,w) then x = z and y = w.
Now we argue that of course the details of the internal implementation
of a pair should not matter. So any operator P with the indicated property
should work as an ordered pair and be effectively interchangeable with the
usual one.
But this last assertion is extremely strong. In fact, in the context of
Zermelo set theory, the claim that pair implementations should be inter-
changeable implies the axiom of replacement"
That was Mathias's own words (quoted from Holmes).
Holmes had objected to that saying that:
"A pair is a binary operator P such that for any x; y; z;w, if P(x, y) =
P(z,w) then x = z and y = w, and further for any relation R with domain
a set A and codomain a set B {P(x, y) : x in A ^ y in B ^ xRy} is a set,
and further for any set C, the set of all x such that for some y, P(x, y) in C
and the set of all y such that for some x, P(x, y) in C exist"
Accordingly Holmes calls an operator that just satisfy the first property as a
"two-element list" while an operator satisfying all above properties as an
"ordered pair", and he argues that those are separate abstract notions. And
therefore there is no conceptual justification for using two-element list operators
for the general implementation of relations.
However Holmes argument is carried out in the context of Zermelo's set theory,
which is admittedly the context of original argument. However that doesn't mean that
Zermelo is the only context in which this argument can be presented, actually if we
argue in the context of Z* (mentioned above) then we gain additional expressive power
although Z* do not confer additional strength over Z as far as what it says about sets
of it, since it is just a conservative extension of Z, however Z* provides more
expressive grounds for speaking about relations than does Z, and this is clear from
the above definitions of ordered pairs functions, relational classes, general
definition of equivalence between ordered pairs as well as between relational classes,
all those are much easily formalized using classes and they do present the abstractness
notion of Mathias argument in a very distinctive manner. Not only that classes increase
the realm of extending relations in the object world and since there is nothing in the
abstract definition of relations per-se that pertains to them being implemented just by
sets, and since class implementations of relations is a very well known practice then
we might as well call classes in, accordingly the extensional coverage of relations
would increase. This results in showing that EVERY two-element list set operator works
as an ordered pair operator exactly as Holmes intended them to be but within the class
realm (in the context of Z*), so the apparent gap between those in the context of Z
would be bridged by just adding class machinery. Saying that I think it is perfectly
legitimate to speak about Mathias's argument in the context of Z*. So in that context
clearly if we are to hold that the choice of an ordered pair operator must
be immaterial in implementing relations in the set realm (which is Mathias stance),
then this translates exactly into the above Uniformity axiom and this proves
replacement.
So the addition of classes did revive Mathias argument.
Best Regards,
Zuhair Al-Johar