Not signed in (Sign In)

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

  • Sign in using OpenID

Site Tag Cloud

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 deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor galois-theory 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 homology homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory itex 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 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 science set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

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

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
  1. starting discussion page

    Anonymous

    diff, v8, current

    • 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:Aa:A. However, there are two different presentations of dependent type theory used in the community. One presentation includes a separate type judgment AtypeA \; \mathrm{type} in addition to the typing judgment a:Aa: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 iU_i such that U i:U i+1U_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 11 for the identity morphism of the terminal object, elements are represented by morphisms with source 11, and sets are represented by morphisms with target 11. We then define the global membership symbol aAa \in A as

    aA(t(A)=1)(s(a)=1)(s(A)=t(a))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 AA such that there exists elements/sets xx and yy such that xAx \in A and AyA \in y.
  2. added section on fully formal ETCS

    Anonymous

    diff, v9, current

    • 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 xx and yy such that xyx \sim y, the following conditions hold:

    • for all morphisms aa such that axa \in x, there exists a morphism bb such that byb \in y and aba \sim b
    • for all morphisms bb such that byb \in y, there exists a morphism aa such that axa \in x and aba \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 fxf \circ x and gxg \circ x only exist if ff and gg have the same source, which is the target of xx. If xx has source the terminal object 11 and If the target of both ff and gg is also 11, then the composite fxf \circ x and gxg \circ x is the identity morphism on 11, and so fxf \circ x and gxg \circ x are always the same. Furthermore, if the target of ff and gg is 11, and the source of ff and gg is the same, then ff and gg 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 11.

    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 aAa \in A if aa is meant to be an element of the set AA.

    • CommentRowNumber15.
    • CommentAuthorGuest
    • CommentTimeOct 21st 2022

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

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

    In ZFC, isSet(a)\mathrm{isSet}(a) and isElem(a)\mathrm{isElem}(a) are both \top for all objects aa, so the statements are trivially true by the principle of explosion. But in fully formal ETCS, there are nontrivial objects ff where both isSet(f)\mathrm{isSet}(f) and isElem(f)\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 ab:=a=ba \sim b := a = b, and in addition, id 2swap\mathrm{id}_2 \sim \mathrm{swap} and swapid 2\mathrm{swap} \sim \mathrm{id}_2 for the identity function and the swap function on the set with two elements 22, is a bisimulation on \in, but it is not true that id 2=swap\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 SetSet and probable elements ElEl, one could define a global membership predicate Γ,x:El,A:Setprop\Gamma, x:El, A:Set \vdash \in \; \mathrm{prop} where xAx \in A if and only if set(A)\mathrm{set}(A) and in A(x)\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.
    • CommentAuthorMadeleine Birchfield
    • 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

    diff, v10, current

    • 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

    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

  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

    diff, v12, current

    • 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 11, 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

    A:Ob() B:Ob()Hom(A,B)\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 aa and bb in a unsorted set theory, if set(a)\mathrm{set}(a) and set(b)\mathrm{set}(b), then ¬(ab)\neg (a \in b). The definition of set(a)\mathrm{set}(a) as s(a)=0s(a) = 0, where 00 is the identity function on the empty set, means that the membership relation aba \in b is defined as s(a)=1s(a) = 1 and s(b)=0s(b) = 0 and t(a)=t(b)t(a) = t(b), where 11 is the identity function on the singleton. The only time that aba \in b when aa is a set is in the trivial theory where 0=10 = 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 SS 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

    diff, v14, current

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

    Anonymous

    diff, v14, current

    • 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 PAPA. 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×PAΩA \times PA \to \Omega.

  8. three -> many

    Anonymous

    diff, v14, current

  9. material moved to unsorted set theory

    Anonymous

    diff, v14, current

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

    Anonymous

    diff, v14, current

    • 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 AsetA \; \mathrm{set} instead of AtypeA \; \mathrm{type} and the typing judgments as aAa \in A instead of a:Aa:A, and include an term reflection rule which turns every term into a type/set

    ΓAsetΓaAΓaset\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.

  11. added context sidebar

    Anonymous

    diff, v18, current

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

    Anonymous

    diff, v18, current

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

    diff, v23, current

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)