指稱語意中集合解釋的缺陷

[dannypsnl]

舉例： $\mathbb{N} \to \mathbb{N}$ 的所有集合函數的集合 $\mathbb{N}^{\mathbb{N}}$ 是不可數的，但按照 inductive principle 生成的 $\text{nat} \to \text{nat}$ 程式函數則並非如此

[dannypsnl]

$2^A$ 是 $A$ 的冪集合，我們知道這就是 $A \to 2$，而又 $2$ 可以解釋為 $boolean$，所以對 $2^A$ 可以解釋為隨意問一個元素 $x \in A$，那 $x$ 是否屬於某個集合 $S$？而符合這個問題的「合理」集合都是 $A$ 的子集合，因此冪集合是所有子集合構成的集合

在這個設定下，反正當 $x \in A$ 又 $x \in S$ 那 $S \cap A$ 肯定是有東西，即便用 $S' = S \cup Y$ 且 $Y \cap A = \emptyset$ 以及 $Y$ 非空集合，我們也分不出來 $S'$ 跟 $S$ 有什麼差別。這也是一個重要的概念，也就是商去某些部分之後有些東西就沒差

[dannypsnl]

另一個更簡單的方法是 system F 中可以定義出 $V \cong (V \to 2) \to 2$^1 ，這對應到集合論中等於在說冪集合總是小於集合，在集合論中不合理但是在 F 中合理，其中 $2 = \forall X . X \to X \to X$

因此集合必定不是 F 的模型

[dannypsnl]

This is sort of complete