Non-wellfounded Set Theory

First published Wed Apr 16, 2008; substantive revision Tue Apr 24, 2018

This entry is about two kinds of circularity:objectcircularity, where an object is taken to be part of itself insome sense; anddefinition circularity, where a collection isdefined in terms of itself. Instances of these two kinds ofcircularity are sometimes problematic, and sometimes not. We areprimarily interested in object circularity in this entry, especiallyinstances which look problematic when one tries to model them in settheory. But we shall also discuss circular definitions.

The termnon-wellfounded set refers to sets which containthemselves as members, and more generally which are part of aninfinite sequence of sets each term of which is an element of thepreceding set. So they exhibit object circularity in a blatant way.Discussion of such sets is very old in the history of set theory, butnon-wellfounded sets are ruled out of Zermelo-Fraenkel set theory (thestandard theory) due to the Foundation Axiom (FA). As it happens,there are alternatives to this axiomFA. This entry is especiallyconcerned with one of them, an axiom first formulated by Marco Fortiand Furio Honsell in a 1983 paper. It is now standard to call this principle theAnti-Foundation Axiom (AFA), following its treatment in aninfluential book written by Peter Aczel in 1988.

The attraction of usingAFA is that it gives a set of tools formodeling circular phenomena of various sorts. These tools areconnected to important circular definitions, as we shall see. Weshall also be concerned with situating both the mathematics and theunderlying intuitions in a broader picture, one derived from work incoalgebra.Incorporating concepts and results from category theory,coalgebra leads us to concepts such ascorecursionandcoinduction; these are in a sense duals to the morestandard notions ofrecursionandinduction.

The topic of this entry also has connections to work in game theory(the universal Harsanyi type spaces), semantics (especiallysituation-theoretic accounts, or others where a “world” is allowedto be part of itself), fractals sets and other self-similar sets, theanalysis of recursion, category theory, and the philosophical side ofset theory.

1. Circular Phenomena in Set Theory

It is difficult to say in a general way what makes a definitioncircular. In this entry we are concerned exclusively withmathematical definitions of various sorts. Consider the equationx = ½x + 1. Is this acirculardefinition of the number 2? In a sense, it is just that: anumber has been defined in terms of itself. But there is nothingproblematic about this equation, and so one may wonder why this is inthe same class of equations asx =x + 1, orx =x. In the set theoretic setting, we oftenemploy circular definitions and characterizations of sets and classes.For example, the collectionHF ofhereditarilyfinite sets may be characterized by

(1)HF is the set of allx such thatx isa finite subset ofHF.

With a bit of work, it can be shown that (1) defines a unique set instandard set theoryZFC. (1) is more of acharacterization than a textbook definition, however. Inother words, if one were presented with (1) as a putativedefinition, then the first step in understanding it would be to “straighten out” the circularity by providinga different definitionD of a set, then to check that everyset satisfyingD satisfies the property definingHF,and vice-versa.

It is easier to think about circularobjects than circulardefinitions. Even so, it will be useful in reading thisentry to keep circular definitions in mind. The most conspicuous formof object circularity would be a set having itself as an element; evenworse would be a setx such thatx = {x}.For those with a background in standard set theory, such sets areruled out by the axioms in the first place, and in the second it isnot clear why one would want to change the axioms in order to admitthem. And if one does take the drastic step of altering the axioms ofa well-established theory, what changes? This entry is an extendeddiscussion of this matter, and related ones.

1.1 Streams

Many of the ideas in this entry may be illustrated usingstreams. Astream of numbers is an ordered pairwhose first coordinate is a number and whose second coordinate isagain a stream of numbers. The first coordinate is called thehead, and the second thetail. The tail of a givenstream might be different from it, but again, it might be the verysame stream. For example, consider the streams whose headis 0 and whose tail iss again. Thus the tail of the tail ofs iss itself. We haves =⟨0, s⟩ ,s = ⟨0, ⟨0, s⟩ ⟩ , etc. This streams exhibits object circularity. It is natural to“unravel” its definition as:

(0,0,…,0,…)

It is natural to understand theunraveled form as aninfinite sequence; standardly,infinite sequences are taken to be functions whose domain is the setN of natural numbers. So we can take the unraveled form tobe the constant function with value 0. Whether we want to take thestreams described above tobe this function is anissue we want to explore in a general way in this entry. Notice thatsince we defineds to be an ordered pair, it follows from theway pairs are constructed in ordinary mathematics thats willnot itself be the constant sequence 0.

One way to define streams is withsystems of equations for them.For example, here is such a system:

(2) x ≈ ⟨0, y⟩
y ≈ ⟨1, z⟩
z ≈ ⟨2, x⟩

We should comment on the ≈ notation here. We are concernedwith modeling various types of ordinary mathematical objects in settheory, and one kind of object that we want to model will be that of asystem of equations. This is an unusual thing to do. Inanticipation of things to come, we use the ≈ sign forequations we would like to solve. So in our discussion ofx = ½x + 1 above, we would prefer to writex ≈ ½x + 1. The point is that‘x’ here is a symbol, but whatever we takesymbols to be, it will almost never be the case that the symbolx is identical to the expression ‘½x +1’ or to anything related to it. For the solution to anequation or a system of them, we will use a “dagger” torefer to the solution. Thus for this equation,x^† = 2; the reason that 2 satisfies theequation is that 2 =½(2)+ 1 (and here we use = ratherthan ≈).

Returning to equation (2), we take it to define streamsx^†,y^†, andz^†. These satisfy equations:

x^† = ⟨0, y^†⟩
y^† = ⟨1, z^†⟩
z^† = ⟨2, x^†⟩

Thesestreams then have unraveled forms. For example, the unraveled form ofy^† is (1,2,0,1,2,0,…).

There is a natural operation of “zipping” two streams.Also called “merging”, it is defined by

(3) (s,t) = ⟨ (s), (t, (s)) ⟩

So to zip two streamss andt one starts with thehead ofs, and then begins the same process of zipping allover again, but this time witht first and the tail ofs second. For example, ifx^†,y^†, andz^† arethe solutions to the system in equation (2) above, then we might wish to consider,for example, (x^†, y^†). In unraveled form, this is

(0,1,1,2,2,0,0,1,1,2,2,0,…).

But please note that our definition of does not work by recursion as one might expect; for one thing, thereare no “base cases” of streams.

We can even ask about solving systems of equations written in terms of . It is easy to see that an equation likex =(x,x) is satisfied by all and only the constant streams. One like

x =((x) + 1,x)

has no solutions whatsoever. But if we do things right, we candefine very interesting streams. For example, consider

(4) x ≈ ⟨1, (x, y)⟩
y ≈ ⟨0, (y, x)⟩

The system has a unique solution. The unraveled form ofx^† begins as

(1,1,0,1,0,0,1,1,0,0,1,0,1,1,0,1,0,…)

that ofy^† begins

(0,0,1,0,1,1,0,0,1,1,0,1,0,0,1,0,1,…).

The first of these is a famous sequence, theThue-Morsesequencet (actuallyx^†= (t).)^[1]

1.1.1 The reduction of streams to functions

We have been careful to emphasize the difference between streams aswe originally spoke of them and their unraveled form as functions onthe natural numbers. At this point we want to look at this mattermore closely.

Before we turn to the details, let us consider the parallel matter ofsequences construed as functions on the natural numbers.Anyone who teaches about (infinite) sequences of some sort, saysequences of integers or real numbers, may at some point need to saywhat a sequence actually is. Surely this is not done very often inelementary presentations: usually one would give examples instead of aformal definition, or illustrate what sequences are for by using themin some way or other. In any case, it happens that in the usualset-theoretic modeling of mathematics, sequences of real numbers wouldbe taken tobe functions from the set of natural numbers tothe set of real numbers. So we have areduction of one kindof object, sequences, to another, functions. Of course, functions arethen reduced to sets of ordered pairs, ordered pairs to sets of acertain form, natural numbers to sets of yet another form, and realnumbers in their own way. Concerning this kind of reduction, weshould always ask whether it is necessary or silly, and whether it isuseful to those using the mathematical objects in the first place.All of this is worth keeping in mind as we turn back to the sequences.

LetN^∞ be the set of streams of naturalnumbers, and let^NN be the set offunctions fromN toN. The reduction employs twofunctions

φ : N^∞ → ^NN
ψ : ^NN → N^∞

defined as follows: For φ, we first take a streams to afunctionf_s : N→N^∞. This time we use recursion:

f_s(0) = s
f_s(n+1) = (f_s(n))

Then fromf we get a functionφ(s) : N →N byg(n) =(f_s(n)). This defines φ, the precise definition of what we spoke ofearlier by the nameunraveling. In the other direction, weneedinfinite systems of equations. Given a functionf : N →N, consider

(5) x₀ = ⟨f(0), x₁⟩
x₁ = ⟨f(1), x₂⟩
…
x_n = ⟨f(n), x_n+1⟩
…

Then this system has a solution, and we take ψ(f) =x₀^†. It is then possible to showthat the composition in one direction, ψ ⋅ φ , is the identity onN^∞ and the other composition φ⋅ ψ is the identity on^NN. In plainerterms, we can pass from streams to functions onnumbers, and we can also go the other way.

At this point, we can ask questions about the reduction. Thefirst question that comes to mind concerns the ontological status ofthe entities:

LetA be a collection of abstract objects (say functionsfrom natural numbers to natural numbers), and suppose thatone believes that the objects inA exist. LetB be a different collection of abstract objects. SupposethatA andB correspond in a natural way, and thateverything one says about objects inB could well be saidabout their correspondents inA, perhaps using differentlanguage. Should one believe that the objects inB alsoexist?

Asking this about streams and functions onN is no differentthan asking it for any other kind of reduction of mathematicalobjects. Any discussion of it would take us to issues in thephilosophy of mathematics that go beyond our goals in this entry.However, there are two additional points to be made on this matter.

