# A rough sketch of a foundation

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:

reversibility

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.

projection

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:

extensionality

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.

specification, separation or restricted comprehension

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.

pairing

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

Infinity

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:

union

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

choice

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.

### Foundation

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.

### Power-set

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:

subsume

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.

### Collection

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

• for each x in r, there exists a y for which P(x, y)
• for all x, y, z, 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.

### 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.

#### Finitely many comprehensions

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:

Sets

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.

Complement

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 …

Intersection

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.

Products

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.

Converse

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

Association

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.

Ranges

This follows from my axiom of projection, above, albeit via a use of reversibility and extraction of a set of fixed points using specification.

Membership

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 …

Diagonal

This asserts the existence of a universal identity, i.e. collection of all values.