Not signed in (Sign In)

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

Discussion Tag Cloud

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

nLab > Latest Changes: axiom of extensionality

Bottom of Page

1 to 11 of 11

  1.  
    • CommentRowNumber1.
    • CommentAuthorzskoda
    • CommentTimeNov 8th 2021
    • (edited Nov 8th 2021)

    I do not quite understand the discussion under the axiom of extensionality. It says that one can do two variants (of course), one is that equality is taken as a primitive (predicate) and another that the axiom is taken as a definition of equality. Of course, this is in the idea so, but then the second version of the axiom is written unclear (and it is not quite a definition) and the discussion is also unclear. I see it this way: there is a propositional calculus and there is a propositional calculus with equality. “The same” is probably here just an informal way to refer to the equality of the propositional calculus with equality, that means a distinguished binary predicate which satisfies substitution axiom, transitivity, reflexivity and symmetry. In that calculus we just state the axiom (not a definition) that the equality can be rephrased via belongness relation. If we work in just a propositional calculus then we can define a relation which we may call equality but we can also call it blablabla. Then we have to state explicitly which properties, possibly weaker than required in the propositional calculus with equality hold for that relation (I am not quite sure how entry extensional relation solves this, in particular, should we now prove the substitution axiom for equality). Now, one should do that version precisely. In calculus with equality there is no space for two versions as far as I see: equality is given (distinguished) by the propositional calculus with equality, we can only characterize it.

  2. Adding links to function extensionality and univalence

    Anonymous

    diff, v4, current

  3. adding link to product extensionality

    Anonymous

    diff, v5, current

  4. added statement of axiom of extensionality without the axiom of foundation.

    Anonymous

    diff, v8, current

    • CommentRowNumber5.
    • CommentAuthorNikolajK
    • CommentTimeOct 21st 2022

    When postulating weak and not the conventional extensionality, how far does epsilon-induction (instead of regularity/foundation) take you in defining equality?

  6. adding some references to the page

    Anonymous

    diff, v11, current

  7. The converse always holds because of the indiscernability of identicals

    Anonymous

    diff, v12, current

  8. Fixed spelling error

    Anonymous

    diff, v12, current

    • CommentRowNumber9.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 22nd 2022

    Clarifying parentheses in the definitions of set(a)\mathrm{set}(a) and element(a)\mathrm{element}(a).

    diff, v13, current

  10. Added 2 additional definitions of set in fully formal ETCS

    Anonymous

    diff, v14, current

  11. added section on the axiom of extensionality in two-sorted set theories

    Anonymous

    diff, v15, current

1 to 11 of 11

  1.