|
本文来自ncatlab词条：inhabited set
什么是有元素的集合？
概念
一个集合或类型如果包含一个元素或术语，则称为有元素。
定义
在集合论中
在集合论中，一个有元素的集合是一个包含元素的集合，即一个集合 X 使得 ∃x, x ∈ X 是真 的。
至少在假设经典逻辑的情况下，这与一个非空的集合是相同的。通常有元素的集合被简单地称为“非空”，但积极的词“有元素”提醒我们，有元素是更简单的概念，而空集是其否定的定义。
“有元素”一词来自构造数学。在构造数学中（如某些拓扑斯的内部逻辑或一般的类型论中），一个非空的集合/类型不一定是有元素的。这是因为在直觉主义逻辑中，双重否定是非平凡的。同样，许多构造数学家使用旧词“非空”，理解为它实际上意味着有元素，并写作
A ≠ ∅ 表示 A 是有元素的。如果我们将 ≠ 保留用于否定不等式，那么我们可以写作 # 表示这种更强的不等式（尽管它不是一个分离关系），因此
A#∅ 表示 A 是有元素的。
在类型论中
在类型论中，有两种可能的有元素类型的概念：一个类型
X 其命题截断
‖X‖ 有一个元素（或术语），或一个类型 X 本身有一个元素（或术语）。前者对应于集合论中的有元素概念，因为
‖X‖ 是 ∃x : X 的命题即类型解释。后者更像是带点集合的概念。
断言 ∀X, (‖X‖ → X)
是一个温和的非构造性逻辑原则，称为命题选择公理。它从排中律中得出，但在某些拓扑斯的内部逻辑中，它可能会失败，因此这两种“有元素类型”的概念确实是不同的。
有元素对象
一个有元素的集合是拓扑斯Set中的一个内部有元素对象的特例。这两种有元素类型的概念对应于内部和外部有元素对象（分别是那些
X → 1 是一个满射的对象，以及那些允许一个全局元素 1 → X 的对象）。
相关概念
在抽象石双性中，“有元素”和“占据空间”空间之间存在区别（这可能对应于地方的某些内容，应在此解释）。
相关概念
| 
