DIAGONAL ARGUMENTS AND CARTESIAN CLOSED CATEGORIES

在一個 cartesian closed category 中，如果 $A \xrightarrow{\phi} B^A$ 是 point-surjective，則所有 $B \xrightarrow{f} B$ 都存在不動點 $1 \xrightarrow{s} B$ （滿足 $f \circ s = s$ ）。

Proof

首先畫出交換圖

其中 $\delta$ 的定義是 $c \mapsto \langle c, c \rangle$ ，所以對 $1 \xrightarrow{p} A$ 來說 $\delta \circ p = \langle p, p \rangle$ 。沿著這個定義，我們知道 $(\phi \times 1_A) \circ \delta \circ p = \langle\phi\circ p, p\rangle$ 。根據 point-surjective 我們知道 $\phi \circ p$ 對每個 $p$ 來說都是唯一確定的。現在把往下方 $B$ 的 $ev$ 也畫出，即可得出等式：

換句話說 $B \xrightarrow{f} B$ 的不動點即是

編碼的方式是找一個只有兩個物件 $1, T$ 的 category $M$ ，讓 lambda calculus 的 terms 是 $M$ -morphisms，這些技巧在 Categorical semantic 領域內相當常見。

到這裡必須檢查 lambda calculus 確實存在 point-surjective，歡迎自行嘗試。

按此編碼後可以得到 $ev \circ \langle\phi\circ p, p\rangle \xrightarrow{encode} \phi(p)(p)$ 。套到等式上

可以得到以下編碼

把 $\phi(p)$ 改寫成 $q$ ，於是等式可以寫成 $q(p) = f(\phi(p)(p))$ ，而函數套用語法可以用 $\lambda$ 退化，於是得到

注意到 $q$ 的定義是非遞迴的，因此一定是可定義的。

計算即可發現確實 $q(p) = \phi(p)(p) = f(\phi(p)(p))$ 。因為所有的 $\lambda$ -term 都屬於 $T$ ，所以現在我們知道任何 lambda calculus 的函數都有不動點。

取 category $\bold{Sets}$ 並令 $B = 2$ 就可以證明 [Cantor's theorem](math-0059)。我們需要引理

Proof

存在 $2 \xrightarrow{\text{not}} 2$ 令所有 $1 \xrightarrow{b} 2$ 都滿足 $\text{not} \circ b \ne b$ ，所以對任何集合 $A$ 都不存在 $A \to 2^A$ 的 point-surjective 函數，因此也不存在 $A \cong 2^A$ 。