First, the standard modeling of pairs in set theory^[2] would have us believe that from the beginning of this sectiononwards, we have been talking about things which do not exist: as wehave literally defined them, there are no streams of numberswhatsoever! We discuss this at length in Section 2.2.1, when we talkabout the Foundation Axiom of set theory. The point is is that thisaxiom forbids object-level circularity in a way that precludes streamsin the exact form that we have them. Thus if one wants to model theintuitive notion of a stream as we have introduced it, one would needto say something like: “By a stream, we mean a function onnumbers. We adopt special notation to make it look like streams arepairs of a certain sort, but deep down they are just functions onnumbers.”

Continuing with questions about the reduction of streams tofunctions, we can ask whether there is any conceptual difference usingstreams as opposed to functions. Certainly these represent differentpoints of view, and for this reason it should be useful to have bothavailable. To see the difference, let us return to the matter ofzipping streams. Done in terms of functionsf,g : N →N,the zipped version would be

(f,g)(n) = f(n/2)
g((n−1)/2)) ifn is even
ifn is odd

It would be harder to use this to turn equation (4) intothe definition of two sequences by recursion.^[3] The upshot is that we can start to see some kind of difference whenwe use one kind of representation instead of another. And this bringsus to our second point on the reduction of streams to functions:conceptual differences worth exploring may be hidden under the surfaceof such a reduction.

At this point, we are done with our discussion of streams. Of coursewe shall revisit them in later sections to illustrate various points.We also broadly foreshadow the main points of this entry:

By changing the usual axioms of set theory, one can modelcircularly defined streams and other objects in a way which is closerto the intuition that one has about them. In particular, it ispossible to work with object-level circularity in a relativelyconsistent set theory, and there may be reasons why one would want todo so.
In the changed theory, we also find different results oncollections defined in terms of themselves. We have already seen sucha collection,HF from (1). The status of circulardefinitions changes when one alters the set theory, and this leads toa broader examination of several issues.
There is also a deeper conceptual issue going far beyond settheory related totop-down vs.bottom-up treatmentsof various phenomena.

1.2 Infinite trees

We want to move from streams to a more complicated example, infinitetrees. Some of the points that we make will be closely related towhat we have seen for streams, and some will raise new issues.

Here is a class of objects which we shall calltrees:^[4]

The variablesx andy alone are trees.
Ift is a tree, then adding a single node labeled •as a new root witht as its only subtree gives a tree.
Ifs andt are trees, then adding a single nodelabeled * as a new root withs as the left subtree andt as the right subtree again gives a tree.
A tree is that which can be obtained by applying the operations any number of times (including infinite applications).

Trees may be specified bytree systems (of equations). Hereis one such system:

(6)
s   ≈
*
t u
t   ≈     •

s
u   ≈
*
x y

Again, we use the ≈ notation in variables for which we want tosolve, and we superscript variables with a dagger in the solution. Inthis case, the one and only solution of this system might be picturedas

s^†     =
*
• *
* x y
• *
… x y
t^†   = •

u^†   =
*
x y

It will be useful to recast the definition of our trees in terms ofpairs and triples:

The symbolsx andy alone are trees.
Ift is a tree, then⟨•, t⟩ is a tree.
Ifs andt are trees, then⟨*, s, t⟩ is a tree.
Trees may be “infinitely deep”.

Then our system above is

s ≈ ⟨*, t, u⟩
t ≈ ⟨•, s⟩
u ≈ ⟨*, x, y⟩

So now we have something that looks more like what we have seen withstreams. But with streams we had an unraveled form, and so we mightwonder what the unraveled form of trees is. To some extent, it wouldbe the pictures that we have already seen. In particular, one couldtake a tree as we have defined them and give a description of how onewould construct the picture. (The full construction would take forever,of course, but the same is true of our work on streams.) Conversely,given a picture, one could set down a tree system for it, where a“tree system” is a system of equations as in equation (6).(In general, the tree system would be infinite, but if you find aregular structure in the picture, then the system could befinite.)

On the other hand, pictures are not entirely respectable as standardmathematical objects, despite the work that has gone on and continuesto go on to rehabilitate them. For work on trees, one would need amore complicated set of definitions. We are not going to present anyof this.

More ‘cheating’. LetTr be theset of trees that we have been discussing. Then our definition interms ofTr would have:

(7) Tr = {x,y} ∪ ({•} ×Tr) ∪ ({*} ×Tr ×Tr).

Now again the standard modeling in set theory gives us a problem: onecan prove inZF set theory thatTr has no solution whatsoever. Andthis runs afoul of our pictures and intuition. The standard way outis to change the equals sign = in (7) to something else. For mostmathematical work this is perfectly fine, but it is the kind of movewe explore in this entry.

1.3 Hypersets

Let us turn from streams and trees to sets. Before presenting someanalogs to what we have just seen, atpictures of sets. Tomake the discussion concrete, consider the set:

x = {∅, {{∅}, ∅}}

Let us call this setx. We want to draw a picture of thisset, so we start with a point which we think of asx itself.Sincex has two elements, we draw add two children:

x
y z

Again, we draw arrows on behalf of the members. We takeyto be ∅ andz to be {{∅}, ∅}. Wedo not add any children ofy because it is empty. But wewant to add two children toz, one forw ={∅} and one for ∅. So we have

x
y ← z
↓
w

We conclude by putting an arrow fromw toy, since∅ ∈ {∅}.

x
y ← z
↓
w

Now we want to forget the identity of the nodes. We could eithertrade in the four sets that we used for numbers (to mention just oneway), or else finesse the issue entirely. We would get one of thepictures below:

1
2 ← 3
↓
4
←
↓

Incidentally, in building this graph, we allowed ourselves to sharethe nodey both times we came to ∅. It would bepossible to avoid doing this, using different nodes. The end resultwould be a tree:

↓

Agraph is a pair (G,→), where → is arelation onG (a set of ordered pairs fromG). Theidea is that we want to think of a graphs asnotations forsets, just as systems of equations were notation for streams.This is explained by the concept of adecoration: Adecorationd of a graphG is a function whose domainisG and with the property that

d(g) = {d(h) : g →h}.

For example, let us introduce names for the nodes in the tree-likegraph and then find its decoration:

1
2 3
4 5
↓
6

Since 6 has no children,d(6) must be ∅. Similarly,d(5) andd(2) are also ∅.d(4) ={d(6)} = {∅}.d(3) ={d(4), d(5)} ={ {∅}, ∅}. Andd(1) ={d(2), d(3)} ={∅, { {∅}, ∅} }.Note this is the setx with which we started. This is noaccident, and you are encouraged to think about why this is true. Arelated point: for a graph like the one in equation (8), where we usethe sets involved as the nodes of the graph, you should check that theidentity function is a decoration.

However, things get more interesting with an example like the loopgraph

x

Letd be a decoration of this graph. Then we would haved(x) = {d(x)}. So writing Ωford(x), we have Ω = {Ω}. This setΩ is the most conspicuous example of object circularity: a setthat is a member of itself. (Indeed, Ω is its own onlymember.)

Finally, we want to consider an example that harks back to the streamsystem (2) in Section 1.1.

Let us try to understand what a decorationd of this graphwould be. In order to follow the discussion below, you shouldremember from set theory that the standard rendering of the first fewnatural numbers is by

0 = ∅, 1 = {∅}, 2 = {0,1} = {∅, {∅}}

and also that the standard definition of the ordered pair ⟨x, y⟩ is as {{x},{x,y}}.

Sincex₀ has no children,d(x₀) must be ∅. Then it followsthatd(y₀) ={d(x₀)} = {∅} = 1. And now

d(z₀) ={d(x₀),d(y₀) } = {0,1} = 2.

Furthermore,d(z₁) = {2}. It follows now that

d(x₁) = {0}, d(y₁) = {1}, d(z₁) = {2}.

And then

d(x₂) = {d(y₃),d(x₁)} = {{0,d(y₂)}, {0} } = ⟨0,d(y₂)⟩
d(y₂) = {d(z₃),d(y₁)} = {{1,d(z₂)}, {1} } = ⟨1, d(z₂)⟩
d(z₂) = {d(x₃),d(z₁)} = {{2,d(x₂)}, {2} } = ⟨2,d(x₂)⟩

The upshot is that we can go back to our original stream system inequation (2) and then solve it by putting down our big graph anddecorating it. The solution would be

x^† =d(x₂), y^† =d(y₂), z^† =d(z₂).

Ahyperset ornon-wellfounded set is a set that isobtained by decorating an arbitrary graph.

Another way of thinking about hypersets is in terms ofsystems ofset equations, as we have done it for streams and trees. By sucha system we mean a setX which we think of as variables (anyset will do), and then a functione fromX to its power set ℘X. That is, the value ofe on each variable is again a set ofvariables. Set systems and related concepts correspond to ones forgraphs in the following way:

the graph (G,→) the system of set equations (X,e)
the nodes ofG the setX of variables
the relation → on the nodes the functione : X → ℘X
the children ofx inG the sete(x) ∈ ℘X
a decoration of the graph a solution of the system

Every graph corresponds to a system of set equations, and vice-versa.For example, corresponding to the picture in (9) we would take

X = {x₀, y₀, z₀, x₁, y₁, z₁, x₂, y₂, z₂, x₃, y₃, z₃}

e(x₀) = ∅	e(x₁) = {x₀}	e(x₂) = {x₁,y₃}	e(x₃) = {z₀,x₂}
e(y₀) = {x₀}	e(y₁) = {y₀}	e(y₂) = {y₁,z₃}	e(y₃) = {x₀,y₂}
e(z₀) = {x₀,y₀}	e(z₁) = {z₀}	e(z₂) = {z₁,x₃}	e(z₃) = {y₀,z₂}

So the way to go from the picture to the function is that eachsete(v) is the set of children ofv.In terms of the kind of notation we have seen before, we prefer towrite this system in a way that elidese:

