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:

...∈A₃∈A₂∈A₁∈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.