NuPRL 中的证明 7

这一篇开头讲一点 constructive real analysis。

Intuitionistic mathematics 中，实数用一个不断提高近似精度的无穷序列(Cauchy Sequence) 定义。

即

$\mathbb{R} =_{\it def} \{q:\mathbb{N}^+\rightarrow \mathbb{Q}\;|\; \forall n,m:\mathbb{N}^+ .|q_n-q_m|\leq n^{-1}+m^{-1} \}$

这样的无穷的序列就是 free choice sequence 中的一种，表现出来是个 $\mathbb{N}^+ \rightarrow \alpha$ 的 function type。在这里 $\alpha \simeq \mathbb{N}$ ，即和自然数一一对应，众所周知地，有理数滿足这一性质。¹

显然地，引入 choice sequence 的概念时，choice sequence 可以分成三种。

一种为 lawlike，即可以用某个 algorithm 表示的。

第二种为 lawless，是完全无序的。

第三种是由前两种 choice sequence 混合得到的，是为 mix。

注意即使是 lawless sequence，也符合 function 的性质，即 $\forall a. f(a) = f(a)$ ，也就是已经生成的数是不会变更了。

尽管 choice sequence 是无限的，但明显地，任何有限的 sequence 同时是无限个 choice sequence 的初始部分。

Brouwer 提出可以用 spread 表示 choice sequence 的集合。如，对于所有限定元素为 $\{0,1\}$ 的 choice sequence (binary sequence) 的集合(Cantor Space)，可以用 binary tree 表示。initial segment 就可以用 spread 里的一条 path 来表示。这里对于一个 choice sequence $\alpha$ 用 $\overline{\alpha}n$ 表示其长为 $n$ 的 initial segment²

Continuity of Number³

对于任何 choice sequence 的特性都可以从其有限的 Initial segment 决定。比如，不可能数出某个数在 choice sequence 中出现的次数。因此，任意接受 choice sequence 的函数都只依靠有限的 initial segment。于是可以写成 continuity of number 如下

$\forall f :\mathbb{S}\rightarrow \mathbb{N}.\forall \alpha:\mathbb{S}.\exists n: \mathbb{N} . \forall \beta : \mathbb{S}.(\overline{\alpha}n=\overline{\beta}n) \Rightarrow f(\alpha)=f(\beta)$

然而上面的 continuity principle 可以证明在 constructive type theory 里是错的。

因为在 constructive type theory 中，以上 proposition 的证明如果存在，则有一个 algorithm $M:(\mathbb{S}\rightarrow \mathbb{N})\rightarrow \mathbb{N}$ 使得 $\forall f. \forall \alpha,\beta. (\forall n. n < M(f) \Rightarrow \overline {\alpha}n=\overline{\beta}n)\Rightarrow f(\alpha) = f(\beta))$ ，然而用证明 program termination is undecidable 类似的思路，可以用在 f 是一个含有 M 的函数的例子证明这样的 M 不存在。

Squash & Half Squash

在 LdBeth：NuPRL 中的证明{x:N|2<x<3}–virtual evidence 中介绍了 squash type， $\forall x:\,\downarrow\! P.x= Ax \in\, \downarrow\! P$ ，这里在 NuPRL 中证明 continuity of number 的 weaken form 用到了比 squash 弱化的 half squash, or extensional squash， $\downharpoonleft\!P = P//True$ ，由 quotient type 定义， $\forall x,y:\,\downharpoonleft\!P.x=y\in\,\downharpoonleft\!P$

$\forall f :\mathbb{S}\rightarrow \mathbb{N}.\downharpoonleft\!\forall \alpha:\mathbb{S}.\exists n: \mathbb{N} . \forall \beta : \mathbb{S}.(\overline{\alpha}n=\overline{\beta}n) \Rightarrow f(\alpha)=f(\beta)$

这样可以用 named exception 实现一个非 extensional 的 M 来得出 n。half squash 在保留了 M 的 computational content 的同时，确保了 M 不能用来 construct 新的带有 computational content 的 term，从而保证了 half squash 后的 proof term 不能用来 self apply 以构造出 M is not consistent 的证明。把 half squash $\downharpoonleft$ 換成 full squash $\downarrow$ 也是可证的，而且只要能通过 meta theory 求得 n 即可而无需 constructively 给出 M。

参考