On Sep 30, 7:37*pm, David BL <davi... (AT) iinet (DOT) net.au> wrote:
May I suggest that the problem is the set theory foundation -- the set
membership operation? After all, one can't possibly think of the least
pretty operation from algebraic perspective. Contrast it to
intersection, union, and (relative) complement -- which form Boolean
algebra on a powerset.

On Sep 30, 9:17*pm, David BL <davi... (AT) iinet (DOT) net.au> wrote:
In RM the level of curly brakets nesting never goes higher than two,
so set theory paradoxes are irrelevant.

Isn't a binary operation on powerset boolean algebra?

On Oct 2, 1:08 am, Tegiri Nenashi <tegirinena... (AT) gmail (DOT) com> wrote:

Let R(T) be the set of all relations where every attribute has domain
T. For any set T, R(T) exists in ZFC (largely by virtue of the axiom
of power set).

Let X be the union of R(T) over all possible T. The definition of X
involves unrestricted comprehension and I don't think it exists under
ZFC.

It seems to me one can study R(T) as an algebraic structure - say with
the relational lattice operators, and to the extent that T is not
specified (but assumed to be a union type big enough to hold all
values of interest) it actually can be regarded as an untyped
treatment of the RM.

Does this make sense?

I'm not sure how RVAs fit into that picture. I think recursive types
should be allowed, but any given relation (value) only involves finite
nesting.


Yes.

As I see it, if one has an operator defined on a proper class, one can
take a restriction to a domain which is a set (i.e. a subset of the
proper class) to make the operator into a function.

Here is a discussion of "proper class":

http://en.wikipedia.org/wiki/Class_(set_theory)