x₀ ≈ ∅ x₁ ≈ {x₀} x₂ ≈ {x₁,y₃} x₃ ≈ {z₀,x₂}
y₀ ≈ {x₀} y₁ ≈ {y₀} y₂ ≈ {y₁,z₃} y₃ ≈ {x₀,y₂}
z₀ ≈ {x₀,y₀} z₁ ≈ {z₀} z₂ ≈ {z₁,x₃} z₃ ≈ {y₀,z₂}

The study of non-wellfounded sets proposes to treateverygraph as a picture of a unique set. In order to make this work, somekind of change is needed in set theory. The reason is that sets likeΩ = {Ω} do not exist in the most commonly-used set theory,ZFC. This is due to the Foundation Axiom (FA):we’ll discuss this issue further in Section 2 below. For now,FA implies that the only graphs with decorations are thosewith no infinite sequence of points following the arrows. The changein set theory that we make is simply to replace this axiomFAwith a different one calledAFA. The content ofAFAis that every graph has a unique decoration (alternatively, everysystem of set equations has a unique solution).

At the same time, there is a reduction of hypersets to ordinary sets.This means that one could regard all talk of hypersets as merelyabbreviatory. This reduction is fairly complicated, and we shallpresent it in due course.

AdoptingAFA not only helps with circularly defined sets,but it also helps with streams and trees. As we have mentioned, ifone usesFA, there are no streams or trees according to ourdefinitions. That is,N^∞ is literally theempty set withFA, as isTr. But withAFAthese sets are non-empty. Moreover, one can prove that underAFA,N^∞ andTr have theproperties that one would want them to have. (For example, one canprove thatN^∞ corresponds to the functionspace^NN in the way we have discussed.)Finally, working out the resulting theory gives tools that are usefulin studying collections of circularly-defined objects such as streamsand trees. The point is that this one axiomAFA gives us allof this, and more.

1.3.1 Terminology and history

The AxiomAFA was first studied by Marco Forti and FurioHonsell in 1983. Their paper (Forti and Honsell 1983) studies a numberof axioms which contradict the Foundation AxiomFA,continuing a much older line of work in set theory that deals withalternatives toFA. The one they callX₁is equivalent to what has now come to be calledAFA.

Peter Aczel’s book (1988) treats many axioms that contradictFA, but it pays most attention toAFA. It alsoproved many of the important results in the subject, including onesmentioned in this entry. Aczel’s own entrance to the subject was anarea of semantic modeling that he had been working on, concerning thecalculus of communicating systems (CCS). He found it natural topropose a set theoretic semantics, and yet the most obvious modelingseemed to run into problems with Foundation. It is always a bold stepto recommend changing the axioms of set theory in order to make anapplication of the subject. Usually it is a brash move. For the mostpart people resist the idea: when the proposal might well be cast inmore standard forms (as can be done with work usingAFA),people wonder why one wants to tamper with a standard theory; when itcannot be cast in a standard way, the reception is even worse.

Aczel’s work became influential for two research areas. He visitedStanford in 1985, where Jon Barwise was director of the Center for theStudy of Language and Information (and this author was a post-docthere). Barwise recognized the value of the work, partly because hehad similar problems with Foundation in his own work on situationsemantics, and partly because he saw in the work an appealingconception of set that was at odds with the iterative conception thathad been received wisdom for him andpractically everyone else raised in the mainstream traditionof mathematical logic.^[5] He thought thatnon-wellfounded sets should be called by aname that reflected the change in conception, and he proposed callingthemhypersets in parallel to thehyperreal numbersof non-standard analysis. This terminology has for the most part notstuck, but it is not completely outdated, either. In this entry,we’ll use both terms interchangeably.

Perhaps the first serious application of the tools we are studying in this entry comes from this period. This is Barwise and Etchemendy’sbookThe Liar (Barwise and Etchemendy 1987). Its proposals are contributions to the theory of truth. Since we are notprimarily interested in those applications of hypersets, we resist the temptationto discuss matters further.

Aczel’s book was also immediately influential for people working onsemantic questions in theoretical computer science. This was not somuch because it raised questions about set theory, but rather becauseit showed the value of using the categorical notion of acoalgebra. The main use in the book is to organize certainconcepts into an elegant subject. But it quickly became apparent thatthis notion of coalgebra could be studied on its own, that themes fromthe book had a field of application much wider than pure settheory.

This entry reflects the influence of all of these sources. To besure, we shall see the main results on the set theory obtained usingAFA. Also, we present enough of the theory that someone whoneeds to read papers that use it should be able to do start doing so.We also emphasize the conceptual underpinnings of the subject, andcompare them to more standard foundational work. This is hardly everdone in technical papers on the subject, but should be of interest topeople in several areas of philosophy. Finally, our work incorporatesmany ideas and results coming from the coalgebra research community inthe years following the publication of Aczel 1988.

We conclude this section with links to the two followingsupplementary documents:

Universal Harsanyi Type Spaces
Self-similar Sets of Real Numbers

These contain introductory points on two issues that we shall revisit (again, in supplementary documents) at the end of this entry. The reason for the separation is that the issues discussed pertain to game theory and measure theory on the one hand, and fractals and metric spaces on the other. That is, the discussions are not entirely set theoretic. In addition, the mathematical prerequisites for all our supplements are greater than for the main body of this entry. They may be omitted without losing the main thread.However, we emphasize that the overall theory presented in this entry does treat all of these instances of circularity “under the same roof.”

2. The Foundation and Anti-Foundation Axioms

The set theoretic side of our story is connected to two axioms, theFoundation Axiom and theAnti-Foundation Axiom. Wepresent them here, and discuss some related conceptions of set.

2.1 Background from set theory

We start with a reminder of a few basic facts of set theory. One canfind more in any textbook on the subject, and also the entry on set theory, especially in itssupplementary documentbasic set theory.

Power sets.For any sets, the power set ofs is the set of subsets ofs.We write this set as ℘(s)or just as ℘s.

Pairing.The Kuratowski ordered pair ⟨a,b⟩ of two setsa andb is {{a}, {a,b}}.^[6]The standard presentation ofset theory defines and studies relations, functions, and the likein terms of this pairing operation.All mathematical facts about these notions can then be proved in set theory.

Natural numbers. One also defines versions of thenatural numbers by: 0 = ∅, 1 = {∅}, etc. Again, all factsabout numbers and functions on them can be proved in set theory. Infact, essentially all mathematical facts whatsoever can be statedformally and proved in set theory.

Union and transitive closure.For any seta,a is the set of elements of elements ofa.A set istransitive if every element of it is also a subset of it.Thetransitive closure ofa is

a ∪a∪a ….

This set is denotedtc(a). It is the smallest transitive set which includesa as a subset.

Theorem [Cantor]. For all setss, and all functionsf :s → ℘s,f is not surjective. In fact,{x ∈ s : x ∉ f(x)} is not in the imagesetf [s]. (Here, the imagesetf[s] ={f(x) : x ∈ s}.)

Proof.Letc = {x ∈ s:x ∉ f(x)}. Suppose towards a contradiction thatc ∈ f[s]. Fixa ∈ s such thatc =f(a).Thena ∈c iffa ∉f(a) iffa ∉c.

Corollary. For all setss, ℘s is not a subset ofs.

Proof. If ℘s ⊆s, we construct a functionf froms onto ℘s: letff(f) =aifa ∈s, and otherwise letff(f) = ∅.So we cannot have ℘s ⊆s, lest we contradictCantor’s Theorem.

Corollary[Russell’s Paradox].. There is no setR such that every set belongs toR.

Proof.Such a set would have ℘s ⊆R for all setssIn particular ℘R ⊆R, contradicting our last result.

We call the last resultRussell’s Paradox in view ofits content. Neither our statement nor our proof are the moststandard ones.

Well-ordered sets and ordinal numbers.We need the concept of ordinal numbers at a few places.

Awell-ordered set is a pairW = (W, <), where < is a relation on the setWwhich is a strict linear order and with the property that every non-empty subset ofW has a <-least element. For example, (N, < )is a well-order, where < is given by

0 < 2 < 4 < … 1 < 3 < 5 < …

One can show using the Replacement Axiom that every well-ordered setWhas a unique decorationd. Anordinal number(orordinal) is a set of the formd(w), for some well-ordered set (W,< ) and somew ∈W.

One usually uses Greek letters such as α and β for ordinal numbers,and one also writes α < β if α ∈ β. There are a number ofstandard facts about ordinal numbers, including the following:

If α is an ordinal, so is α ∪ {α}.
The standard modeling of natural numbers renders them as ordinals,and the set ω of natural numbers is also an ordinal.
The collection of ordinal numbers is not a set.
Except for not being a set, the ordinal numbers with < has all the properties of a well-ordered set.

An ordinal α is asuccessor ordinal if α = β ∪ {β} for some (other) ordinal β.Ordinals which are neither 0 norsuccessor ordinals are calledlimit ordinals. The smallestlimit ordinal is ω; it isd(1) for the well-order we saw above,0 < 2 < 4 < … 1 < 3 < 5 < …

The cumulative hierarchy.There is a unique operation taking ordinals α to setsV_α such that

V₀ = ∅
V_α+1 = ℘V_α
V_λ = _β<λV_β for λ a limit ordinal

TheZFC axioms.We are not going to state them here, but see the entry onset theory.

Classes.The axioms of set theory are not about sets as much as they are about theuniverse of sets. One of the intuitiveprinciples of the theory is that arbitrary collections of mathematical objects“should be” sets. Due to paradoxes, this intuitive principle is not directly formalizedin standard set theories. In a sense, the axioms one does have are intended to give enough sets to constitute a mathematical universe while not having so manyas to risk inconsistency. But it is natural in this connection to consider some collections of objects whichare demonstrably not sets. These are calledproper classes. Thetermclass informally refers to a collection of mathematical objects. Classes are usually not first-class objects in set theory. (Certainly they are notin the most standard set theory,ZFC. However, the SEP entry onAlternative Axiomatic Set Theories does mention quite a few theories which treat classes as first-class objects.) Instead, a statement about classesis regarded as a paraphrase for some other (more complicated and usually lessintuitive) statement about sets. This is probably not a good place to discussthe details of the formalization; one useful source is Chapter 1 of Azriel Levy (1979).

