## Not signed in

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

## Discussion Tag Cloud

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

• 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)\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!

• 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 24th 2021

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

• CommentRowNumber4.
• CommentAuthorYimingXu
• CommentTimeDec 30th 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 $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.

• CommentRowNumber5.
• CommentAuthorMike Shulman
• CommentTimeJan 1st 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 2nd 2022
• (edited Jan 3rd 2022)

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

• 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 $\mathbb{N}\times An$ to $A$ 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:

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

• CommentRowNumber9.
• CommentAuthorMike Shulman
• CommentTimeJan 4th 2022

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

• 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 $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!

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

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?

• CommentRowNumber12.
• CommentAuthorTobyBartels
• CommentTimeJan 6th 2022

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.

• 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)]$. 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!

• 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

Re: