nLab powerset structure

Contents

Definition

Given a set VV with an extensional relation \prec, a proto-powerset structure is a function 𝒫:VV\mathcal{P}:V \to V such that

  • for all elements bVb \in V, and cVc \in V, if for all elmemets aVa \in V, aba \prec b implies aca \prec c, then b𝒫(c)b \prec \mathcal{P}(c).

A powerset structure is a function 𝒫:VV\mathcal{P}:V \to V such that

  • for all elements bVb \in V, and cVc \in V, b𝒫(c)b \prec \mathcal{P}(c) if and only if for all elements aVa \in V, aba \prec b implies aca \prec c.

Uniqueness of 𝒫(c)\mathcal{P}(c) follows from \prec being an extensional relation.

Foundational concerns

In any material set theory, instead of postulating the mere existence of a set 𝒫\mathcal{P} in which for all sets bb, if for all sets aa, aba \in b implies aca \in c, then b𝒫b \in \mathcal{P}, one could add a primitive unary operation 𝒫(c)\mathcal{P}(c) which takes material sets cc and returns a material set 𝒫(c)\mathcal{P}(c) such that for all bb, if for all aa, aba \in b implies aca \in c, then b𝒫(c)b \in \mathcal{P}(c).

See also

Last revised on December 12, 2022 at 18:06:31. See the history of this page for a list of all contributions to it.