内附集合论

内附集合论是一个用于建立 Gödel 不完备性定理的弱集合论.

1定义

有三种定义内附集合论的方案.

定义 1.1 (仅用集合论语言的内附集合论). 我们称一阶集合论语言 ${\mathcal{L}}_{\in }=\{\in \}$ 中以下两语句构成的理论为内附集合论 $\mathsf{AD}$:

•	空集公理: $\exists x\forall y(y\notin x)$
•	内附公理: $\forall x\forall y\exists z\forall w(w\in z\leftrightarrow (w\in x\vee w=y))$

定义 1.2 (外延的内附集合论). 我们称一阶集合论语言 ${\mathcal{L}}_{\in }=\{\in \}$ 中向 $\mathsf{AD}$ 中加入以下外延公理形成的理论为外延内附集合论 ${\mathsf{AD}}^{ext}$: $\forall x\forall y(\forall z(z\in y\leftrightarrow z\in x)\to y=x)$

定义 1.3 (函数语言式的内附集合论). 我们考虑语言 ${\mathcal{L}}_{\mathsf{AD}}=\{\varnothing ,[-;-]\}$, 其中有常元符号 $\varnothing$ 与二元函数符号 $[-;-]$. 我们称此语言中以下语句构成的理论为函数式内附集合论 ${\mathsf{AD}}^{fun}$:

•	空集公理: $\forall x([\varnothing ;x]\ne x)$
•	内附公理: $\forall x\forall y\forall w([[x;y];w]=[x;y]\leftrightarrow ([x;w]=x\vee w=y))$

定理 1.4. $\mathsf{AD}$ 与 ${\mathsf{AD}}^{ext}$ 与 ${\mathsf{AD}}^{fun}$ 相互解释.

证明. 先用 $\mathsf{AD}$ 解释 ${\mathsf{AD}}^{ext}$. 我们定义 $x\simeq y$ 为 $\forall z(z\in x\leftrightarrow z\in y)$, 不难验证 ${\mathsf{AD}}^{ext}$ 将等于解释为这个 $\simeq$ 后即翻译入 $\mathsf{AD}$. 用 ${\mathsf{AD}}^{ext}$ 解释 ${\mathsf{AD}}^{fun}$ 只需将 $\varnothing$ 解释为由空集公理和外延公理共同确定的那个集合, 将 $[x;y]$ 解释为由内附公理和外延公理共同确定的那个集合. 最后用 ${\mathsf{AD}}^{fun}$ 解释 $\mathsf{AD}$, 只需在 ${\mathcal{L}}_{\mathsf{AD}}$ 中定义二元谓词符号 $x\in y\leftrightarrow [x;y]=x$.

$\square$

2与不完备性定理的联系

我们知道, Robinson 算术即允许证明有两大 Gödel 不完备性定理, 因此我们只需建立以下定理.

定理 2.1. ${\mathsf{AD}}^{ext}$ 与 $\mathsf{Q}$ 相互解释.

证明.

$\square$

这顺带指出, 在 $\mathsf{ZF}$ 公理中用内附公理取代对集公理或许是更自然的处理.

术语翻译

内附集合论 • 英文 Adjunctive set theory