# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

1. starting discussion page

Anonymous

• CommentRowNumber2.
• CommentAuthorGuest
• CommentTimeOct 20th 2022

So let me get this clear.

Is the difference between material set theory and structural set theory is that in the former, the membership $\in$ is a predicate in first order logic, while in the latter, the membership $\in$ is a typing judgment? Or is the difference between material set theory and structural set theory is that in the former, sets and elements are regarded as the same kinds of objects (one-sorted first order theory), while in the latter, sets and elements are regarded as two different kinds of objects (multiple or dependently sorted first order theory)?

Because in dependent type theory, the corresponding thing to membership in set theory is the typing judgment represented by the colon $a:A$. However, there are two different presentations of dependent type theory used in the community. One presentation includes a separate type judgment $A \; \mathrm{type}$ in addition to the typing judgment $a:A$, and thus inherently treats types and terms differently. The other presentation does not include any type judgments at all, but rather a hierarchy of universes $U_i$ such that $U_i:U_{i + 1}$, and treats types and terms as the same thing: types are terms of universes. The former presentation is used in Jon Sterling’s most recent article on XTT, as well as Egbert Rijke’s Introduction to Homotopy Type Theory textbook, while the latter presentation is used in the Univalent Foundations Project’s HoTT book.

• CommentRowNumber3.
• CommentAuthorGuest
• CommentTimeOct 20th 2022

Or is the difference between material set theory and structural set theory is that in the former, sets and elements are regarded as the same kinds of objects (one-sorted first order theory), while in the latter, sets and elements are regarded as two different kinds of objects (multiple or dependently sorted first order theory)?

ETCS is regarded as a structural set theory but there is a presentation of ETCS with only one sort (sets are identity functions) written by Todd Trimble at fully formal ETCS.

John Jacobs

• CommentRowNumber4.
• CommentAuthorGuest
• CommentTimeOct 20th 2022

Is the difference between material set theory and structural set theory is that in the former, the membership $\in$ is a predicate in first order logic, while in the latter, the membership $\in$ is a typing judgment?

Also, fully formal ETCS doesn’t have the membership symbol $\in$ in its theory, whether as a predicate or as a typing declaration.

John Jacobs

• CommentRowNumber5.
• CommentAuthorGuest
• CommentTimeOct 20th 2022

One could however define the global membership symbol $\in$ in fully formal ETCS as a global binary relation on the single sort of morphisms. Fully formal ETCS has a symbol $1$ for the identity morphism of the terminal object, elements are represented by morphisms with source $1$, and sets are represented by morphisms with target $1$. We then define the global membership symbol $a \in A$ as

$a \in A \coloneqq (t(A) = 1) \wedge (s(a) = 1) \wedge (s(A) = t(a))$

So I think fully formal ETCS is a material set theory rather than a structural set theory.

• CommentRowNumber6.
• CommentAuthorGuest
• CommentTimeOct 20th 2022

Also, the given definition of the membership relation above implies that 1 is a reflexive set.

• CommentRowNumber7.
• CommentAuthorGuest
• CommentTimeOct 20th 2022

There are really multiple issues going here with regards to material and structural set theories.

1. Whether the set theory is single sorted/unsorted or has multiple (possibly dependent) sorts
2. Whether the set theory has a membership predicate, or a membership typing judgment $\in$, or neither.
3. If the set theory has a membership predicate $\in$, whether the membership predicate is a primitive or derived concept.
4. Whether there exists a element/set $A$ such that there exists elements/sets $x$ and $y$ such that $x \in A$ and $A \in y$.
2. added section on fully formal ETCS

Anonymous

• CommentRowNumber9.
• CommentAuthorGuest
• CommentTimeOct 20th 2022

The main distinguishing feature of a material set theory is a global membership predicate, whereby it is meaningful to ask, given any object and a set, whether the object is an element of the set. A set’s identity here is determined by its elements, in other words the axiom of extensionality holds.

Since fully formal ETCS has a (derived) global membership predicate which is an extensional relation, either it is a material set theory or these two sentences needs to be modified or removed from the article.

