学习 Hurkens' Paradox (Pt.1)

前几天和群友一起学习了一下 Type-in-type 可能导致的问题。作为一个能够勉强背诵 ZFC 公理的工科🐖，感觉 Girard’s paradox 的构造十分神奇，遂做学习笔记，尝试在 Lean 上实现。事实上，接下来讨论的主要都是 Hurkens 的 Girard’s paradox 简化版本。 Girard’s paradox 是 Burali-Forti paradox 在类型论中的编码，本文先主要处理较为朴素的编码（Hurkens95 的第五节），后续如果我还能写的出来的话，会继续跟进这一个编码的简化，以及如何应用到 Type-in-type 的系统内，例如如果 Coq 或者 Lean 加入一些非直谓宇宙公理之后导出的矛盾。

Burali-Forti Paradox

Burali-Forti paradox 简单来说就是“全体序数不构成集合”：

如果全体序数构成一个集合 $Ord = \{ x | x \text{ well-ordered and transitive} \}$ ，那么可以检查 $Ord$ 本身 WO & transitive, s.t. $Ord \in Ord$ ，那么 $\{ Ord \}$ 是 $Ord$ 无最小元的子集，矛盾。

如果把传统 von Neumann 序数直接翻译到 Lean 里，那么如果想不遍地用排中律，定义其实非常麻烦，有很多小细节需要考虑。尤其是“全序”，传统的定义方式是 $a < b \lor b < a \lor a = b$ ，不排中的话非常倒闭。

Hurkens’ paradoxical universe

Hurkens 用了一个比较聪明的方法刻画了序数的概念，或者说序数里我们比较关心的属性： $\epsilon$ -well-foundedness

定义: 如果存在一个集合 $x$ 满足 $\forall y, (\forall z \in y, z \in x) \to z \in x$ ，称 $x$ 为 Inductive set

可以把 $x$ 理解为描述了一个 “ $\epsilon$ -超穷归纳可证的性质”。那么一个 Well-founded set 就是满足所有 $\epsilon$ -归纳可证属性的集合。

定义: 如果存在一个集合 $x$ 满足 $\forall y, (y \text{ inductive}) \to x \in y$ ，称 $x$ 为 Well-founded set

注意这里某个特定的 Inductive set $x$ 里面可能有一些妙妙不 Well-founded 的元素：毕竟我们没有加入正则性公理对 $\epsilon$ 关系加入限制。不过如果定义 $\Omega = \{ x | x \text{ well-founded} \}$ ，那么它一定是最小的 Inductive set。这个很像从无穷公理得到 $\omega$ 集合的过程：Informally， $\omega$ 是所有验证无穷公理的集合的交 = 最小的验证无穷公理的集合 = 由 $0$ 和 $S$ 自由生成出来的集合。

Hurkens 随后在类型论中将以下两个常量解读为序数上的操作：如果有 Universe U，解读 τ : (U -> Prop) -> Prop 和 σ : U -> (U -> Prop)。

对于前者，将 T : U 全部解读为序数，那么 P : U -> Prop 可以被解读为一个序数 subclass。如果它变成了一个集合的话，我们可以考虑 P 上的 $\epsilon$ -序型 [1]，得到序型的过程是一个 (U -> Prop) -> U 的映射。
对应地，后者解读为“前驱”，即 σ x 是所有小于 x 的序数构成的子集。

根据这个解读，存在以下性质：

axiom paradoxical : forall (p : U -> Prop) (x : U), σ (τ p) x <-> exists y, p y ∧ τ (σ y) = x

如果上述两个常量和性质存在，据此可以后续推出矛盾。

喵喵的解读

不过我个人其实没太看懂这个解读。这里有两个不太 Make sense 的地方：

首先根据最终构造的矛盾，不是所有东西都是序数，否则其实只有一个 Inductive set。甚至因为不存在正则性， $\epsilon$ 关系其实都不太 Well-founded，对任意集合谈论序型其实就比较怪。
论文中提了一嘴，但是确实对于一个序数 x，有 τ (σ x) = x：因为在 von Neumann 序数的序型是自身，然后前驱关系就是 $\epsilon$ 。据此，上述 paradoxical 性质就变成了 σ (τ p) = p（考虑外延性）。这说明 p 不能只是任意序数子集，而只能也就是一个序数。

所以感觉符合上述那个解读的模型估计论域里真的就只有序数。我个人的解读如下：

Universe U 里面都是集合。
把 σ 直接当成 $\epsilon$ 。
τ 其实说的是 Unrestricted comprehension，读作“把满足特定属性的集合收集成一个集合”。

这种解读下恢复出来了上述 σ (τ p) = p 以及 τ (σ x) = x 的性质。In some sense，集合本身刻画的就是属于关系，所以 U 和 U -> Prop 除了大小问题以外在集合论内确实就是同样的概念。在下面的构造中先使用 σ (τ p) = p 得到矛盾，后续文章中再放松至论文原先的条件。

在这种解读下哪里出了问题就比较明显了：Unrestricted comprehension。对应地，在这种脱离了序数的解读下，Hurkens 的构造变得更像传统的 Burali-Forti paradox 的陈述。

构造

重点是考虑 $P(x) = x \not \in x$ ，这一性质是 $\epsilon$ -归纳可证的，因此对所有具有正则性的集合都满足，特别是 Well-founded 的集合。然而如果通过 Unrestricted comprehension 收集所有 Well-founded 集合 $\Omega$ ，那么 $\Omega$ 本身也 Well-founded，因此 $\Omega \in \Omega$ ，因此矛盾。

class Paradoxical.{u} (U : Type u) where
  σ : U -> (U -> Prop)
  τ : (U -> Prop) -> U
  paradoxical {u} {pu : U -> Prop} : (σ (τ pu)) u ↔ pu u

notation a "ε" b => Paradoxical.σ b a

def Paradoxical.bad {U} [Paradoxical U] : False := by {
  let Inductive (x : U) := forall y, (forall z, (z ε y) -> (z ε x)) -> (y ε x)
  let WellFounded (x : U) := forall y, Inductive y -> x ε y
  let Ω : U := Paradoxical.τ (fun x => WellFounded x)

  have Ω_wf : WellFounded Ω := by {
    intros x h
    apply h
    intros z hz
    rw [Paradoxical.paradoxical] at hz
    exact hz x h
  }

  have Ω_in_self: Ω ε Ω := by {
    rw [Paradoxical.paradoxical]
    exact Ω_wf
  }

  have lemma : Inductive (Paradoxical.τ (fun x => ¬ (x ε x))) := by {
    intros y h
    rw [Paradoxical.paradoxical]
    intros hyiny
    have h' := h y hyiny
    rw [Paradoxical.paradoxical] at h'
    exact h' hyiny
  }

  have Ω_not_in_self : ¬ (Ω ε Ω) := by {
    have h := Ω_wf _ lemma
    rw [Paradoxical.paradoxical] at h
    assumption
  }

  exact Ω_not_in_self Ω_in_self
}

那么在原先的解读下问题在哪里呢？

在原先的解读下，τ 的含义是序数 Subclass 到序型。这里最大的问题就是不是所有序数 Subclass 都能得到一个序数作为序型，典型例子就是 Ord class 本身。

[1] 其实不是集合的话也可以，见 Mostowski collapse，结果如果是 proper class 那么一定是 Ord 本身。