For our purposes, classes may be taken asdefinable subcollectionsof the universe of sets. For example, ifa is any set, then the class of all sets which do not containa as an element is {x :a ∉x}. In specifying a class, one may use the first-order language with the membership symbol and the rest of the syntax from logic, and one may also use particular sets as parameters, as we have just done.

The classV of all sets is {x :x =x}.The definability here is in the first-order logic with just a symbol ∈ for membership,and the quantifiers range over sets (not classes).Another class of interest isWF, the class of all well-founded sets.This is the same as_αV_α, the sets that belong toV_α for some ordinal α.

IfC is a class, we define thepower class of C, ℘C,by

℘C = {x : for ally, ify ∈x, then φ_C(y)},

where φ_C is the formula that defines the classC.It is important that in this definitionx ranges oversets and not classes;the formal language used does not directly talk about classes in the first place.For example, ℘V =V, and ℘(WF) =WF.We also define the action of other operations on classes in the same general way.For example, the finite power set ℘_fin takes a classC to the class offinite subsets ofC.

2.2 The Foundation Axiom

The Foundation Axiom (FA)may be stated in different ways. Here are some formulations;their equivalence in the presence of the other axioms is a standard result of elementary set theory.

There are no infinite sequences of sets
x₀ ∋ x₁ ∋ x₂ ∋ …x_n ∋ x_n+1 ∋ …
each of whose terms is an element of the previous term.
For every non-empty setx, there is somey ∈x such thaty∩x=∅.
Leta be any set, and letf : ℘a →a.Letb be any transitive set. Then there is a unique functiong : b →a so that forallx ∈b,g(x) =f(g[x]).
For every setx, there is an ordinal number α such thatx ∈V_α.
V =WF.

The first of these is probably the easiest to remember and think about.The second is important because it is the one most easily expressed in first-orderlogic. The third is a recursion principle; we shall consider a closely related principle inSection 4.4.

2.2.1 The iterative conception of set

As we have seen, one formulation ofFA says that every set belongsto someV_α. This is a mathematical formulation of theiterative concept of set: sets are just what one gets byiterating the power set operation on the well-ordered class of ordinalnumbers. We start with nothing, the empty set.^[7]This isV₀. Then we formV₁ = ℘V₀. ThenV₂ = ℘V₁.Going on, when we come to the first limit ordinal ω, we takeV_ωto be the union of all the setsV_n. Then we proceed toV_{ω+ 1} = ℘V_ω. We continue like this absolutelyforever, going through “all the ordinal numbers”. The collection sodescribed is the universeV of sets.

This way of describing the iterative picture suggests that the ordinal numberswere somehow present “before” all the iteration takes place, or at leastthat they have a life apart from the rest of the sets. There is a different wayof understanding the iterative conception, one that emphasizes the harmony between the iteration of the power set operation and the Replacement Axiom:as one iterates the power set axiom, more and more well-ordered sets appear.Replacement allows us to decorate these well-ordered sets, creating new ordinalsin the process. Thus the whole picture is one of balance.Indeed, this point about balance can be phrased without reference to any“iteration” at all: there is an equilibrium in the set theoretic universebetween the “sideways” push of the Power Set Axiom and the “upward” push of the ReplacementAxiom.^[8]

Using the Foundation Axiom.FA plays no role in the formalization of mathematics or in the study of infinity.It is an “optional extra” for mathematics.FA is usedto clarify our picture of sets, just as we have described. This often comes with an implicit argument of roughly the following shape:

An argument.One is tempted to justifyFA along the following lines:

Russell’s Paradox shows that there is no set of all sets:the classV cannot be a member of itself.
The iterative picture shows whyno set can be amember of itself.
The iterative picture also suggestsFA in the form that everyset belongs to someV_α.
ThusFA reflects a picture which avoids Russell’s Paradox,hence it is sensible to accept it.

The rejoinder here is that there might be other intuitive picturesor conceptions of sets that also explain, or draw lessons from, the paradoxes. So they would be as sensible asFA in this regard.

SinceFA plays a conceptual role but no mathematical role, it is not surprising that there are widely different views on whether it is an important part of standard set theoryZFC or not. For a collection of quotes on the role ofFA, see Barwise and Moss (1991).

The Foundation Axiom and object circularity.We mentioned in connection with streams that according to standard set theory,streams of numbers do not exist. Here is the reasoning.Recall that we defined a stream to be a pair of a number and another stream. Suppose that a streams exists, so that the setN^∞of streams is non-empty. Recall that we have a functionf_s : N →N^∞ by recursion:

f_s(0) = s
f_s(n+1) = (f_s(n))

To save on some notation at this point, let’s writeh_n for (f_s(n))andt_nfor(f_s(n)).For alln,

f_s(n) = ⟨ h_n,t_n ⟩ = {{h_n}, {{h_n,t_n}}};

this is true of any pair whatsoever.Notice that

f_s(n+1) =t_n∈{h_n,t_n}∈f_s(n).

So we have

f_s(0)∋{h₀,t₀}∋f_s(1)∋{h₁,t₁}∋f_s(2)∋…

This is a descending sequence in the membership relation, something forbidden byFA.

The same kind of remark applies to infinite trees as we discussed them,and certainly to hypersets. The conclusion is that if one wants to work with such objectsin a set theory withFA, then one must do so indirectly.

2.3 The Anti-Foundation Axiom

The Anti-Foundation AxiomAFA is stated as follows:

Every graph has a unique decoration.

The theoryZFA isZFC withFA replaced byAFA.It includes the Axiom of Choice, even though there is no “C” in the acronym.

The coiterative conception of set.AFA gives rise to, or reflects, a conception of set that is at oddswith the iterative conception. For lack of a better name, we call itthecoiterative conception. According to this, a set is an abstractstructure obtained by taking a graphG (a set with a relation on it),and then associating to each nodex in the graph a set in such a way thatthe set associated tox is the set of sets associated to the children ofxinG . This association is what we calleddecoration earlier. This association might be thought of procedurally, but it need not beso construed. One can instead posit a harmony between decorationand power sets.^[9]

What changes withAFA, and what does not change?.AFA gives us unique solutions to systems of set systems;this is almost immediate from the axiom and the close relation of set systemsand graphs. But it also gives us unique solutions for stream systems and tree systems.The details of this are suggested by our work on the decoration of the graph related to streams and pairs which we sawearlier on.

All of the results in set theory whichdo not useFA go through when one replaces it byAFA. In particular, the following topics are unchanged: Russell’s Paradox and the Separation(Subset) Axioms;the modeling of ordered pairs, relations and functions; the natural numbers, real numbers, etc.; well-orderings and the ordinal numbers;transfinite recursion on well-orders and well-founded relations;the Axiom of Choice; problems and results concerning the sizes of infinite sets.The only difference would be in modeling questions for circularly defined objects of varioussorts,as we have been discussingthem.

In terms of modeling circularity,AFA gives several new conceptsand techniques. These are described in our next section.

3. UsingAFA

This section offersa quick introduction to the central parts of the theorynon-wellfounded sets: what one would need to know to usethe theory and to read papers on it.

3.1 Bisimulation

The topic ofbisimulation is one of the earliest goals in atreatment of non-wellfounded sets.

Let (G,→) be a graph. A relationR onG is abisimulation if the following holds:wheneverx R y,

Ifx →x′, then there is somey →y′such thatx′ R y′.
Ify →y′, then there is somex →x′ such thatx′ R y′.

These are sometimes called by the suggestive nameszig andzag.

Bisimulation between graphs.Before giving examples, we should clarify some usage.At a few points, we’ll speak of bisimulationbetween two graphsG andH, rather thanon a single graph. This can be defined in the same general way. Note also that one can take thedisjoint unionG +H of the graphsG andH, and then a bisimulation betweenG andH would be a bisimulation onG +H.

Returning to bisimulation on a graph. For an example, let’s look at the following graphG:

All of the 3-points have no children. (Point3d is not reached from any other point, butthe arrowsinto a node are of no interest.) So every relation whichonly relates3-points is a bisimulation onG.Concretely,

{(3a, 3b), (3c, 3a), (3d, 3d)}

is easily seen to be a bisimulation.

For that matter, the empty relation is also a bisimulation onG.

Another bisimulation is

{(2a, 2b), (2b, 2c), (2c, 2a), (3a, 3b), (3b, 3c), (3c, 3a)}.

Let’s call this relationR.It would take a lot of checking to actually verifythatR is a bisimulation.Here is just two items of it: We see that 2b R 2c.Now 2c → 2b. Thus we need some nodex so thatx R 2b and 2b →x.For this, we take 2a. For our second point of verification, again note that 2b R 2c . Since 2b → 3b, we need some nodex so that 2c →x and 3b R x. We takex = 3c for this.

The largest bisimulation on our graphG is the relation that relates1 to itself, all 2-points to all 2-points, and all 3-points to all 3-points. Note that this is an equivalence relation: reflexive, symmetric, and transitive. This is not an accident.

Proposition For any graphH, there is a largest bisimulation onH. This relation is an equivalence relation denoted ≡_b, and it is characterized by
x ≡_by iff there is a bisimulation onH relatingx toy.

This relation ≡_b iscalledbisimilarity.

We can always form thequotient graph using the largest bisimulation.Here is how this works, usingG from aboveas an example. InG/≡_b,we would have three nodes, corresponding to thethree equivalence classes under the largest bisimulation; let’s call these classes1,2 and3. We put an arrow between two of these classes if some (every) element of the first has an arrow to some element of the second. In this way, we construct the quotient. Here is a picture ofG again, along with its quotientG/≡_bunder the largest bisimulation:

