Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory object of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthornLab edit announcer
   • CommentTimeOct 20th 2022
   • PermaLink
   Author: nLab edit announcer
   Format: MarkdownItexstarting discussion page Anonymous <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/8">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/8">v8</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

   starting discussion page

   Anonymous

   diff, v8, current

2. • CommentRowNumber2.
   • CommentAuthorGuest
   • CommentTimeOct 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexSo 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]].

   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.

3. • CommentRowNumber3.
   • CommentAuthorGuest
   • CommentTimeOct 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItex> 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

   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

4. • CommentRowNumber4.
   • CommentAuthorGuest
   • CommentTimeOct 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItex> 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

   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

5. • CommentRowNumber5.
   • CommentAuthorGuest
   • CommentTimeOct 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexOne 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.

   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.

6. • CommentRowNumber6.
   • CommentAuthorGuest
   • CommentTimeOct 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexAlso, the given definition of the membership relation above implies that 1 is a [[reflexive set]].

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

7. • CommentRowNumber7.
   • CommentAuthorGuest
   • CommentTimeOct 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexThere 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$.

   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$.
8. • CommentRowNumber8.
   • CommentAuthornLab edit announcer
   • CommentTimeOct 20th 2022
   • PermaLink
   Author: nLab edit announcer
   Format: MarkdownItexadded section on fully formal ETCS Anonymous <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/9">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/9">v9</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

   added section on fully formal ETCS

   Anonymous

   diff, v9, current

9. • CommentRowNumber9.
   • CommentAuthorGuest
   • CommentTimeOct 20th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItex> 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.

   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.

10. • CommentRowNumber10.
    • CommentAuthorGuest
    • CommentTimeOct 20th 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexWell-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.

    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.

11. • CommentRowNumber11.
    • CommentAuthorGuest
    • CommentTimeOct 20th 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexA [[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.

    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.

12. • CommentRowNumber12.
    • CommentAuthorGuest
    • CommentTimeOct 20th 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexAnyhow 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](https://mathoverflow.net/questions/432874/strong-extensionality-of-membership-relation-defined-on-the-set-of-all-morphis)

    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

13. • CommentRowNumber13.
    • CommentAuthorGuest
    • CommentTimeOct 20th 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItex@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.

    @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.

14. • CommentRowNumber14.
    • CommentAuthorGuest
    • CommentTimeOct 20th 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexAnyways, 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$.

    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$.

15. • CommentRowNumber15.
    • CommentAuthorGuest
    • CommentTimeOct 21st 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexA 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.

    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.

16. • CommentRowNumber16.
    • CommentAuthorMadeleine Birchfield
    • CommentTimeOct 21st 2022
    • PermaLink
    Author: Madeleine Birchfield
    Format: MarkdownItex@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}$.

    @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}$.

17. • CommentRowNumber17.
    • CommentAuthorGuest
    • CommentTimeOct 21st 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItex@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.

    @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.

18. • CommentRowNumber18.
    • CommentAuthorMadeleine Birchfield
    • CommentTimeOct 21st 2022
    • (edited Oct 21st 2022)
    • PermaLink
    Author: Madeleine Birchfield
    Format: MarkdownItexSomehow 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".

    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”.

19. • CommentRowNumber19.
    • CommentAuthorGuest
    • CommentTimeOct 21st 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexTodd 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.

    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.

20. • CommentRowNumber20.
    • CommentAuthornLab edit announcer
    • CommentTimeOct 21st 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdded info emphasizing that material set theories have a global equality on the sets/elements. Anonymous <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/10">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/10">v10</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

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

    Anonymous

    diff, v10, current

21. • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeOct 21st 2022
    • PermaLink
    Author: Urs
    Format: MarkdownItexI 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 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.

22. • CommentRowNumber22.
    • CommentAuthorHurkyl
    • CommentTimeOct 21st 2022
    • (edited Oct 21st 2022)
    • PermaLink
    Author: Hurkyl
    Format: MarkdownItexI'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.

    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.

