Not signed in

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

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorYimingXu
   • CommentTimeDec 23rd 2021
   • (edited Dec 23rd 2021)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexHi, 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)\mid n\in N\}$ should work as follows: we have a predicate taking a natural number $n$ and a set $Pn$, such predicate holds if $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 $B$, a function $p:B\to N$. and a $B$-indexed family of sets $M:B\looparrowright Y$ such that for any $b\in B$, $M_b \cong P^{p(b)}( N)$ and for any $n\in N$, there exists a member of$b$ which is mapped to $n$. (because $P^n(N)$ exists for every $n$). Does this sound correct? If so, then it seems to me that the application of Axiom 5 only gives $Y$ contains $\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)\mid n\in N\}$ as in ZF? Other examples on SEAR Axiom 5 would also be nice! Thank you!

   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)\mid n\in N\}$ should work as follows: we have a predicate taking a natural number $n$ and a set $Pn$, such predicate holds if $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 $B$, a function $p:B\to N$. and a $B$-indexed family of sets $M:B\looparrowright Y$ such that for any $b\in B$, $M_b \cong P^{p(b)}( N)$ and for any $n\in N$, there exists a member of$b$ which is mapped to $n$. (because $P^n(N)$ exists for every $n$).

   Does this sound correct?

   If so, then it seems to me that the application of Axiom 5 only gives $Y$ contains $\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)\mid n\in N\}$ as in ZF?

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

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeDec 23rd 2021
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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](https://arxiv.org/abs/1808.05204v2). That's written using ETCS-like language, but it's fairly straightforward to translate back and forth to SEAR-style.

   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.

3. • CommentRowNumber3.
   • CommentAuthorYimingXu
   • CommentTimeDec 25th 2021
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexMany thanks! The reference looks nice and I will try to read that!

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

4. • CommentRowNumber4.
   • CommentAuthorYimingXu
   • CommentTimeDec 31st 2021
   • (edited Dec 31st 2021)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexAnother question is that how would we define the relation between a natural number and a set? The axioms says "For any set $A$ and any property $P$", say the property is, in informal language: "$n$ is related to $An$ iff $An$ is the $n$-copy product of $A$", $1$ is related to $A$, $2$ is related to $A \times A$, $3$ is related to $A \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^n$'s, we do not have such a set that contains all of the $A^n$ as members.

   Another question is that how would we define the relation between a natural number and a set? The axioms says “For any set $A$ and any property $P$”, say the property is, in informal language: “$n$ is related to $An$ iff $An$ is the $n$-copy product of $A$”, $1$ is related to $A$, $2$ is related to $A \times A$, $3$ is related to $A \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^n$’s, we do not have such a set that contains all of the $A^n$ as members.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeJan 2nd 2022
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThe "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.

   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.

6. • CommentRowNumber6.
   • CommentAuthorYimingXu
   • CommentTimeJan 3rd 2022
   • (edited Jan 3rd 2022)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexThanks 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: $\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 $n$-ary product but need list object first, since we cannot use induction. Here $EL(n,l)$ is the $n$-th item of the list $l$., and $\overline{f}$ is the exponential transpose. Is there any better way to define the $P$? I am also a bit worrying because the same approach does not apply when we define $P^n(A)$.

   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:

   $\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 $n$-ary product but need list object first, since we cannot use induction. Here $EL(n,l)$ is the $n$-th item of the list $l$., and $\overline{f}$ is the exponential transpose.

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

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeJan 3rd 2022
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThat looks fine to me. You should be able to do without list objects by saying the projections are a relation from $\mathbb{N}\times An$ to $A$ with certain properties.

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

8. • CommentRowNumber8.
   • CommentAuthorYimingXu
   • CommentTimeJan 4th 2022
   • (edited Jan 4th 2022)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexThank 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: $\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 $A$ and $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?

   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:

   $\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 $A$ and $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?

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeJan 5th 2022
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexYou can make a conjunction symbol $\wedge$ with `\wedge`. I don't understand why you say "we need $A$ and $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 "$B$ is the $n$-fold power set of $A$" between the element $n\in\mathbb{N}$ and the set $B$ to say that there exists an $\mathbb{N}$-indexed family of sets $C$, isomorphisms $C_0 \cong A$ and $C_n \cong B$, and such that for all $k\lt n$, $C_{k+1}$ is the power set of $C_k$.

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

   I don’t understand why you say “we need $A$ and $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 “$B$ is the $n$-fold power set of $A$” between the element $n\in\mathbb{N}$ and the set $B$ to say that there exists an $\mathbb{N}$-indexed family of sets $C$, isomorphisms $C_0 \cong A$ and $C_n \cong B$, and such that for all $k\lt n$, $C_{k+1}$ is the power set of $C_k$.

10. • CommentRowNumber10.
    • CommentAuthorYimingXu
    • CommentTimeJan 5th 2022
    • (edited Jan 5th 2022)
    • PermaLink
    Author: YimingXu
    Format: MarkdownItexI 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 $A$ and $P(A)$ to be elements of the same set", I intended to say that we need both $P(A)$ and $A$ 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!

    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 $A$ and $P(A)$ to be elements of the same set”, I intended to say that we need both $P(A)$ and $A$ 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!

11. • CommentRowNumber11.
    • CommentAuthorHurkyl
    • CommentTimeJan 5th 2022
    • (edited Jan 5th 2022)
    • PermaLink
    Author: Hurkyl
    Format: MarkdownItexIncidentally, $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?

    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?

12. • CommentRowNumber12.
    • CommentAuthorTobyBartels
    • CommentTimeJan 6th 2022
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexYou can define $isPow(B,A)$ as an abbreviation for $\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 $A$ and $B$ into a single set to make sense of this; the list in ‘$isPow(B,A)$’ is metanotation.

    You can define $isPow(B,A)$ as an abbreviation for $\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 $A$ and $B$ into a single set to make sense of this; the list in ‘$isPow(B,A)$’ is metanotation.

13. • CommentRowNumber13.
    • CommentAuthorYimingXu
    • CommentTimeJan 7th 2022
    • (edited Jan 7th 2022)
    • PermaLink
    Author: YimingXu
    Format: MarkdownItexRe: 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)]$. So we need all of the $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)$. (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 $\forall S\subseteq A$, but it is easy to replace it with $\forall s:1\to A$, so we can quantify over the $s$, or make a definition of being a subset. I think this is the thing I use to formalise it. I was trying to collect $A$ and $B$ into a single set just because I wanted to use list. By using $N$-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!

    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)]$. So we need all of the $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)$. (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 $\forall S\subseteq A$, but it is easy to replace it with $\forall s:1\to A$, so we can quantify over the $s$, or make a definition of being a subset. I think this is the thing I use to formalise it. I was trying to collect $A$ and $B$ into a single set just because I wanted to use list. By using $N$-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!

14. • CommentRowNumber14.
    • CommentAuthorRodMcGuire
    • CommentTimeJan 7th 2022
    • PermaLink
    Author: RodMcGuire
    Format: MarkdownItexin the nForum the standard way to quote someone is to precede the quoted text with a `>` character like this >Re:

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

    Re: