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).
    • CommentRowNumber1.
    • CommentAuthorYimingXu
    • CommentTimeDec 23rd 2021
    • (edited Dec 23rd 2021)

    Hi, all.

    I would like to understand hoe does SEAR Axiom 5 works, that is Axiom of collection in SEAR.There is a section on “Application of Collection” and a sentence “(more detail to be added here…)”. My question is basically “what is intended to be there” in short.

    According to my current understanding the example in this incomplete section, which aims to construct the ghost of {P n(N)nN}\{P^n(N)\mid n\in N\} should work as follows: we have a predicate taking a natural number nn and a set PnPn, such predicate holds if PnP n(N)Pn \cong P^n(N) (here \cong means bijection, cannot use equality here because the nlab page claims that there is no equality between sets.). And by axiom 5, we have a set BB, a function p:BNp:B\to N. and a BB-indexed family of sets M:BYM:B\looparrowright Y such that for any bBb\in B, M bP p(b)(N)M_b \cong P^{p(b)}( N) and for any nNn\in N, there exists a member ofbb which is mapped to nn. (because P n(N)P^n(N) exists for every nn).

    Does this sound correct?

    If so, then it seems to me that the application of Axiom 5 only gives YY contains nNP n(N)\coprod_{n\in N}P^n(N). As the nlab page claims that the collection axioms plays a similar role as replacement. How can I demonstrate that the thing I have obtained here is useful enough to be an analogue of the set {P n(N)nN}\{P^n( N)\mid n\in N\} as in ZF?

    Other examples on SEAR Axiom 5 would also be nice! Thank you!

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeDec 23rd 2021

    I don’t have time to write anything out now, but maybe you can get some of the idea from section 7 of Comparing material and structural set theories. That’s written using ETCS-like language, but it’s fairly straightforward to translate back and forth to SEAR-style.

    • CommentRowNumber3.
    • CommentAuthorYimingXu
    • CommentTimeDec 25th 2021

    Many thanks! The reference looks nice and I will try to read that!

    • CommentRowNumber4.
    • CommentAuthorYimingXu
    • CommentTimeDec 31st 2021
    • (edited Dec 31st 2021)

    Another question is that how would we define the relation between a natural number and a set? The axioms says “For any set AA and any property PP”, say the property is, in informal language: “nn is related to AnAn iff AnAn is the nn-copy product of AA”, 11 is related to AA, 22 is related to A×AA \times A, 33 is related to A×A×AA \times A\times A… and so on. How can we define such a property in the formal language of SEAR? The point of confusion is that we can only define property by induction on N for elements of the same set, but before we construct the set of all A nA^n’s, we do not have such a set that contains all of the A nA^n as members.

    • CommentRowNumber5.
    • CommentAuthorMike Shulman
    • CommentTimeJan 2nd 2022

    The “properties” referred to in the comprehension and collection axiom schemata of SEAR are those specified by a first-order formula, just as in the ZFC axiom schemata of replacement, collection, and separation. The property you mention can be specified directly by a first-order formula, without using any induction.

    • CommentRowNumber6.
    • CommentAuthorYimingXu
    • CommentTimeJan 3rd 2022
    • (edited Jan 3rd 2022)

    Thanks for replying!

    Yes, it is a first-order formula, but I do not think it can be defined “directly”. If I am asked to define it, in formal language, my approach will be proving the existence of list object first, and state such property as:

    Ann.P(n,An)projsList(A An).Length(projs)=nandXlList(A X).Length(l)=n!f:XAn.n0.n0nEL(n0,projs)¯f=El(n0,l)¯\forall An\forall n.P(n,An) \Leftrightarrow \exists projs\in List(A^{An}). Length (projs) = n \and \forall X\forall l\in List(A^X). Length(l) = n \implies \exists ! f:X\to An. \forall n0. n0 \le n \implies \overline{EL(n0,projs)} \circ f = \overline{El(n0,l)}

    I believe this can serve the definition of nn-ary product but need list object first, since we cannot use induction. Here EL(n,l)EL(n,l) is the nn-th item of the list ll., and f¯\overline{f} is the exponential transpose.

    Is there any better way to define the PP? I am also a bit worrying because the same approach does not apply when we define P n(A)P^n(A).

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeJan 3rd 2022

    That looks fine to me. You should be able to do without list objects by saying the projections are a relation from ×An\mathbb{N}\times An to AA with certain properties.

    • CommentRowNumber8.
    • CommentAuthorYimingXu
    • CommentTimeJan 4th 2022
    • (edited Jan 4th 2022)

    Thank you for feedback again!

    I am sorry that I still have trouble defining “being the nth power” of some set, as claimed on the nlab page.

    I think if I can define “being a power set of”, that is, I have

    isPow(PA,A) iff PA is a power set of A. Then the nth power can be defined as:

    n.nPow(Pn,A)l.Length(l)=nandn0.n0<nisPow(El(n0,l),El(n0+1))andHD(l)PnandEl(n,l)A\forall n. nPow(Pn,A) \Leftrightarrow \exists l. Length(l) = n \and \forall n0. n0 \lt n\implies isPow(El(n0,l),El(n0+1)) \and HD(l)\cong Pn \and El(n,l)\cong A

    (The “and”s above are logical conjunctions.)

    And the notion of isPow is not obvious for me. Since for it to be usable, we need AA and P(A)P(A) to be elements of a same set (since items of a list can only be members of a same set). How can we do this? Or are there any other suggested approach?

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeJan 5th 2022

    You can make a conjunction symbol \wedge with \wedge.

    I don’t understand why you say “we need AA and P(A)P(A) to be elements of the same set”. In the collection axiom the property is a relation between an element of a set (such as an element of \mathbb{N}) and a set, not an element of a set. I would define the relation “BB is the nn-fold power set of AA” between the element nn\in\mathbb{N} and the set BB to say that there exists an \mathbb{N}-indexed family of sets CC, isomorphisms C 0AC_0 \cong A and C nBC_n \cong B, and such that for all k<nk\lt n, C k+1C_{k+1} is the power set of C kC_k.

    • CommentRowNumber10.
    • CommentAuthorYimingXu
    • CommentTimeJan 5th 2022
    • (edited Jan 5th 2022)

    I did noticed that the input of collection is a member of a set and a set. Sorry that I did not state my intended meaning clearly! By “need AA and P(A)P(A) to be elements of the same set”, I intended to say that we need both P(A)P(A) and AA to be a member of the same set if we want to put them into a same list, and this leads me to trouble. I am not claiming that the relation “isPow” should be between elements of some set.

    I think I understand your definition, this is nice and I believe I am saved from the trouble! Thanks!

    • CommentRowNumber11.
    • CommentAuthorHurkyl
    • CommentTimeJan 5th 2022
    • (edited Jan 5th 2022)

    Incidentally, AA and P(A)P(A) are both subobjects of P(A)P(A) (by identifying elements of AA with singleton subsets of AA), and thus correspond to elements of P(P(A))P(P(A)). Is that sufficient for your purpose?

    • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeJan 6th 2022

    You can define isPow(B,A)isPow(B,A) as an abbreviation for ε:AB,SA,!sB,xA,x ASε(x,s)\exists\, \epsilon\colon A \looparrowright B,\; \forall\, S \subseteq A,\; \exists!\, s \in B,\; \forall\, x \in A,\; x \in_A S \;\leftrightarrow\; \epsilon(x,s), the defining property of powersets in Axiom 3. Note that the there's no need to collect AA and BB into a single set to make sense of this; the list in ‘isPow(B,A)isPow(B,A)’ is metanotation.

    • CommentRowNumber13.
    • CommentAuthorYimingXu
    • CommentTimeJan 7th 2022
    • (edited Jan 7th 2022)

    Re: Incidentally, A and P(A) are both subobjects of P(A) (by identifying elements of A with singleton subsets of A), and thus correspond to elements of P(P(A)). Is that sufficient for your purpose?

    If I still want the list approach, then I will need the n-fold power set to be the last member of [A,P(A),P(P(A)),P(P(P(A))),...,P n(A)] [A,P(A),P(P(A)),P(P(P(A))),...,P^n(A)]. So we need all of the P k(A)P^k(A)’s to be in the same set. It seems to me that the list approach is still hopeless, since we need to organise all the list items neatly into subsets of P n(A)P^n(A). (I have not devoted much time to think about this approach, but I have not discovered an obvious neat way to do it so far. I will share progress if I can use it to make a definition or give an argument that I cannot.)

    If it is clear to you what should the definition of n-fold power set using this definition of power set, I am still curious to see such a definition!

    Re: You can define isPow(B,A) as an abbreviation for ∃ε:A↬B,∀S⊆A,∃!s∈B,∀x∈A,x∈AS↔ε(x,s), the defining property of powersets in Axiom 3. Note that the there’s no need to collect A and B into a single set to make sense of this; the list in ‘isPow(B,A)’ is metanotation.

    Yes, this statement is formal except for the part SA\forall S\subseteq A, but it is easy to replace it with s:1A\forall s:1\to A, so we can quantify over the ss, or make a definition of being a subset. I think this is the thing I use to formalise it. I was trying to collect AA and BB into a single set just because I wanted to use list. By using NN-indexed family, I agree that we can take it as definition of isPow to define n-fold Pow when using Shulman’s definition above.

    Thanks to all of you!

    • CommentRowNumber14.
    • CommentAuthorRodMcGuire
    • CommentTimeJan 7th 2022

    in the nForum the standard way to quote someone is to precede the quoted text with a > character like this