Wow, this thread-starting business is pretty heady stuff. I've got a real-world application of the axiom of regularity (in ZF Set Theory). In an inventory database of parts, where we allow assemblies of parts, I need an algorithm to check that no-one inadvertently entered a part as part of itself in an assembly, or as a part of a part that is in the first part, etc. In other words, we can't have any membership cycles. We don't allow for any n.
It struck me that this problem is precisely what the axiom of regularity is trying to avoid in ZF set theory. I will quote that axiom here, as it appears in Suppes' Axiomatic Set Theory (for some reason, the ampersand AND isn't working, so I'll use the \land symbol):
So I interpret this to mean that for any nonempty set, any elements of A cannot themselves have any elements in common with A. So here's my algorithm for implementing this check in my database:
Let's say I run that algorithm on the following assembly data:Code:
boolean checks_out = TRUE;
For each assembly A[i]:
For each immediate component part x of A[i]:
For each immediate component part y of x:
If y in A[i] Then set checks_out = FALSE;
A consists of parts B, C, D, and E.
B in turn consists of F, G, and H.
H in turn consists of I, J, K, and A (here’s the oops).
Where would this algorithm flag the error? Well, you’d start with A. Its components are B, C, D, and E. Loop through each of those.
For B, it checks out that F, G, and H are not components of A.
For C, there are no components. Done.
For D, there are no components. Done.
For E, there are no components. Done.
The next assembly is B. Loop through its components.
For F, there are no components. Done.
For G, there are no components. Done.
For H, it checks out that I, J, K, and A are not components of B.
Here the algorithm stops, and it didn't flag the error.
So here's my question: does my algorithm really implement the check I need? Does it check to make sure the axiom of regularity is followed? Or do I need to alter it in some way? If so, how?