Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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
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
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.
Also, the given definition of the membership relation above implies that 1 is a reflexive set.
There are really multiple issues going here with regards to material and structural set theories.
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.
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.
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:
The defined membership predicate $\in$ is strongly extensional if the equality relation for fully formal ETCS is the terminal bisimulation.
Anyhow I’ve created a question on mathoverflow for whether the defined $\in$ above in any strict well-pointed topos is strongly extensional
@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.
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$.
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.
@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}$.
@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.
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”.
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.
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.
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.
Madeleine,
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
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
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
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
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)$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
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.
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$.
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.
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.
Adding reference
Anonymouse
1 to 41 of 41