Tuesday, April 04, 2006

Anti-Foundation and Strong Extensionality

Barwise and Moss's Vicious Circles is about the Anti-Foundation axiom, an alternative to the usual axiom of foundation in set theory. I had a look at various online introductions to this subject and they all seem a bit long winded. So here's my own quick summary pared down to the bare minimum. (I sacrifice a bit of accuracy along the way but it should be enough to give a feel for the subject.)

Firstly: the whole point of the Axiom of Foundation is to eliminate infinite chains of membership. So the Axiom of Foundation says that there are no infinite descending chains:

...∈A3∈A2∈A1∈A

(I hope you can read that, I'm using this list.)

The kind of thing that the Axiom of Foundation eliminates are sets x such that x∈x. It means we can define functions inductively over sets as we're always guaranteed to have a base case to start the induction. More generally imagine a system of equations such as

x = {x,y,z,4}
y = {x,z,2}
z = {{3},x,y}

The Axiom of Foundation rules out any solution to this. The Axiom of Anti-Foundation, on the other hand, says that any set of equations like this, with unknowns on the left, and sets containing those unknowns on the right, has a unique solution. (Note that the containing in that sentence is essential, x = x doesn't have a unique solution.)

And that's it, the Axiom of Anti-Foundation.

But there's a slight problem. Consider the equation x = {x} and the equation pair y = {z}, z = {y}. The solution to the first equation seems like it ought to be the solution to the second as well. But we have no way of telling this. In fact, there are issues just telling whether or not the sets x = {x} and y = {y} are equal. Normally in set theory we'd use the Axiom of Extension. Two sets are equal iff their elements are equal. So in this case we have x = y iff their elements are equal, ie. iff x = y. So the Axiom of Extension tells us nothing here. We need a new kind of Extension.

The idea is to find something like an isomorphism between two sets. For example, define f(x) = y for our last example above. Notice that for every element x' of x, there is an element y' of y such that f(x') = y'. f also has an inverse. It's a bit trivial in this case but it's a start. But suppose we compare the set x defined by x={x} with y defined by y={z} and z = {y}. We want some kind of isomorphism that maps x to both y and z. And with more complex sets of equations there might be any number of elements of one set that we need to map to any number of elements in the other. So what we need isn't a function but a relation connecting elements in one set to the other. The relation R is said to be a bisimulation between sets a and b if

aRb
for all a'∈a there exists a b'∈b such that a'Rb'
for all b'∈b there exists an a'∈a such that a'Rb'

If two sets are related by a bisimilarity then it can be shown that they satisfy the same equation and hence by the uniqueness of solutions they must be the same set. This property is known as Strong Extension. (I've paraphrased this from the original but I think it's essentially correct.)

And that's it - you can now go off and make your own non-well founded sets and compare them for equality.

I should add some interesting connections with computer science. Bisimulations are more familiar as a relation holding between automata. The usual Axiom of Extension gives a recursive definition of equality. Recursive definitions require a base case and with a base case we can get inductin proofs started. Without base cases we have corecursion instead and have to use a different proof technique, coindunction, whose main tool is bisimilarity.

Another interesting link with computer science is through F-algebras and F-coalgebras. I mentioned that F-algebras and F-coalgebras may have initial and final objects so that there is an isomorphism X≅F(X). The Axiom of Anti-Foundation often allows us to make the isomorphism equality. For example it's not hard to see that for a finite state automaton we can make a state simply equal to the set of transitions available from that state. In fact, that gives a nice way to answer the question I was originally asking in that earlier posting - how can I remove the labelling of the states and leave just the bare information about what transitions take me where?

And one important thing I should add - you can make a model in ZF for set theory with Anti-Foundation and Strong Extensionality. So it's consistent if ZF is. Additionally, Barwise and Moss also work with urelements, elements of sets that are not the empty set and yet contain no elements. I'm not sure, but I don't think these are essential to making sense of Anti-Foundation. Anti-Foundation, as described by Barwise and Moss, does make use of urelements in the definition of an equation (in particular to label the 'unknowns') but I think Anti-Foundation can be rewritten so as not to use urelements.

Update: I originally stated that Strong Extension was an axiom which it isn't. Just to add to the confusion, the Axiom of Anti-Foundation that I described above is called "The Solution Lemma" in Vicious Circles, even though it is an axiom.

9 comments:

Kenny said...

The presentation I had seen about anti-foundation talked about directed graphs rather than systems of equations, but I think it works approximately the same.

Also, I believe the fact that anti-foundation says the solution is unique guarantees strong extensionality as a theorem. For instance, any solution to x={x} is also a solution to y={z} and z={y}, and since this is a solution, it must be the unique one.

Anyway, since I saw it in terms of directed graphs, I assume that you can just represent all these things as directed graphs within ordinary ZF, so you don't need urelements. And the consistency result is actually an equivalence - ZF is consistent iff AFA is, because you can start with any model of AFA and consider the subclass of well-founded sets, and they will satisfy ZF.

Anyway, it's neat to see the bisimulation stuff! I had only run into bisimulation in terms of frames for modal logic, so it's neat to see that the same relation works here to prove that two sets of equations have the same solutions.

Jacobian said...

This looks similar to unification over rational trees. In the case of rational trees we are dealing with labeled directed graphs rather than simply directed graphs. Unifying over rational trees is nice because you can directly represent cyclic structures in logic programming.

In the case of rational trees we are restricted to finitary graphs (although, with higher order unifcation we might be able to eek out a lazy infinite structure, I'm not sure).

I assume that in the case of AFA we are talking about arbitrary directed graphs?

Also is there a recommended reference to bisimulation.

sigfpe said...

Kenny,

Don't know what I was thinking. Having actually worked through the proof of Strong Extensionality I don't know why I went on to write about it as an axiom. I'll fix that in the main text.

Jacobian,

I think various papers on streams by Rutten give a good intro to bisimulation in certain contexts.

thedatabase said...

Hello SIGFPE --- that's a coincidence... I searched for "axiom anti-foundation" while reading This Weeks Finds, and up you pop, a This Weeks Finds reader who's just posted on the subject. Small internet!

Anyway, if you've been reading the tale of n-categories, 3-morphisms between 2-morphisms, 2-morphisms between morphisms, etc, don't you sometimes feel it's a shame that a theory that emphasises form and structure only up to isomorphism, should still depend on a very concrete "Level-1" case, ie some base category with objects?

In fact, the whole motivation for objects seems just to be to get morphisms off the ground, allowing us to start stepping up the (at least strict) n-category ladder in a quasi-inductive way

This got me thinking that objects in a category and the axiom of foundation play a very similar role.

If one were to attempt to do-away with objects, ie just have morphisms between morphisms between morphisms, one would quickly find oneself with either infinite or circular chains of descent, just as with unfounded sets

I've not paid this much thought, as evidenced by you being my first hit on google, but perhaps you may have some insight into:
- would a category theory without objects be doable at-all, and if so, would it share any features with unfounded set theory?
- how would you recover either natural transformations or n-category theory? My inital thought would be that there would only remain certain classes of "differences" or "quotients" between your unfounded categories (assuming you managed to recover anything resembling category theory!)

Jacobian said...

I think there is a typo in this diagram from your literate haskell at:

http://homepage.mac.com/sigfpe/Computing/fold.html

F(h)
F(X) --> F(Y)
| |
fin| | f
V h V
X --> X h = fold f

Jacobian said...

I think it just occured to me why bisimulation and removal of state labels is important here so let me try to explain it to see if I'm on the right track.

x = {x} can be thought of as an arrow from the state x to the state x, a loop.

x -> x

Now if we look at the simultaneous equations y={z},z={y} then we have

y->z->y a circle with two points. But in actuality, y and z are indistinguishable since the available transitions from y are the same as those from z, and therefor we collapse to the same graph as x={x}. Is this correct?

sigfpe said...

Jacobian,

Your intuition about erasing labels agrees with mine. I'll get back to you on the typo...

sigfpe said...

thedatabase,

In effect you'd like to erase the objects leaving just the arrows, just as you can do with many other kinds of coalgebraic structure. That might in fact be doable with AFA, but I'm no expert on category theory. Part of me thinks "what a cool idea!" and part of me is repelled by the thought :-)

sigfpe said...

jacobian,

I had to look at that diagram several times to see that the bottom right X should be a Y.

I might have to rewrite the whole thing at some point. It seems that the Haskell type system is flexible enough to unify all of the initial algebras as instances of one type parametrised by the functor F, and the same goes for the final coalgebras. I think fold and unfold just pop out automatically without me having to think hard about how to implement them - I'd just have to implement fmap for the functor. I'll have to work out the details. But it's hard to revisit something you thought was finished.

Blog Archive