The map fromG toG/≡_b takes the 2-points to the point 2,and the 3-points to the point 3.

Up until now, we have said what bisimulation is, but we did not describe its relation to anything else. To rectify matters, here is the main result.

TheoremAssumeAFA. LetG be a graph, letx andy be nodes ofG, and letd be the decoration ofG.Then the following are equivalent:
d(x) =d(y).
There is a bisimulation relatingx andy.

We are not going to prove this theorem in full here, but instead hereare two hints. To prove that (1) implies (2), check that thekernel relation of d,

{(u,v) :d(u) =d(v)}

is a bisimulation onG.

In the other direction, the idea is to turn a bisimulation into a graphitself, and then extract two decorations of it; by the uniqueness partofAFA these must coincide.Here is how this is done in a concrete example. We saw above that

R = {(2a, 2b), (2b, 2c), (2c, 2a),(3a, 3b), (3b, 3c), (3c, 3a)}.

is a bisimulation. We make it into a graph by taking the product relation.This gives the following graph which we callH:

Letd be a decoration (no,the decoration) ofG.We get two decorations ofH,k andl defined by

k(u,v) =d(u), andl(u,v) =d(v).

(It is good to check that these really are decorations ofH.) ButH can have only one decoration. Sok =b. And then, corresponding to the fact that 2a R 2c, for example, we have

d(2a) =k(2a,2b) =l(2a,2b)=d(2b).

This concludes our sketch. For more details, see Aczel (1988).

3.2 Doing withoutAFA

Our work on bisimulation above can be used to effect a reduction of the of non-wellfounded sets to that of ordinary sets,much in the spirit of what we saw for streams and functions inSection 1.1. There are several ways to describe such a reduction.

Apointed graph is a triple (G,→,g) such that → is a relation onG andg ∈ G. Abisimulation between pointed graphs (G,→,g) and (H,⇒,h) is a bisimulationR between (G,→) and (H,⇒) such thatg R h.

In the remainder of this discussion, we letp,q, … denote pointed graphs. We writep ≡_bq if there is a bisimulationbetweenp andq. We writep εq ifthere is a pointed graph (G,→,g) and someg →hinG so that

p ≡ (G,→,h) and q ≡ (G,→,g).

Sentences in the language of set theory talk about sets, andwe translate them to sentences about pointed graphs by restricting all quantifiers to the class of pointed graphs, and thentranslating ∈ to ε, and ≡ for =. Forexample, the Axiom of Extensionality

∀x,y(x=y → ∀z(z ∈x →z ∈y)).

would translate to (wherep,q,r range overpointed graphs):

∀p,q(p ≡q → ∀r(r εp →r εq)).

This last sentence is then provable. (Hint: the union of any setof bisimulations on a graph is again a bisimulation on it.)

Indeed, all of the axioms ofZFA are provable, includingAFA.This is a fairly long and tedious verification, but it is not so tricky. A version of it(for set theory withurelements, objects which are not sets)is the topic of a chapter in Barwise and Moss (1996).

One can also go further: instead of translating the identity relation = into something more complex, we may keep the language simpleand complicate the interpretation. We would like to replace “pointed graph”by “≡-class of pointed graph”. Since these are not sets, we insteademployScott’s trick and instead use “set of well-founded pointed graphs whose node sets are ≡-equivalentand with the property that no pointed graph of smaller rank is also ≡-equivalent to them.”

Doing all of this leads to relative consistency result:

Theorem.IfZFC is consistent, then so isZFA,and vice-versa.

3.3 Extended graphs

The way we have presented graphs, decorations, andAFA is a very “minimalist” presentation. If one would like some node of a graphGto be decorated by some seta the most obvious way would be toadd all the elements oftc({x}) as fresh nodes inG, withy→z iffz ∈y. This means that one must take new copiesif some of the sets intc({x}) already happen to be nodes inG.This is often cumbersome:when working with graphs and decorations, one might well want topre-specify as much as possible the value of the decoration ona node. There are several ways to do this withAFA, and we’ll indicateone here.

Two sets aredisjoint if their intersection isempty. When one takes the union of two sets,saya andb, it is sometimesa good idea to make sure that no element occursin both sets. The way to do this is to replace one or bothofa andb by copies.

Thedisjoint union of setsa andb isa+b, defined by

a+b = (a × {0}) ∪ (b × {1}).

It is easy to see that the two sets in the union are disjoint:the elements ofa+b “wear on their sleeve” a mark of whichset they come from.

The disjoint union comes with two natural functions:

:a →a+b and :b →a+b

defined by (x) = ⟨x,0⟩ and (x) = ⟨x,1⟩ .^[10]

Agraph extended with set parameters (orextended graph for short)is a setG together with a functione:G→ ℘G+V. Ife(g) is of the form ⟨s,0⟩ for somes ⊆G, then we intend it as a node just as in our earlier treatment. In particular, we want to decorateit with the set of decorations of its children. Ife(g) = ⟨x,1⟩ , thenwe want a decoration to be forced to have the valuex ong.

Formally, a decoration of an extended graph is a functiond defined onGso that for allg ∈G,

d(g) = {d(h) :g →h}
x ife(g) = ⟨s,0⟩
ife(g) = ⟨x,1⟩

Here is an example: LetG be the extended graph with node set {w,x,y,z}and withe given by

e(w) = ⟨{w,x,y}, 0⟩ e(y) = ⟨2,1⟩
e(x) = ⟨{z}, 0⟩ e(z) = ⟨∅,0⟩

Then a decorationd of this extended graph would satisfy the following conditions:

d(w) = {d(w),1,2} d(y) = 2
d(x) = {0} = 1 d(z) =∅ = 0

TheoremAssumeAFA. Then every extended graph has a unique decoration.

The point we are trying to make is that there is quite a bit of theoryaround to facilitate working inZFA in order to do modeling ofvarious forms of circular phenomena.

3.4 Collection circularity inZFA

The fact thatAFA allows us to solve various kinds ofsystems of set equations is only the beginning. When we discussedinfinite trees inSection 1.2, we noted that the collectionTr of infinite treesshould satisfy (7), repeated below:

Tr = {x,y} ∪ ({•} ×Tr) ∪ ({*} ×Tr ×Tr).

A similar equation should hold of streams fromSection 1.1:

N^∞ = N ×N^∞ .

For that matter, the universeVof sets should satisfy

V = ℘V

Assuming the Power Set Axiom and the formulation of ℘ as an operatoron classes, the universeV does satisfy this equation.

We are free to step back and think of these as equations whichwe hope to solve. For example, we could take the setN as known,regardN^∞ as a variable, and then consider an equation likeX =N×X. However, the none of these is the kind of equation that we could hope tosolve in a perfectly general way usingAFA: the right-hand sides are not given in terms of sets of objects on the left.Solving more complicated systems takes special additional work.Here is what is known on this.

First, underFA, the first two of our three equations each have a uniquesolution: the empty set. UnderAFA, they have many solutions.For example, for the stream equation, the set of streams corresponding tofunctions which are eventually 0 is a solution. However, thelargest solutions are of special interest. For these, one can prove that the largest solutions are in one-to-one correspondencewith what we have called the unraveled forms. And for other reasons which weshall see, there is a good reason to accept the claim that the largest solutionsare good mathematical models of the intuitive concepts.

UnderAFA, things are different. Here is the general picture:An operator on setsF ismonotone if whenevera ⊆b,then alsoFa ⊆Fb. This is a very common featurefor operators on sets. Thepolynomial operators on setsare the smallest collection containing the constant operators, and closed under cartesian product, disjoint union, and functions froma fixed set. For example, ifA andB are fixed sets, thenFs = (A ×s) +^B(s +A) is a polynomial operator on sets.If one also allows the power set operator to occur, then weget thepower polynomial operators. Every power polynomial operatorismonotone. And now, we have the following results due to Aczel:

Proposition. Then every monotone operatorF onsets has a least fixed pointF_* and a greatest fixed pointF^*. In particular, every polynomial operator on classes has least and greatest fixed points. On classes, the same is true for the larger collection of power polynomial operators.

AssumingFA, the fixed points are unique; frequently they are the empty set. WithAFA, the greatest fixed points usually have non-wellfounded members. We shall study this in more detail when we turn to coalgebra.For now, we return to the last of the example equationsat the top of this section,V = ℘V. This equation has no solutionsin sets due toCantor’s Theorem.However, in terms of classes, this equation does have solutions, as weknow. The universal classV is a solution, as we have seen. And the classWF of well-founded sets is a solution. This is the smallest solution ℘_*, andV is the largest. UnderFA, ℘^* =V = ℘_*. UnderAFA, ℘_* and ℘^* aredifferent: ℘_* =WF, and ℘^* =V and thus contains sets such as Ω= {Ω}.

4. Comparing Foundation and Anti-Foundation

The purpose of this section is to compareFA andAFA in a technical way, using ideas from category theory. That is, the language of category theory and especially its built-in feature ofduality are used to say something insightfulabout the relation betweenFA andAFA. Further, the dualstatements about the axioms suggest a much more systematic and thoroughgoing duality about a host of other concepts. This deeper point isnot a strictly mathematical result but rather more of a research program,and so the final subsection here will detail some of what is knownabout it.

As we said, our work here begins to use category theory.We realize that not all readers will be familiar with that subjectat all. So we shall try to make this section as accessible as possible.In particular, we’ll only present those notions from category theory that we actuallyneed in our work of this section. We also illustrate all of the definitions on a few categories which will be of interest. And as we goon in future sections, we’ll develop only the background that we need.^[11]

Our use of category theory is mainly for the terminology and intuition. We know that there are philosophical issues connected with the useof category theory as a foundation for mathematics. This entry does notdeal with any of these issues in a head-on way.

Initial and final objects.

