Is there any theorem achieving Conway's "Mathematician's Liberation Movement"

Question

John Conway on in the appendix to part zero of ONAG describes a "Mathematician's Liberation Movement". The goal would be to give mathematicians the freedom to create mathematical theories with the following two (soft) properties "

• Objects may be created from earlier objects in any reasonably constructive way
• Equality among the created objects can be any desired equivalence relation

" (pg 66)

In particular, these objects should be distinct from sets, and distinct from different kinds of objects. Conway gives the example that you could define $(x, y)$ and $[x, y]$, which would be distinct from each other and from any set. He also goes on to say that he is not looking for a specific alternative to ZF, but the ability to create such theories.

As an example, the theory of numbers would have the following axioms:

1. For any sets of numbers $L$ and $R$ such that $\lnot \exists l \in L. r \in R. r \le l$, we say that $\langle L, R \rangle$ is a number. Numbers are never equal to sets, since they are different kinds of objects.
2. $\langle L, R \rangle \le \langle L', R' \rangle \iff (\lnot \exists l \in L. \langle L', R' \rangle \le l) \land (\lnot \exists r' \in R'. r' \le \langle L, R \rangle)$
3. $\forall x. y. x = y \iff x \le y \land y \le x$ (this is the equivalence relation defining equality)
4. $(\forall L. R. (\forall l \in L. P(l) \land \forall r \in R. P(r)) \implies P(\langle L, R \rangle))$ implies $P(x)$ for all games $x$, where $P$ is any proposition. This is an induction scheme.

The movement would be considered successful once a meta-theorem proving all such theories to be relatively consistent to ZF.

My question is, is there such a theorem achieving this goal?

It actually does not look too hard, once you nail down the details, so to speak. It seems like most theories of the form need to use sets in some way, so we can just add the axioms of ZFC to its list of axioms. If classes are needed, we add NBG or KM. This lets us deal with sets. The object construction and induction axioms all take regular forms. You would have to check that equality obeys all the properties you expect equality to obey (substitution, is an equivalence relation). Then you can just take a model of ZF and represent objects as "tagged" sets. For example, $\langle L, R \rangle$ would be represented by $(1, L, R)$. A set $S$ in the theory would correspond to $(0,S)$ in the model of $ZF$. Then form the equivalence classes under equality, and bam: you have a model of the theory, and it is therefore consistent.

The hard part I think is nailing down the details of which theories should be considered, since Conway left it a little open ended.

Is there a theorem achieving Conway's "Mathematician's Liberation Movement"?

---

I think we can force the axioms to take some standard forms. Let $T$ be a theory. $T$ has relations $\in$ and $isSet$. Also proves the $ZFC$ (this could be changed to a different set theory) axioms, when restricted to sets. $T$ other axioms are described as follows:

1. $T$ has object defining axioms. An object defining axiom says $f(x, y, \dots, z)$ is defined if $P(x, y, \dots, z)$, for some proposition $P$ and function symbol $f$ ($f$ may be nullary, in which case it is a constant). If $T$ has axioms of this form, it must also include axioms stating that $f(x, y, \dots, z) \neq g(x, y, \dots, z)$ when $f$ and $g$ are different function symbols, and that the result of a function symbol is never a set.
2. $T$ should have an equality axiom for each function symbol $f$. This takes the form of $\forall x.y \dots z. P(x, y, \dots, z, x', y', \dots, z') \iff f(x, y, \dots, z) = f(x', y', \dots, z') \text {(if both sides are defined)}$ for some proposition $P$.
3. An induction axiom for each proposition $P$ stating that given that $P$ is satisfied by the domain of a function symbol anytime its arguments satisfy $P$ (for each function symbol), and that $\forall S. (\forall x \in S. P(x)) \implies P(S)$, we may conclude that $\forall x. P(x)$. (Notice how we combined the induction axioms for all different objects.)

All axioms are one of the above. The only thing we have to do is make sure the equality axioms do not imply any contradictions (by violating the inference rules associated with equality).

This hopefully nails down some details. I hope I nailed them correctly.