As I indicate elsewhere, I do not aim to formally found mathematics but rather to provide a framework, for discussing mathematics, which can be expressed in terms of any half-way sensible foundation. (It should be noted that, since Gödel, we know that half-way sensible is as good as it gets.)
It remains that I do believe a foundation based directly on relations (the central abstraction by which I package foundations) should be possible. Classically, those working on foundations have felt the need to distinguish a set of values from the identity function on that set; consequently, they have felt the need to include sets as primitive entities in their foundations. Since one can implement pairs, relations and functions using sets, they have considered it superfluous to treat relations as primitive entities. However, by using the identity mapping on a collection of values as the way to identify that collection, I avoid the need for the set as a separate primitive entity: instead, the relation is the only primitive, with functions (or mappings), sets (or collections) and pairs as special cases of this (far more powerful) primitive.
In common with the variation among set theory axioms, we have a choice of
whether to restrict the values (which relations relate to one another) to only
allowing relations or allow some urvalues
(as opposed
to urelements for sets)
as well, which are not themselves relations. These might, for example, be the
real world entities our relations describe. We augment these with relations
as allowed values and only specify rules for defining relations where the
values are either relations or urvalues; the theory might admit of some less
restricted type like relation but not bound by these rules, as some set
theories include classes extending the notion of set beyond the rules by which
set has to be bound to avoid paradoxes.
Because relations are a richer foundation, they need some axioms with no direct parallel in set theory, or whose equivalents for set theory arise trivially. For example:
For any relation r there exists a relation s
(known as the reverse of r) for which, for all x and y, s relates x to
y
precisely if r relates y to x
.
For any relation s, there exists a relation r
for which, for all x, y: r relates x to y
precisely if, for all z, s
relates z to x
implies s relates z to y
and there does exist some
such z. (In my notation, r is (:s|) and we can use reversibility to obtain
(|s:) likewise. We can use specification, below, to extract the sets of fixed
points from these as the sets of right and left values.)
It is also necessary to specify certain properties of relations,
analogous to properties of sets referenced in some axioms, appropriately. A
relation r is empty
precisely if, for all x, y, r relates x to y
is false; it is thus non-empty
precisely if there exist some x, y for
which r relates x to y
is true. Two relations r and s
are disjoint
precisely if, for all x and y, r relates x to y and s
relates x to y
is false. A relation r is an identity
precisely
if r relates x to y
implies x is y
; a value x is said to
be in
a relation r precisely if r relates x to x, so identities serve
the rôle of sets in this theory. Indeed, the aim is to have the theory
identify the same things, as identities, as classic set theory identifies as
sets.
Some of what the classic set-theoretic formalisms specify in their axioms of set theory can be carried over, with only mild transposition, to a putative axiomatisation founded on relations:
Two relations r and s are equal precisely
if, for all x and y, the statements r relates x to y
and s relates x
to y
imply one another.
For
any relation r and any predicate P(x, y) – which may involve the
relation named by r but may not use the names r, s – there
exists a relation s for which s relates x to y
precisely if P(x, y)
and r relates x to y
. In short, if you can specify a restriction on the
values r relates to one another, r does have a sub-relation which abides by
it.
For any w, x, y and z there exists a relation r for
which r relates u to v
precisely if either u is w and v is x
or u is y and v is z
. (When w = x and y = z, this collapses down to
the usual set-theoretic axiom of pairing – which, in turn, yields the
existence of singleton sets when all four values are equal. When w = y and x
= z, we obtain the atomic relation w←x, which is indeed the singleton set
{x} when w = x.)
This is the axiom that insists that there is at least one infinite set. I see no special benefit in adapting this at all – the same assertion will do fine, albeit phrased as: there exists some identity A for which {monic (A:|A)} and {mapping (A|:A)} are distinct.
Other axioms of set theory suggest analogous, though different, axioms applicable to relations. My choice to have bulk actions take a relation and combine its left values, ignoring the right values save where some ordering or similar requirement is involved, leads to a natural re-statement of the axiom of union; and analogous thinking to one for choice:
For any relation r there exists a relation s for
which, for all x and y, s relates x to y
precisely if there exist
some w, z for which: r relates w to z and w relates x to y
. (As in set
theory, combining this with pairing enables pair-wise union, repeated use of
which yields arbitrary finite union.)
For any relation r for which r relates y to z
implies y is a non-empty relation
and r relates w to x and y to z
implies: either x is z and w is y; or w and y are disjoint
there is a
relation s for which, for all x, y, r relates x to y
implies there
exist unique u, v for which s relates u to v and x relates u to v
. (That
is: given any mapping whose outputs are disjoint relations, there is a
relation whose intersection with each output of the mapping is a
singleton. One of the set-theoretic forms is simply the special case of this
in which the mapping and its left values are all sets; the mapping is thus
(the identity on) a set of disjoint sets; the relation whose existence is
asserted is then a set containing exactly one member from each output of this
identity.)
What are we left with ? Choice has diverse alternate forms, including well-ordering and limitation of size; for now, I'll settle for the version of it given above, at least partly because it's an axiom I deeply mistrust, so am disinclined to spend much time on thinking about how to replace it. That leaves the axioms of infinity, power-set and foundation; the axiom schema of collection; and one variant or another on (not as restricted as separation) comprehension.
In set theory, Foundation (or Regularity) asserts that every non-empty set is disjoint from at least one of its members. One can transform this into an assertion that every non-empty relation is disjoint from at least one of its (left or right) values; or from at least one left value and from at least one right value. However, as I don't understand what rôle the axiom of foundation plays in set theory – what does it make work out right, that otherwise wouldn't ? – I'm not clear about what the correct alternative to it might be. I suspect it simply exists to preclude the existence of a set x = {x} or some similar un-grounded self-reference; if so, I suppose either of the suggested transformed versions just given should suffice.
The case of the power-set (the set of all sub-sets of a given set) gets a
bit tricky. First, I would replace discussion of the power-set with
discussion of the subsumes relation among its members: one relation,
r, subsumes
another, s, precisely if, for all x, y, s relates x to
y
implies r relates x to y
. One would like to define a relation,
whose name would naturally be subsume
, that relates r to s precisely in
this case; however, it is apt to be too big
, like a set of all
sets
. So, instead, for any relation r, we look at the restriction of
subsume whose values (left and right) are precisely the relations that r does
subsume, the sub-relations of r. When r is a set, these are its sub-sets and
the restriction of subsume is the super-set relation among them. So, although
a formal axiomatisation may well need to steer clear of subsume itself, to
avoid paradoxes, it likely can replace the power-set axiom with:
For any relation r there exists a relation s for
which s relates x to y
precisely if r subsumes x, r subsumes y and x
subsumes y
.
The important point of this axiom is that the subsume-hierarchy of
any relation's sub-relations is a relation, i.e. isn't too big
or otherwise excluded from the foundation, as subsume itself likely shall
be. Note that every relation subsumes itself (fatuously) and so is a fixed
point of each such subsume-hierarchy of which it is a (left or right)
value. Given that I use fixed-point of a relation
as the natural
extension of member of a set
(every member of a set is a fixed-point of
the identity on that set), the sub-relations of a relation are all in
its subsume-hierarchy.
The Zermelo-Fraenkel axiom schema of collection wants to say that if you feed the members of a set through a function and collect up the outputs, you get a set – but has to phrase it rather more carefully. My axiom of projection (above) is similar in effect once you've obtained the relation which would be the function the ZF axiom scheme is so careful to not mention explicitly. So it suffices to say that, given an identity relation r and a predicate P(x, y) – which, as for specification, may involve the relation named by r but may not use the names r and s – satisfying
x in r and P(x, y) and P(x, z)implies
y is z
there is a relation s for which, for all x, y, s relates y to
x
precisely if x is in r and P(x, y)
. We can then use projection
on s to recover r or on the reverse of s to obtain ZF's collection. It is
possible that the uniqueness constraint on P could be weakened, e.g. replacing
the pair of conditions above with for each x in r, {y: P(x, y)} is
non-empty and finite
or, modulo some careful wording, a set.
In other axiom schemes, collection is replaced by some variant on comprehension.
Naturally, naïve set theory's comprehension is problematic; however, it is essentially the specification I use in practice (outside this page's examination of possible axiomatisation) for what a relation is. A proper axiomatisation would need to take more care than that. Following the distinction some foundations make between sets and classes, we could perhaps specify some looser type than relation, which applies naïve comprehension while excluding quantification over this looser type (but allowing parameters of this type), to obtain entities of this looser type – while, at the same time, declining to allow use of this looser type as values for relations to relate to one another, save when they can actually be shown to be relations after all.
In NBG (von Neumann, Bernays and Gödel) comprehension takes the place of ZF's collection; and can be replaced by finitely-many specific instances of its immense generality, several of which translate, in the world of relations, into axioms about the admissibility of currying; these look a lot more promising than comprehension itself. Let's look at the specific instances:
Every set is a class. I'm not going to attend overly closely, here, to the distinction between relations (corresponding to sets) and whatever generalisation of them (closer to how I actually describe relations when wrapping some other foundation), so I gloss over this. Suffice it to say that the more general includes the more specific.
Every class has a complement relative to the
all-class (which is not a set). One can likewise take a relation r and define
its complement s by s relates x to y
precisely if r does not relate
x to y
. However, I would sooner use r does not relate x to y
as a
predicate to use (optionally in building up predicates for use) in
specification, to extract r's complement within some other
relation. This leads naturally into …
Which has a natural equivalent for relations, namely: given relations r and s, there is a relation t (known as the intersection of r and s) which relates x to y precisely if r relates x to y and s relates x to y. This naturally extends to finite intersections; elsewhere, I merrily presume that I can get away with a bulk action intersect which maps any non-empty relation, r, to a relation which maps x to y precisely if every left value of r relates x to y; and I entertain the potential extension of this to allow empty r, yielding an all-relation which relates x to y for all x, y. This is doubtless excessive in a true foundation.
This stipulates the existence of cartesian
products of classes. There is a limited sense in which a constrained
all-relation (A||B), which relates every right value of A to every left value
of B, is similar to a cartesian product, although it fails to fill its
rôle in a relational theory. Elsewhere, I define a cartesian product
mapping Rene which maps any relation r to a relation which relates u to v
precisely if u and v have the same right values as r and: r relates w to
x
implies w composes cleanly after (:v:{x}) with composite
(:u:{x})
, i.e. for all y, v relates y to x implies that there is some z
for which w relates z to y and u relates z to x; which can be summarised by
the slogan r(x) relates u(x) to v(x)
when r, u and v are functions and,
when every left value of r is a set, u(x) is in r(x)
. When r is a list
of two sets (i.e. a mapping ({sets}:|{0,1})), Rene(r) is a set of lists, each
of which maps 0 to a member of r(0) and 1 to a member of r(1). (At the same
time, when r is a mapping from a smooth manifold, taking each point to the
tangent bundle at that point, Rene(r) is the set of mappings from the smooth
manifold to, at each point, a tangent vector; the smooth members of Rene(r)
are thus the tangent-valued sections of the manifold.)
So an axiom asserting cartesian products would likely stipulate that Rene's output is a relation whenever its input is a suitable relation, for some suitability criterion.
One variant of this matches directly to my axiom
of reversibility, above; the other translates as standard currying, i.e. for
every relation r there is a relation s which relates x to y precisely if y is
non-empty and: for all u, v, w, r relates u to v and v relates x to w
implies y relates u to w
. (Note that applying this twice is not
necessarily an identity: if r relates x to the singleton a←b and relates
x to some other singleton c←d, then the twice-curried r will relate x to
a non-singleton relation which relates a to b and c to d.)
This has similar form to currying, albeit
somewhat hairier. I paraphrase the first variant as, for any relation r,
there exists a relation s which relates x to y precisely if x is non-empty
and: for all u, v, w, r relates u to v and v relates w to y
implies x relates u to w
. One might alternatively have s relate x to y
precisely if x is a singleton relation a←b and r relates u to some v
which relates b to y; both here and for currying I have tacitly united all
such singletons into a single relation.
The second re-bracketing axiom given for association I paraphrase to, for any relation r, yield a relation s which relates x to y precisely if r relates x to a relation that the preceding association transforms into y.
This follows from my axiom of projection, above, albeit via a use of reversibility and extraction of a set of fixed points using specification.
Given my interpretation of membership as fixed-point, this just asserts the existence of the fixed-point relation, which relates x to r precisely if r relates x to x. This is doubtless best specified only as a looser-than-relation entity, as is …
This asserts the existence of a universal identity, i.e. collection of all values.
The (by now) classical set theoretic foundations have been formalised in
several ways; most
famously, ZFC
(Zermelo-Fraenkel with the (highly suspect, IMO) axiom of (transfinite)
choice). The
related NBG (von
Neumann, Bernays and Gödel) axiomatisation looks more susceptible of
adaptation to a relation-grounded (rather than set-grounded)
formalism. Quine's New
Foundation
(NF) behaves nicely, especially when augmented
with urelements
(to produce NFU), which are non-set entities allowed as
members of sets, analagous to my acceptance that the theory should be able to
describe relations among things which are not themselves relations.
Contrast with Codd's rules for relational database management systems and the set-theoretic formulation of the relational model of the predicate calculus.
Written by Eddy.