We need a definition from category theory.Fix a categoryC.An objectx isinitial if for every objectythere is exactly one morphismf : x →y Dually, an objectx isfinal if for every objectythere is exactly one morphismf : y →x.

In , the empty set is an initial object; for every sety,the empty function is the only function from ∅ toy.In addition, the empty set is the only initial object.

As for final objects, every singleton {x} is a final object.For every sety, the constant function with valuex is the onlyfunction fromy tox. And the singletons are the only final objects in the category.

PropositionLetC be a category, anda andbbe initial objects.Thena andb areisomorphic objects: there are morphismsf : a →b andg : b →a and such thatg⋅f =id_aandf⋅g =id_b.

ProofBy initiality, we get (unique) morphismsf andg as in our statement.Note thatg⋅f is a morphism froma to itself. And sincea is initialandid_a is also such a morphism, we see thatg⋅f =id_a.Similarly forb.

4.1 The category of sets, the category of classes

We refer the reader to the entry oncategory theory for the definitions of category and functor.

We need to mention the objects and morphisms in the categories of setsand of classes, and also to spell out the functors of interest onthem.

.The objects are the sets, and the morphisms are triples ⟨x,y,f⟩, wheref : x →y. That is,each triple ⟨x,y,f⟩ is amorphism fromx toy. The identitymorphismid_a for a seta is⟨a,a,f⟩ , wheref isthe identity function ona and the composition operation ofmorphisms is given by:

⟨y,z,g⟩ ⋅ ⟨x,y,f⟩ = ⟨x,z,g ⋅f⟩

Functors on.The polynomial operators on sets extend to endofunctors on . The way that these operations are defined on morphisms is straightforward and may be found in any book on category theory. Here is a brief summary: For any sets, the constant functor with values is a functoron . It takes every function toid_s.For any two functorsF andG,we have a functorF×Gdefined by (F×G)(a) =Fa ×Ga; here we use the cartesian product on sets. Iff : a →b, then

(F×G)f(a,b) =(Ff(a),Gf(b)).

We also have a functorF+G defined by (F +G)(a) =Fa+Ga using the coproduct on sets, that is, the disjoint union. Here the action on morphisms is by cases

(F +G)(f) (x) =Ff(x)
(F +G)(f) (x) =Gf(x)

A special case isFx =x + 1. That is,Fx is the disjoint union ofxwith a singleton. And iff : x →y, thenFf : Fx →Fyworks in much the same way, taking the new point inx to the new point iny,and otherwise behaving likef.

The power polynomial operators also extend to endofunctors on :on morphismsf : x →y, the function ℘f: ℘x → ℘y takes each subseta ⊆xto its image

f[a] = {f(z) :z ∈ a}.

.Here the objects are formulas in the language of set theoryφ(x,y₁,…,y_n) together withn setsa₁,…,a_n.We think of this as

{b : φ[b,a₁,…,a_n]}.

The morphisms are then triples consisting of two formulas with parameters defining the domain and codomain,and a third one with two free parameters defining the actionof the morphism.

Functors on.The functors of interest are again the power polynomials.They are defined on similarly to the way they are defined on .For our purposes, the main difference between the two categories is thatin we cannot solve ℘(x) =x, while we can do so in .

4.2 Algebras for a functor

LetF be an endofunctor on a categoryC. Analgebra forF is a pair (c,f),wherec is an object ofC, andf : Fc →c.

Here is a basic example that illustrates why these are calledalgebras. Let’s take the category of sets, and the functor

Ha = (a ×a) + (a ×a).

For the objectN of natural numbers,HN is thustwo copies ofN×N. We’ll use colors to indicatethe different copies, with red for the first copy and blue forthe second. So we can viewHN as

One example of an algebra for this functoris (N,α), whereα() =a + b and α() =a ×b. In other words, α operates on the red pairsby adding and on the blue pairs by multiplying.

Getting back to the terminology of “algebra”, the point is that the function α does the work of the two tables. The function “is” the tables.

Here is another example of an algebra. This time we are concerned on withFx =x +1, as defined above.The algebra we have in mind is (N,s). Heres : N+1 →N takes the natural numbern to its successorn+1,and the new point inN+1 to the number 0.

Up until now, we have merely given examples of algebras fordifferent functors.The advantage of the categorical formulation is that the usual notionsof amorphism of algebras turn out to be special caseof a more general definition.

Let (c,f) and (d,g) be algebras for the same functorF on the categoryC.Amorphism of algebras from (c,f) to (d,g) isa morphismα : c →d so thatthe diagram below commutes:

Fc f
→ c
Fα ↓ ↓ α
Fd →
g d

(This means that the two compositions, α ⋅f andg⋅Fα, are the same function.)

It now is clear that we have a category of algebras for a given functor.And so we immediately have the concept ofinitial andfinalalgebras. There is no guarantee that these exist, but in many interesting cases they do. The reason we are interested in initial algebras is their connection torecursion.

To see this in detail, we return to the functorFx =x + 1 on .We saw the algebra (N,s) above. We claim that this is an initial algebra.What this means is that for any algebra (A,a), there is a unique algebra morphismh : (N,s) → (N,s). That is, the diagram below commutes:

N+1 s
→ N
h+1 ↓ ↓ h
A+1 →
a A

Thue functiona fromA+1 toA may be decomposed into a mapi : A →A together withan elementb ∈a. And to say that the diagram above commutesis the same thing as saying thath(0) =b, and for alln ∈N,h(s(n)) =a(h(n)).

Stepping back, the purported initiality of (N,s) is the same as the following assertion:

For every setA, everyb ∈ A, and everya : A →A, there is a uniquefunctionh : N →A such thath(0) =b, and for alln ∈ N,h(s(n)) =a(h(n)).

This is the standard form of the Principle of Recursion onN.The upshot is that this principle is equivalent to the assertion that (N,s) is aninitial algebra of the functorFx =x +1.

One way to interpret this equivalence is that we can take the existenceof an initial algebra forFx =x+ 1 as anaxiom of set theory,in place of the usual Axiom of Infinity. That axiom says that there isan algebra for the singleton functorSx = {x} on sets which contains∅ as an element and whose structure is the inclusion.This principle is easier to state than the algebraic reformulation.It takes a bit of work to use the simpler standard formulation to derivethe Recursion Principle, and this is one of the basic topics in anycourse on axiomatic set theory.

Two general facts: First, the structure map of an initial algebra on is always a bijection. This follows from a very general result in category theory due to J. Lambek.And from this we see that ℘ has no initial algebras on , byCantor’s Theorem.

Initial algebras for polynomial functors on.

LetF : → be a power polynomial functor. We know thatF is monotone (it preserves the subset relation on sets), and it is not hard to check a slightly stronger property:F preservesinclusion maps between classes: Aninclusionis a mapi_a,b : a →b on classes which “doesn’t do anything”:a must be a subset ofb,and for allx ∈a,i(x) =x. We say thatF isstandard if it preserves inclusions in the sense thatFi_a,b =i_Fa,Fb.Once again, every power polynomial endofunctor on is standard.

The polynomialoperations on sets (without power) are alsocontinuous:they preserve countable unions of sets.

LetF : → be a polynomial endofunctor.We sketch the proof that the least fixed pointF_* carries the structureof an initial algebra, together with the identity on it.

One forms the increasing sequence

0 ⊆F0 ⊆F(F0) ⊆F(F(F0)) …

We write 0 for ∅.Each of the maps shown is an inclusion, by standardness.LetF_* be the union of the increasing sequenceFⁿ0 of sets.ThenF(F_*) =F_* by continuity. So (F_*,id) is an algebra forF.To check initiality, let (A,a)be an algebra forF, soa : Fa →a.Define mapsg_n : Fⁿ(0) →A by recursion, withg₀ : 0 →A the empty function(this is what initiality of ∅ amounts to), andg_n+1 =a ⋅Fg_n.Check that we have an increasing sequence of functions

g₀ ⊆g₁ ⊆g₂ ⊆ …

then take the union to get φ : F_* →A.One checks that this φ is a morphism ofF-algebras, and indeedis the only such.

4.3 Coalgebras for a functor

We now turn to coalgebras.Again, letF be an endofunctor on a categoryC.Acoalgebra forF is a pair (c,f), wherecis an object ofC, andf : c →Fc. Comparingthis to the definition of an algebra, we can see that acoalgebra is the same kind of structure, except that the direction of the arrow is reversed.

For example, every graph is a coalgebra of ℘ onF : → .That is, every graph (G,→) may be re-packaged as (G,e), withe : G → ℘G given bye(x) = {y ∈G :x→y}. In words, we trade in the edge relation of a graph with the function that assigns to eachpoint its set of children. This re-packaging has an inverse,and so the notions of “graph as set with relation”and “graph as coalgebra of ℘” are in this sensenotational variants.^[12]

Let (c,f) and (e,g) be coalgebras for the same functor.Amorphism of coalgebras from (c,f) to (d,g) isa morphismα : c →d in the categoryC so thatthe diagram below commutes:

c f
→ Fc
α ↓ ↓ Fα
d →
g Fd

A coalgebra (d,g) is afinal (orterminal)coalgebra if for every coalgebra (c,f), there is aunique morphism of coalgebrasα : (c,f) → (d,g).

Here is another example as we wind our way backto set theory.These are based on discussions at the beginning of this entry,concerning streams of numbers (Section 1.1).We are dealing with the functorFa =N×a. Then a system of stream equations is a coalgebra forF.To see how this works in a concrete case, we returnto equation (2), reiterated below:

(2) x ≈ ⟨0, y⟩
y ≈ ⟨1, z⟩
z ≈ ⟨2, x⟩

We regard this system as a coalgebra (X,e), whereX = {x,y,z},e(x) = ⟨0,y⟩ , and similarly fore(y) andz(x) .So now we have a concrete example ofa coalgebra for thisF. Anothercoalgebra forF uses the setN^∞ of streams as itscarrier set. The coalgebra itself is

(N^∞, ⟨, ⟩ ).

This coalgebra is final. We shall not verify this here, but instead weapply this point.By finality, there is a uniquee^† : X →N^∞such that the diagrambelow commutes:

Fc f
→ c
Fα ↓ ↓ α
N^∞ →
⟨ , ⟩ N ×N^∞

We now follow the elements ofX around the diagramboth ways.Forx, this tells us that

⟨, ⟩ (e^†(x)) = ⟨0,e^†(y)⟩

That is,e^†(x) is a stream whosefirst component is 0 and whose second component ise^†(y).Similar observations hold fore^†(y)ande^†(z), of course.The upshot is thatthe three streamse^†(x),e^†(y)ande^†(z)are exactly the ones we are after.

Much the same applies to the tree example fromSection 1.2.

4.4 The axioms again

At this point we rephraseFA andAFA to make a comparison.Recall thatV is the class of all sets, and thatV = ℘V. Thismeans that (trivially) the identity on the universe mapsV onto℘V, and vice-versa. Despite this, we want to introduce notationfor these two maps that makes them different. We shall write

i: ℘V →V

Thusitakes a multiplicity (a set of sets) andregards it as a unity (a set).We also have a map in the other direction

j:V →℘V

Thisj takes a set and regards it as a set of sets.

The Foundation Axiom in Algebraic Form. Except for not being a set,(V,i) is an initial algebra for ℘:for all setsa and allf : ℘a →a, there is a uniques : V →f such thatm =f ⋅ ℘m:

℘V i
→ V
℘m ↓ ↓ m
℘a →
f a

The Anti-Foundation Axiom in Coalgebraic Form.Except for not being a set,(V,j) is a final coalgebra for ℘:for every setb and everye:b→ ℘b,there exists a uniques : b →V such thats = ℘s ⋅e:

b e
→ ℘b
s ↓ ↓ ℘s
V →
i ℘V

The maps is called thesolution to thesysteme.

Class forms. We only mentioned forms of the axioms pertainingto sets. They are a little nicer whenstated as axioms on :

FA is equivalent to the assertion that (V,i) is an initial algebra for ℘ on.

AFA is equivalent to the assertion that (V,j) is a final coalgebra for ℘ on.

4.5 Conceptual comparison

A chart just below indicates a kind of conceptual comparison of iterative and coiterative ideas. The entries towards the top aredualities in the categorical sense.Moving downwards, the rows in the chart are more like research directionsthan actual results. So spelling out the details in the chart is more likean ongoing research project than a settled matter.

For many functors on , especially polynomial functorsand the finite power set functor, the initial algebra is the least fixed point together with the identity.For the polynomial functors, this least fixed point is itself an algebra of terms.

algebra for a functor coalgebra for a functor
initial algebra final coalgebra
least fixed point greatest fixed point
congruence relation bisimulation equivalence relation
equational logic modal logic
recursion: map out of an initial algebra corecursion: map into a final coalgebra
Foundation Axiom Anti-Foundation Axiom
iterative conception coiterative conception
set with operations set with transitions and observations
useful in syntax useful in semantics
bottom-up top-down

The connection between greatest fixed points and final coalgebras is thecontent of the following result.

Theorem [Aczel]For every power polynomialF on , the greatest fixed point together with the identity on it, (F^*,id), is a final coalgebra ofF on .Moreover, ifF is a polynomial functor, thenF^* is a set, and (F^*,id)is a final coalgebra ofF on .

The original result used much weaker hypotheses onF, using notions which we did not define, so our statement is rather weaker than in Aczel’s book. Several papershave gone on to weaken strengthen this Final Coalgebra Theorem.

Bisimulation.We have given the definition of bisimulation earlier,inSection 3.1.We discussed it in connection with graphs, but the reader may alsoknow of a notion with the same name coming from modal logic.Actually, the theory of coalgebra studies a more general notion,that of bisimulation on a coalgebra for a given functor, defined firstin Aczel and Mendler (1989).This more general notionspecializes to several concepts which had been proposed in their own fields. In addition, it is (nearly) the dual concept of a congruence onan algebra; this explains our line inthe conceptual comparison chart.

Equational logic and modal logic.A great deal of work has shown ways in which equational logicand modal logic are “dual”, but to spell this out in detail wouldrequire quite a bit more category theory than we need in the restof this entry.

There is a growing fieldof coalgebraic generalizations of modal logic. For a survey ofthis area, see Kurz (2006).

The final coalgebraof a functor may be regarded as a space ofcomplete observations.(As with all our points in this section, this statement is mainly for functors on, and the notion of “complete observation”is, of course, merely suggestive.) For example, letAtProp be a set whose elements arecalledatomic propositions, and consider the functorF(a) = ℘_fin(a) ×℘(AtProp ). A coalgebra for this is a setatogether with one map ofa into its finite subsets, andanother map into the collection of sets of atomic propositions.Putting the two maps together gives afinitely-branchingKripke model: each point has finitely many children and some set ofatomic propositions. Now modal logic gives us a way of“observing” properties of points in coalgebras (Kripkemodels). And the record of everything that one could observe from apoint is the modal theory of that point. Further, one may take thecollection of all theories of all points in all finitely-branchingKripke models and make this collection (it is a set) into the carrierof a final coalgebra for the functor. Indeed, this would be one wayto construct a final coalgebra.

Corecursion. Returning now tothe chart, we present an example of a corecursivedefinition.The equation for given above shows how the function on streams isto work. It should satisfy

(s,t) = ⟨(s), (t, (s))⟩

Here is how is uniquely defined via a corecursive definition.WriteN^∞×N^∞ asS in this discussion.We want a map fromS toN^∞. We are dealing withS as the final coalgebra of the functorFa =N ×a. And we’ll write the structure on the final coalgebra as⟨ ,  ⟩, just as we did it inSection 1.1.The idea is to turnS into the carrier setof a coalgebra for, say (S,f). Then will be the unique coalgebra morphism from (S,f) to (S,⟨ , ⟩ ). It remains to definef.Let

f(s,t) =⟨(s), ⟨t, (s)⟩⟩ .

As mentioned, by finality there is a unique : S →N^∞ so thatthe diagram below commutes:

S f
→ FS
↓ ↓ F
N^∞ →
⟨,⟩ FN^∞

To make sure that this works, we follow an arbitrary pair of streams,say ⟨s,t⟩ around the square, starting in the upper-left. Going down, we have the stream (s,t).From this, the structure takes this to⟨((s,t)), ((s,t))⟩ ∈FN^∞.But we could also take our ⟨s,t⟩ across the top viaf to get ⟨(s), ⟨t, (s)⟩⟩.NowF applies to this pair, and this is where the action ofF as a functorenters. We get ⟨(s),((t),s)⟩.So overall, we have

(s,t)) = (s)

((s,t)) = ((t),s)

just as desired. It says: to zip two streams, start with the head of the first,and then repeat this very process on the second followed by the tail of the first.

The main point of this demonstration is that the principle of finality is sufficient to define and study corecursive definitions. There are many furtherdevelopments in this area.

Sets, again. We have already discussed at length the lines in the table concerning the Foundation and Anti-Foundation Axioms, and their attendant conceptual backgrounds. The point of this section is to situatethat entire discussion inside of a larger one.

Examples of final coalgebras and corecursive definitions. Our conceptual comparison makes the point that algebras embody sets with operations. This point is almost too easy: the reason behind the terminologyof “algebras” in category theory is that sets with operations may be modeledas algebras in the categorical sense. For coalgebras, it is harder to make thecase that they directly correspond to sets with either “transitions” or “observations”.However, we present a few examples that motivate this point.

FunctorFa	coalgebra	final coalgebra	logic
S ×a	stream system	infinite streams overS	a : φ fora ∈S
(S ×a) + 1	stream system, allowing ends	finite and infinite streams overS	add an “end of stream marker”
℘a	graph = Kripke frame = system of set equations	pointed graphs modulo bisimulation	a fragment of infinitary modal, no atoms
℘_fina× ℘(AtProp)	finitely branching Kripke model over thesetAtProp of atomic propositions	a certain subset of the canonical model	a fragment of modal logic overAtProp

The table above lists a few functors on or along withfinal coalgebras or other data from theconceptual comparison chart.

First, for any setS, the functorFa =S×a. A coalgebra for thisF is astream system of equationsas we saw it inSection 1.1, except that therewe made things concrete and tookS to be the set of natural numbers.The final coalgebra is the setS^∞ =S ×S^∞ ofstreams overS. The logical language for this functorwould be a sentential (propositional) language whose sentences are either or of the forms : φ wheres∈S.The semantics would be the obvious one; for example

(0, 1, 2, 3, … ) ⊨ 0 : 1 : 2 : .

One should note that carrier of the final coalgebra may be taken to be certain theories in this language. These may be described extrinsically asthe theories of all points in all coalgebra. It is more informative, however, to set down a logical system and then consider the maximal consistent sets in the system.With the right definition, the maximal consistent sets do turn out to be the carrier of afinal coalgebra for the functor.

Second, we considerFa = (S ×a) + 1.Here 1 = {0} and + is the disjoint union operation. However, it is more common for people to represent the one and only element of 1 using a symbol like*.The coalgebras are like stream systems of equations, except now anequation might ask for a stream to “stop” by having * on the right-hand side.So an example of a coalgebra would bex ≈ ⟨s,y⟩ ,y ≈*.Then the solution would takex^† to be the one-term sequences.The logic for this functor would be the same logic (HML) as before, except thatnow we add an atomic sentence to detect the ends of finite sequences.

Turning to the last two lines, we already know thatAFA is equivalent tothe assertion that (V,id) is a final coalgebra of ℘; also, even withoutAFA, we have a final coalgebra whose carrier set is the pointed graphs modulobisimulation. The logic in this case is infinitary modal logic,actually, it is a fragment of this logic. It turnsout that two points in a given coalgebra have the same infinitary modal theoryiff they are bisimilar.