23. • CommentRowNumber23.
    • CommentAuthorGuest
    • CommentTimeOct 21st 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexMadeleine, 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

    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

24. • CommentRowNumber24.
    • CommentAuthornLab edit announcer
    • CommentTimeOct 21st 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdded 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 <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/12">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/12">v12</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

    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

    diff, v12, current

25. • CommentRowNumber25.
    • CommentAuthorGuest
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexThe 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

    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

26. • CommentRowNumber26.
    • CommentAuthorGuest
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexMeant 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

    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

27. • CommentRowNumber27.
    • CommentAuthorGuest
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexJohn, 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)$$

    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)$$
28. • CommentRowNumber28.
    • CommentAuthorGuest
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexThe 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

    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

29. • CommentRowNumber29.
    • CommentAuthorGuest
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexThe 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

    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

30. • CommentRowNumber30.
    • CommentAuthorHurkyl
    • CommentTimeOct 24th 2022
    • (edited Oct 24th 2022)
    • PermaLink
    Author: Hurkyl
    Format: MarkdownItexI 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.

    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.

31. • CommentRowNumber31.
    • CommentAuthornLab edit announcer
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexadded 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 <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/14">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/14">v14</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

    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

    diff, v14, current

32. • CommentRowNumber32.
    • CommentAuthornLab edit announcer
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexexpanded on the example of fully formal ETCS, as there are three ways to define sets in fully formal ETCS Anonymous <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/14">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/14">v14</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

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

    Anonymous

    diff, v14, current

33. • CommentRowNumber33.
    • CommentAuthorHurkyl
    • CommentTimeOct 24th 2022
    • (edited Oct 24th 2022)
    • PermaLink
    Author: Hurkyl
    Format: MarkdownItexWell, 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$.

    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$.

34. • CommentRowNumber34.
    • CommentAuthornLab edit announcer
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexthree -> many Anonymous <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/14">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/14">v14</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

    three -> many

    Anonymous

    diff, v14, current

35. • CommentRowNumber35.
    • CommentAuthornLab edit announcer
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexmaterial moved to [[unsorted set theory]] Anonymous <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/14">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/14">v14</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

    material moved to unsorted set theory

    Anonymous

    diff, v14, current

36. • CommentRowNumber36.
    • CommentAuthornLab edit announcer
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexadded sentence addressing the difference between the material/structural distinction and the sorted/unsorted distinction Anonymous <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/14">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/14">v14</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

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

    Anonymous

    diff, v14, current

37. • CommentRowNumber37.
    • CommentAuthorGuest
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: Guest
    Format: MarkdownItexTo 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.

    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.

38. • CommentRowNumber38.
    • CommentAuthornLab edit announcer
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexadded context sidebar Anonymous <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/18">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/18">v18</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

    added context sidebar

    Anonymous

    diff, v18, current

39. • CommentRowNumber39.
    • CommentAuthornLab edit announcer
    • CommentTimeOct 24th 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexput the information about unsorted material set theories into its own section Anonymous <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/18">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/18">v18</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

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

    Anonymous

    diff, v18, current

40. • CommentRowNumber40.
    • CommentAuthorUrs
    • CommentTimeNov 14th 2022
    • PermaLink
    Author: Urs
    Format: MarkdownItexI 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. <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/23">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/23">v23</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

    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.

    diff, v23, current

41. • CommentRowNumber41.
    • CommentAuthornLab edit announcer
    • CommentTimeMay 17th 2024
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexAdding reference * [[Håkon Robbestad Gylterud]], [[Elisabeth Stenholm]], *Univalent material set theory* ([arXiv:2312.13024](https://arxiv.org/abs/2312.13024)) Anonymouse <a href="https://ncatlab.org/nlab/revision/diff/material+set+theory/26">diff</a>, <a href="https://ncatlab.org/nlab/revision/material+set+theory/26">v26</a>, <a href="https://ncatlab.org/nlab/show/material+set+theory">current</a>

    Adding reference

    • Håkon Robbestad Gylterud, Elisabeth Stenholm, Univalent material set theory (arXiv:2312.13024)

    Anonymouse

    diff, v26, current