• CommentRowNumber10.
• CommentAuthorGuest
• CommentTimeOct 20th 2022

Well-pointedness for fully formal ETCS implies that the defined membership relation $\in$ is only weakly extensional. However, the axiom of foundation fails in fully formal ETCS with respect to the defined $\in$, which means that weak extensionality isn’t the right axiom of extensionality for $\in$. Instead, one has to show that $\in$ is strongly extensional in order for it to be a material set theory.

• CommentRowNumber11.
• CommentAuthorGuest
• CommentTimeOct 20th 2022

A bisimulation in fully formal ETCS is a binary relation $\sim$ such that for all morphisms $x$ and $y$ such that $x \sim y$, the following conditions hold:

• for all morphisms $a$ such that $a \in x$, there exists a morphism $b$ such that $b \in y$ and $a \sim b$
• for all morphisms $b$ such that $b \in y$, there exists a morphism $a$ such that $a \in x$ and $a \sim b$

The defined membership predicate $\in$ is strongly extensional if the equality relation for fully formal ETCS is the terminal bisimulation.

• CommentRowNumber12.
• CommentAuthorGuest
• CommentTimeOct 20th 2022

Anyhow I’ve created a question on mathoverflow for whether the defined $\in$ above in any strict well-pointed topos is strongly extensional

https://mathoverflow.net/questions/432874/strong-extensionality-of-membership-relation-defined-on-the-set-of-all-morphis

• CommentRowNumber13.
• CommentAuthorGuest
• CommentTimeOct 20th 2022

@12

One doesn’t need well-pointedness for weak extensionality of your defined $\in$ to hold. The composites $f \circ x$ and $g \circ x$ only exist if $f$ and $g$ have the same source, which is the target of $x$. If $x$ has source the terminal object $1$ and If the target of both $f$ and $g$ is also $1$, then the composite $f \circ x$ and $g \circ x$ is the identity morphism on $1$, and so $f \circ x$ and $g \circ x$ are always the same. Furthermore, if the target of $f$ and $g$ is $1$, and the source of $f$ and $g$ is the same, then $f$ and $g$ are the same by the universal property of the terminal object. Thus, weak extensionality of your $\in$ holds in all categories with a terminal object $1$.

This is why in topos theory one talks about function extensionality rather than the axiom of extensionality.

• CommentRowNumber14.
• CommentAuthorGuest
• CommentTimeOct 20th 2022

Anyways, back to the original topic of this discussion. I highly suspect that in any unsorted first order theory where some objects are meant to represent sets and some objects in the theory are meant to represent elements, one could define a global membership endorelation $\in$ which is extensional, and $a \in A$ if $a$ is meant to be an element of the set $A$.

• CommentRowNumber15.
• CommentAuthorGuest
• CommentTimeOct 21st 2022

A general unsorted first order theory of sets should have predicates $\mathrm{isSet}$ and $\mathrm{isElem}$ in addition to the global membership $\in$, such that

$\forall a.(\neg \mathrm{isSet}(a) \implies \neg \exists b.b \in a)$ $\forall a.(\neg \mathrm{isElem}(a) \implies \neg \exists b.a \in b)$

In ZFC, $\mathrm{isSet}(a)$ and $\mathrm{isElem}(a)$ are both $\top$ for all objects $a$, so the statements are trivially true by the principle of explosion. But in fully formal ETCS, there are nontrivial objects $f$ where both $\mathrm{isSet}(f)$ and $\mathrm{isElem}(f)$ are $\bot$, namely the functions for which both sorurce and target are not isomorphic to the terminal object.

3. @5, 8

Fully formal ETCS is not a material set theory, because your membership relation $\in$ defined there is not strongly extensional. The relation $\sim$ defined by equality on every pair of functions $a \sim b := a = b$, and in addition, $\mathrm{id}_2 \sim \mathrm{swap}$ and $\mathrm{swap} \sim \mathrm{id}_2$ for the identity function and the swap function on the set with two elements $2$, is a bisimulation on $\in$, but it is not true that $\mathrm{id}_2 = \mathrm{swap}$.

