powerset.cppm File Reference

The power set \(\mathfrak{P}(S)\) as a filtered universe over a reified subobject domain Sub(C) (#830). More...

#include <concepts>
import dedekind.order:inclusion;
import dedekind.sets;
import dedekind.category;

Include dependency graph for powerset.cppm:

Classes
struct	dedekind::order::Sub< C, L >
	Sub(C) for an ordered carrier: a subobject reified as a runtime interval value. Bounds are C values with ±∞ (unbounded) flags and an empty flag; the convex families coerce in via the converting constructors below (which also are the 𝔓 gate — no constructor ⇒ no Sub(C)). Folds onto SetExpr (so it is itself a first-class IsSubobject / IsSet) and is std::regular, so Set<Sub,…> is an IsSet and Sub values are usable in generic set APIs. More...
struct	dedekind::order::SubsetOf< C, L >
	The membership predicate of 𝔓(S): \(X \mapsto X \subseteq S\), with S coerced to Sub(C). A named functor (no lambda). More...

Concepts
concept	dedekind::order::SubReifiable
	A base that reifies as an ordered-carrier subobject Sub(C): it is SetShaped, its carrier is totally ordered (the enabler — so the gate itself, not a later membership call, rejects an unordered carrier), and it coerces to Sub via one of the converting constructors above. The single gate concept for both power_set and 𝔓 (DRY), and — because it conjoins the very SetShaped atom the :sets default is constrained on — it subsumes that deleted gate, so it wins by partial ordering for the ordered families.

Functions
template<SubReifiable S>
constexpr auto	dedekind::order::power_set (const S &base)
	\(\mathfrak{P}(S) = \mathbb{A}\langle\mathrm{Sub}(C)\rangle \mid (X \mapsto X \subseteq S)\) — a bona-fide Set over Sub(C). Gated on S coercing to Sub(C): an unordered / general base is ill-formed.
template<typename C, typename L, typename Card> requires IsTotallyOrdered<C>
constexpr auto	dedekind::order::power_set (const dedekind::sets::𝔸< C, L, Card > &)
	\(\mathfrak{P}(\mathbb{A}) = \mathbb{A}\langle\mathrm{Sub}(C)\rangle\) — the universe of ALL (decidable convex) subobjects, as the universal boundary type, not a trivially-true filtered Set. A more-specialised overload than the generic power_set above, so it wins by partial ordering; keeping the 𝔸 type (rather than Set<Sub,…,SubsetOf>) preserves the boundary / cardinality metadata and the lattice identities 𝔸|X=𝔸 / 𝔸&X=X on 𝔓(𝔸). (Sibling of the :sets closed form \(\mathfrak{P}(\emptyset)=\{\emptyset\}=\mathbb{A}\langle\varnothing\rangle\).)
template<SubReifiable S>
constexpr auto	dedekind::order::𝔓 (const S &base)
	Textbook fraktur-P alias for power_set (blackboard 𝔓). Forwards to power_set, so the 𝔸 closed form above is selected for a universe base and the filtered form for a proper ordered base.

Detailed Description

The power set \(\mathfrak{P}(S)\) as a filtered universe over a reified subobject domain Sub(C) (#830).

@partition :powerset

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.

In the grammar's own vocabulary (empty / universe / filtered base),

\[ \mathfrak{P}(S) \;\equiv\; \mathbb{A}\langle \mathrm{Sub}(C)\rangle \,\mid\, (X \mapsto X \subseteq S), \]

an ordinary Set over the subobject domain Sub(C). So 𝔓(S) is a bona-fide IsSet and inherits the lattice laws (&Ø=Ø, |𝔸=𝔸) and setexpr participation — meet / join / filter as any Set — from the set machinery, with no bespoke carrier. (This is not self-composition: 𝔓(𝔓(S)) is not decidable-convex — \(\downarrow\!S\), the principal ideal \(\{X : X \subseteq S\}\), is a down-set in Sub(C), not a convex Sub value — so nested 𝔓 correctly meets the honest wall, like any non-convex base.)

Sub(C) is the gated part (the exists / forall pattern: an algebraic default lifted by decidable specialisations). Over an ordered carrier the decidable convex subobjects — Ø, 𝔸, Singleton, Halfspace, Interval — all collapse to ONE std::regular type, a runtime Sub; membership \(X \subseteq S\) is then a homogeneous interval nesting (no family variant, no double dispatch), reusing the #835 endpoint comparison. A base with no coercion to Sub (a general / unordered set) has no Sub(C) — 𝔓 is then ill-formed (type-check failure by default), the honest wall.

Home

The enabler here is an ordered carrier, not intervals: Sub becomes a decidable std::regular normal form precisely because C is totally ordered, and membership \(X \subseteq S\) is the subset order (:inclusion). So the home is order, where that order lives. Sub is the order-level normal form of a convex subset — it coerces in the :sets boundaries (Ø / 𝔸) and the value-carrying order shapes (Singleton / Halfspace / Interval), reading their pivots as its two bounds — and it has no topology dependency; being upstream, it reaches every downstream layer (topology's readers included).

@build_order (order layer) @dependency :category, :sets, :total, :halfspace, :inclusion

Wikipedia: Power set, Subobject, Interval (mathematics)

Note

"A set is a Many that allows itself to be thought of as a One." — Georg Cantor (letter to Dedekind, 1899). \(\mathfrak{P}(S)\) reifies "the subobjects of @c S" as one Set, over one carrier.

See also

#308 undergraduate probability and statistics (work in progress): measures and σ-algebras over Sub.