The line concerning ℘_fin(a) × ℘(AtProp) is the closest to the Kripke semantics of modal logic. One might hope that the final coalgebrawould turn out to be the canonical model of the modal logicK, but this is notquite right. One needs to cut down to those maximal consistent sets which arerealized by some point in somefinitely branching model.

As the reader may notice, we are being extremely vague about mattersconcerning the logics: is there a principled explanation of where they come from?What, if anything,is the relation between the final coalgebras andcanonical modelsas we find them in modal logic? The explanations here are too long and tooinvolved for this entry. Once again,one place to start reading about these matters is Kurz (2006).

The lines in at the bottom of theconceptual comparison chart are the most programmatic of all.

Doing withoutAFA: final coalgebrasinZF. We mentioned in note [2] that it is possible to alter the pairingoperation in such a way that one may prove many of the results thatour treatment obtains only by usingZFA. This points ismentioned in Forster (1994) and developed in detail in Paulson (1999)(and in other papers by Paulson). One replaces the Kuratowski pair⟨x,y⟩ with a variant,({0}×a)∪ ({1}×b). (This is theusual disjoint union operation, also called thecoproduct onsets.) Then one defines variants of other notions: the cartesianproduct, functions, etc. And in terms of these one can indeed studystreams and infinite trees, and many other sets of interest in thisentry. Even more, one can provefinal coalgebra theorems, stating sufficient conditionsfor the existence of a final coalgebra whose structure is the identity.(This is an important point for this line of work: inZF we can show the existence of final coalgebras for the same functors as inZFA, but in the latter theory we can get final coalgebras whosestructure maps are the identity.)

One might think that this move undermines much of the interestinAFA. For Paulson, the reduction is important since he wantsto use an automatic theorem prover to work with assertions in set theory.It makes sense to work out detailed reductions so as to avoid changingthe set theory.

Otthers may not find this conclusive, for two reasons. First, themethod doesn’t apply to equations likex ={x}, or to collections likex = ℘_fin(x). The latter kind ofequation is especially useful in applications. But even more, whatwill be of interest will be the whole assembly of what we mightcallcoalgebraic concepts: coinduction, corecursion, andtop-down treatments of various phenomena. Someone who is using theseconcepts and is also worried about modeling in set theory wouldprobably find it convenient to work withAFA, even if many ofthe end applications could be done in standard set theory.

To put things differently, and to ask a question that surely belongsin this entry, why should one work withAFA insteadofFA? Much depends on the purposes one brings to settheoretic modeling in the first place. For most purposes, includingmost of mathematics, it makes little or no difference. To model somecircular phenomena, it turns out to be convenient to work with finalcoalgebras of various functors. It is especially nice with thestructure maps on those final coalgebras may be taken to be theidentity function. For example, this would allow us to say that astream of numbers really and truly is an ordered pair of a number anda stream. In this case, havingAFA would be nice, but theresults above show that in many of the interesting cases, it is notactually needed. On the other hand, if one is content to work withisomorphisms, then having the structure map be the identity is a kindof “optional extra”. Further, the question of which axiomto adopt might appear to be besides the point.

Interested readers may consult the following supplementarydocument for a discussion of how the more general ideas from coalgebraand closely related fields help with discussions of the kinds ofmathematical circularity which we looked at previously.

Additional related modeling of circularity

Conclusion

This entry has two major thrusts. First, it introducednon-wellfounded sets and described some of the mathematics aroundthem. It was not comprehensive in this regard, and one should seePeter Aczel’s book (1988) for much more, includingdiscussions of axioms besidesAFA that we did not even mention.One could also see Barwise and Moss (1996) for more on some of thepoints that were touched on here.^[13] The presentation owes much to work in coalgebra that beganshortly after these books appeared. So readers familiar with eitherof them would still find something new in the first sections of theentry.

The other thrust had to do with the conceptual points made inSection 4.5.The idea is to situate themathematics of set theoretic circularity inside a larger topic,coalgebra, and then to understand both points in terms of a largerdivision between “bottom-up” and “top-down”ideas. This larger discussion is more programmatic than we wouldlike, and much remains to be done on it. Our hope is that it helpsreaders understand set theoretic circularity, bothhow itworks, and alsowhy it is attractive.

Bibliography

Aczel, P., 1988,Non-Well-Founded Sets (CSLI LectureNotes: Number 14), Stanford: CSLI Publications.
Aczel, P. and Mendler, N., 1989, ‘A final coalgebratheorem,’ in D. H. Pitt et al. (eds.),Category Theory andComputer Science, Heidelberg: Springer-Verlag,357–365.
Adámek, J., and Reitermann, J., 1994, ‘Banach’sFixed-Point Theorem as a Base for Data-Type Equations,’Applied Categorical Structures, 2: 77–90.
Alexandru Baltag, 2000, ‘STS: A Structural Theory ofSets,’ in Michael Zakharyaschev, Krister Segerberg, Maarten deRijke & Heinrich Wansing (eds.),Advances in Modal Logic(Volume 2), Stanford: CSLI Publications,. 1–34.
Barwise, J., and Etchemendy, J., 1987,The Liar, Oxford: Oxford University Press.
Barwise, J., and Moss, L., 1991, ‘Hypersets’,The Mathematical Intelligencer, 13(4): 31–41.
Barwise, J., and Moss, L., 1996,Vicious Circles (CSLILecture Notes: Number 60), Stanford: CSLI Publications.
Böge, W., and Eisele, T., 1979, ‘On solutions ofBayesian games,’International Journal of Game Theory,8(4): 193–215.
Boolos, G., 1971, ‘The iterative conception of set,’The Journal of Philosophy, 68: 215–231.
Burgess, J., 1985, Reviews,Journal of Symbolic Logic, 50(2): 544–547.
Corfield, D., 2011, ‘Understanding the Infinite II:Coalgebra,Studies in History and Philosophy of Science (A),42: 571–579.
Edalat, A., 1995, ‘Dynamical Systems, Measures and Fractalsvia Domain Theory,’Information and Computation,120(1): 32–48.
Thomas Forster, 1994, ‘Why Set theory without the axiom offoundation?’Journal of Logic and Computation, 4(4):333–335.
Forti, M. and Honsell, F., 1983, ‘Set theory withfree construction principles‘,Annali Scuola Normale Superioredi Pisa, Classe di Scienze, 10: 493–522.
Harsanyi, J. C., 1967, ‘Games with incomplete informationplayed by ‘Bayesian’ players. I. The basic model,’Management Science, 14: 159–182.
Hayashi, S., 1985, ‘Self-similar sets as Tarski’s fixedpoints,’,Publications of the Research Institute forMathematical Sciences, 21(5): 1059–1066.
Heifetz, A., and Samet, D., 1998, ‘Topology-free typology ofbeliefs,’Journal of Economic Theory, 82(2):324–341.
Incurvati, Luca, 2014, ‘The Graph Conception of Set,’Journal of Philosophical Logic, 43(1): 181–208.
Jacobs, B. and Rutten, J., 1997, ‘A Tutorial on (Co)Algebrasand (Co)Induction’, inBulletin of the European Associationfor Theoretical Computer Science, 62: 222–259.
Kurz, A., 2006, ‘Coalgebras and Their Logics’,ACMSIGACT News, 37(2): 57–77.
Levy, A., 1979,Basic Set Theory, Berlin:Springer-Verlag.
Milius, S., 2005, ‘Completely iterative algebras andcompletely iterative monads,’Information andComputation, 196: 1–41.
Moss, L., and Viglizzo, I., 2006, ‘Final coalgebras forfunctors on measurable spaces,’Information andComputation, 204(4): 610–636.
Parsons, C., 1975, ‘What is the iterative conception ofset?’, in Hintikka and Butts (eds.),Logic, foundations ofmathematics and computability theory (University of WesternOntario Series in the Philosophy of Science, Volume 9: Proceedings ofthe Fifth International Congress on Logic, Methodology and thePhilosophy of Science, University of Western Ontario, London, Ontario,1975), Dordrecht: Reidel, 1977, Part I, pp. 335–367.
Paulson, L., 1999, ‘Final coalgebras as greatest fixedpoints in ZF set theory,’Mathematical Structures inComputer Science, 9: 545–567.
Pavlovic, D., and M. H. Escardo, 1998,‘Calculus in Coinductive Form,’ in13th Annual IEEE Symposium in Logic in Computer Science(LICS 98), Los Alamitos, CA: IEEE,408–417. doi:10.1109/LICS.1998.705675
Rieger, A., 2000, ‘An argument for Finsler-Aczel set theory,’Mind, 109(434): 241–253. doi:10.1093/mind/109.434.241
Rutten, J., 2000, ‘Universal coalgebra: a theory ofsystems,’Theoretical Computer Science, 249(1):3–80.
Turi, D., and Rutten, J., 1998, ‘On the foundations of finalsemantics: non-standard sets, metric spaces, partial orders,’Mathematical Structures in Computer Science, 8(5):481–540.
Viglizzo, I., 2005,Coalgebras on measurable spaces,Ph.D. Dissertation, Indiana University, Bloomington.

Academic Tools

How to cite this entry.
Preview the PDF version of this entry at theFriends of the SEP Society.
Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

Bart Jacobs,Introduction to Coalgebra. Towards Mathematics of States and Observations [PDF] (book draft)
Freyd, P., 1999, ‘Real coalgebra’, web posting onthe Categories (mailing) List, 22 December 1999,available via the mailing list archive.

Acknowledgments

I would like to thank Edward Zalta and Uri Nodelman for theiradvice, encouragement, and patience. I also thank Maricarmen Martinezfor her comments on an earlier version of this entry.

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free

Browse

About

Support SEP

Mirror Sites

View this site from another server:

USA (Main Site)Philosophy, Stanford University

Info about mirror sites

Library of Congress Catalog Data: ISSN 1095-5054

Movatterモバイル変換