• CommentRowNumber17.
• CommentAuthorGuest
• CommentTimeOct 21st 2022

@9

That paragraph needs to be rewritten to be made clearer.

In any two-sorted structurally presented set theory with types representing probable sets $Set$ and probable elements $El$, one could define a global membership predicate $\Gamma, x:El, A:Set \vdash \in \; \mathrm{prop}$ where $x \in A$ if and only if $\mathrm{set}(A)$ and $\mathrm{in}_A(x)$. So the global membership predicate alone isn’t sufficient for a theory to be a material set theory, nor is it the distinguishing feature of a material set theory. One needs the theory to be an unsorted theory with a global membership predicate which is strongly extensional, to exclude theories like ETCS.

• CommentRowNumber18.
• CommentTimeOct 21st 2022
• (edited Oct 21st 2022)

Somehow I got logged out of the nForum before I wrote the previous comment.

What I meant when I said “structurally presented set theory” is actually “first order theory with a notion of set”.

• CommentRowNumber19.
• CommentAuthorGuest
• CommentTimeOct 21st 2022

Todd Trimble’s fully formal ETCS is not a structural set theory because in a structural set theory, elements of different sets cannot be compared for equality. But in fully formal ETCS, elements of different sets can be compared for equality because there is a global equality predicate. If one wants to make Todd Trimble’s fully formal ETCS a structural set theory, one has to first work in first order logic without equality, and then define local equality of morphisms to be a quaternary predicate on the morphisms.

4. Added info emphasizing that material set theories have a global equality on the sets/elements.

Anonymous

• CommentRowNumber21.
• CommentAuthorUrs
• CommentTimeOct 21st 2022

I suppose you all are acting in good faith, but can’t you see that a discussion between people all signing by the same pseudonym is a disservice to the community? Also to yourselves, I would think.

Preparations to disable all guest accounts is underway, though I wished we would not have to take this step. I am at a loss for why this has become an issue in the last months.

• CommentRowNumber22.
• CommentAuthorHurkyl
• CommentTimeOct 21st 2022
• (edited Oct 21st 2022)

I’m not sure the distinction of #19 is that meaningful. One can mechanically replace a local equality predicate with a global one by extending it by “false”, and conversely restrict a global one to a local one by defining the local one to defer to the global judgement.

The only reason that you have global equality in that formalization anyways is an artifact of choosing the “type of arrows” formalization of categories, rather than the “type of objects and dependent type of morphisms” formalization.

• CommentRowNumber23.
• CommentAuthorGuest
• CommentTimeOct 21st 2022

Requiring strong extensionality in the definition of material set theory would mean that Zermelo set theory is excluded from the definition of material set theory.

Mary Brasier

5. Added a better characteristic of the difference between material and structural set theories in terms of the membership graphs of the set theories. This definition puts fully formal ETCS strictly in the structural set theory camp, while putting ZFC and ZFA in the material set theory camp.

I have moved the pre-existing definition to a separate section titled “materially presented set theories”, to parallel the existing article structurally presented set theory

Anonymous

• CommentRowNumber25.
• CommentAuthorGuest
• CommentTimeOct 24th 2022

The fact that the morphism representing a terminal object is a Quine atom means that neither identity functions nor functions into a singleton are the right notion of set. The right notion of set is actually a function out of empty set. That way, sets and elements are always different in any model of unsorted ETCS.

John Weaver

• CommentRowNumber26.
• CommentAuthorGuest
• CommentTimeOct 24th 2022

Meant to say, “the morphism representing the terminal object is a Quine atom, as currently defined in the article”. Properly defined, no morphism should be a reflexive morphism with respect to the membership relation.

John Weaver

• CommentRowNumber27.
• CommentAuthorGuest
• CommentTimeOct 24th 2022

John,

No, it just means that there are three different models of material sets in any model of ETCS, as identity functions, as functions into the specified singleton $1$, and as functions from the specified empty set $\emptyset$, and thus three different models of the membership relation $\in$ in ETCS. The first two have a Quine atom, while the third doesn’t.

