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!

]]>I have created a stub for constructible universe. I did not go through the version of the definition via definability. Now constructible sets are sets in the constructible universe. The notion of course, intentionally reminds the constructible sets in topology and algebaric geometry as exposed e.g. in the books on stratified spaces, on perverse sheaves (MacPherson e.g.) and in Lurie’s Higher Topos Theory. Now I wanted to create constructible set but I was hoping that there is a common definition for all these cases or at least logically defendable unique point of view, rather than partial similarity of definitions. I mean one always have some business of unions, complements etc. starting with some primitive family, say with open sets, or algebraic sets, or open sets relative strata etc. and inductively constructs more. Now, all the operations mentioned seem to have sense in some class of lattices. Maybe in Heyting lattices or at least in Boolean lattices. On the other hand, google spits out several references on *constructible lattices* *one of the authors is certain Janowitz), but the definition there is disappointing. I mean I would like that one has some sort of constructible completion of certain kind of a lattice and talk about the constructible elements as the elements of constructible completion. I am sure that the nLab community could nail the wanted common generalization down or to give a reference if the literature has it already.