I added a section on **Motivation**. I'm still unsure about the section **Formalisation in material set theory**, as well as the discussion of material set theory in **Idea**. I suppose that this stuff is unarguably correct if we wish to define ‘pure set’ in a material set theory (especially one which allows atoms), but it still seems to me beside the point (and rather trivial).

Perhaps we should move the page to material set; it's really about how to formalise material sets within a structural set theory, and we restrict to the pure ones for the sake of simplicity. (Although ‘pure material set’ is redundant, since there is no structural notion of a pure set as a set with the property or structure of purity, as you remarked earlier.)

]]>Sounds good to me.

]]>The term ‘pure’ in the second sense can still an adjective, just an adjective denoting structure instead of property, such as ‘monoidal’ in ‘monoidal category’. However, the set which is given the structure (the set of nodes in the graph) is not really the set that we are talking about; for finite sets, at least, it does not even have the correct cardinality. So after all that, I agree, the second meaning should take ‘pure set’ as an unanalysable noun in its own right.

I think that the reason that I used the name pure set for this article was something like this: There is an intuitive conception of what a set is in material set theory, and this is something which needs to be modelled by mathematics; in particular, it needs to be modelled by structural mathematics if that is to encompass all of mathematics. In its simplest form (without atoms), this concept is known to set theorists as a ‘pure set’. So that is the concept at hand; the article discusses how to model those in (structural) mathematics. I use it because it is the term of art in (material) set theory, at least the term used when ‘set’ simple is not being used (and that term is not available to us for this purpose).

Maybe I'll write a little introductory bit along those lines.

]]>I finished the reorganization of pure set that I had in mind. We should continue the terminological discussion.

]]>Fair enough. I guess it would be more appropriate to talk about just two ways of interpreting "pure set," either with "pure" as an adjective (which only makes sense materially), or with "pure set" as a noun (which makes sense structurally, and hence also materially).

I wonder whether it is really a good idea to use "pure set" with the second meaning. I mean, really what we're talking about are structures which *model* or *imitate* the (adjectival) notion of a pure set in material set theory, right?

There is a bit of a mismatch between what we get with the formalisation in material vs structural set theories. One point about the formalisation in structural set theory is that it works also in material set theory; of course, this is just because every material set theory defines a structural set theory. (More than that, the formalisation works precisely as written, that is in the same informal language; of course, this is because the interpretation of structural set theory in material set theory uses the same language, just a smaller portion of it.) The reason that this is important is that we can define a notion of possibly ill-founded pure set *even if* our material set theory includes an axiom of foundation.

In fact, this is what Aczel does, as you can see when he proves theorems about the correspondence between sets and well-founded APGs; he is working in a well-founded material set theory. So while I like the new section on the formalisation of pure sets within material set theory, as far as it goes, I don't like saying that the other section is about formalisation within structural set theory. The formalisation there is also important even if one is using a material set theory.

I'm not writing anything now, because the page is locked, but I may rearrange things further in light of this.

]]>While watching your work in progress (an hour ago when you wrote this), I had the same thought about the organisation.

]]>I'm in the process of reworking pure set to incorporate those of AN's points that were valid and remove as many of the query-boxes as possible, in order to make it readable.

Right now, the page describes trees, and then extensional graphs, and then briefly mentions the more general notion of which these are specializations. I would find it more intuitive, and more concise, to first describe the general notion, and then introduce trees and extensionality as two ways of ensuring that equivalent graphs (in the loose "bisimulation" sense appropriate for the general notion) are in fact isomorphic. Unless someone objects, I'll probably reorganize it that way.

]]>