Definition
In the philosophy of mathematics, Atomism is the stance that a mathematical object is a composite of distinct, self-contained, and complete individual units (“atoms”).
Two Interpretations
We distinguish between the philosophical view and its specific type-theoretic formalization.
1. Classical/Philosophical Atomism
The view that the continuum (and other structures) is a “dust” of pre-existing points.
- Ontology: The whole is secondary to the parts.
- Equality: Elements are strictly separable ().
- Implication: This implies Discrete (decidable equality).
2. Structural Atomism (HoTT)
The view that a type has no higher-dimensional path structure.
- Formalization: A type is an h-set (0-type).
- Crucial Distinction: In constructive mathematics, structural atomism (being a set) does not imply computational discreteness (decidable equality). The Real Numbers are structurally atomistic (paths are unique) but not discrete.