This is true also of any structural presentation or dependent type theoretic model of ETCS $\mathcal{E}$, where the three membership relations $\in$ are defined on the type

$\sum_{A:Ob(\mathcal{E})} \sum_{B:Ob(\mathcal{E})} Hom(A, B)$
• CommentRowNumber28.
• CommentAuthorGuest
• CommentTimeOct 24th 2022

The key characteristic of structural set theory is not what was added to the article in 24. Instead, it is that given objects $a$ and $b$ in a unsorted set theory, if $\mathrm{set}(a)$ and $\mathrm{set}(b)$, then $\neg (a \in b)$. The definition of $\mathrm{set}(a)$ as $s(a) = 0$, where $0$ is the identity function on the empty set, means that the membership relation $a \in b$ is defined as $s(a) = 1$ and $s(b) = 0$ and $t(a) = t(b)$, where $1$ is the identity function on the singleton. The only time that $a \in b$ when $a$ is a set is in the trivial theory where $0 = 1$.

John Weaver

• CommentRowNumber29.
• CommentAuthorGuest
• CommentTimeOct 24th 2022

The definition of set using morphisms from the initial object also makes sense in a single-sorted allegory-based set theory, like whatever the single-sorted version of SEAR is. A set $S$ is just a relation whose domain $\emptyset$ is the identity relation on the empty set.

John Weaver

• CommentRowNumber30.
• CommentAuthorHurkyl
• CommentTimeOct 24th 2022
• (edited Oct 24th 2022)

I can’t agree with #28. The underlying philosophical issue here is whether the ’meaning’ of a set is derived from its relationship to other sets (structural) or derived from the ’meaning’ of its elements (material).

And thus, in a structural set theory, any set-theoretic proposition must respect isomorphisms. If a proposition about a set with an element is true, it must be true for any other isomorphic data – such as the same set with another element. This idea is what I think #24 means to encode.

The distinction described in #28 sounds more like about whether you’re encoding a multi-sorted theory in an unsorted formalism.

6. added clarification that singletons can be represented in two different ways in unsorted structural set theory: as a tree whose root only has one child which is also a leaf of the tree, as well as a Quine atom.

Anonymous

7. expanded on the example of fully formal ETCS, as there are three ways to define sets in fully formal ETCS

Anonymous

• CommentRowNumber33.
• CommentAuthorHurkyl
• CommentTimeOct 24th 2022
• (edited Oct 24th 2022)

Well, you’re describing three ways to recover the notion of “object” from the “arrows-only” description of a category.

There are other ways to formalize the notion of set using a topos. For example, you could define a set to be an element (or generalized element) of an object in the form $PA$. E.g. I have a book by Bell (Toposes and Local Set Theories) that defines a “set-like term” in this fashion. In this case $\in$ could be described as a family of arrows $A \times PA \to \Omega$.

8. three -> many

Anonymous

9. material moved to unsorted set theory

Anonymous

10. added sentence addressing the difference between the material/structural distinction and the sorted/unsorted distinction

Anonymous

• CommentRowNumber37.
• CommentAuthorGuest
• CommentTimeOct 24th 2022

To answer the question in #2, the answer is no, whether $\in$ is a predicate or a typing judgment doesn’t matter. One could write the type judgments as $A \; \mathrm{set}$ instead of $A \; \mathrm{type}$ and the typing judgments as $a \in A$ instead of $a:A$, and include an term reflection rule which turns every term into a type/set

$\frac{\Gamma \vdash A \; \mathrm{set} \quad \Gamma \vdash a \in A}{\Gamma \vdash a \; \mathrm{set}}$

This is the generalization of one of the rules for Russell universes to all types/sets.

Anonymous

12. put the information about unsorted material set theories into its own section

Anonymous

• CommentRowNumber40.
• CommentAuthorUrs
• CommentTimeNov 14th 2022

I have added a link to material versus structural set theory back to the beginning of the entry, so that the reader has a better chance of seeing it.