The Dedekind Set Model: Concrete Collections and Set Morphisms. More...

import dedekind.sets:recursion;

Include dependency graph for sets.cppm:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Detailed Description

The Dedekind Set Model: Concrete Collections and Set Morphisms.

sets__Set_Theory

This module provides concrete implementations for the abstract laws defined in dedekind.ontology. While the ontology defines the requirements for a set, this module provides the mechanisms to construct them.

In the Dedekind architecture, set theory bridges logic (Level -1) and magnitude. By implementing monadic and comonadic extensions for specific structures, we enable:

Extensional Sets: Materialized collections (Singleton, Finite Sets).
Intensional Sets: Rule-based definitions (Comprehensions).
Set Morphisms: Automatic lifting of functions (a functor's F(f)) and filters (bind).

sets__The_Comprehension_Syntax

This module enables symbolic set-builder notation: { f | x % S | P } -> The mapping of elements in S satisfying P by f.

See also: dedekind.sets:singleton (The Atomic Point); dedekind.sets:expressions (The Symbolic Calculus)

Wikipedia: Set theory, Axiom of Specification, Naive Set Theory

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

Note: "Das Wesen der Mathematik liegt in ihrer Freiheit." — Georg Cantor, Grundlagen einer allgemeinen Mannigfaltigkeitslehre (1883). [Trans: "The essence of mathematics lies entirely in its freedom."]

Roadmap (work in progress)

#308 undergraduate probability and statistics: probability over sets: measures and σ-algebras over the subobjects, random variables, distributions and expectation; nothing delivered yet.
#274 Probabilistic Set Membership: graded membership exists as L-valued sets over chains (IsLSet, Percentage); still open are real or semiring scores (ScoreSet), Boltzmann weights, entropy, and SoftMeet and SoftJoin with a temperature.