上一篇 LdBeth：NuPRL 中的证明 (二) – 我从来不写递归的
这篇的主要內容是 Virtual Evidence: A Constructive Semantics for Classical Logics 和 Constructive Reading of Classical Logic 的导读。 也算是第一次展示了下 NuRPL 中的证明，順帯引入 squash type 的概念。
MLTT Agda 中要获得 LEM 得 posutulate （防止你们说 CubicalTT）。众所周知这样 p 出来的 LEM 虽然和 MLTT 相容，但还是沒有 computational meaning 的，这样的 classical logic 是沒有灵魂的。
那 NuPRL 是怎么解決这个的呢？
Recall, refinment type OR subtyping in NuPRL
$\{x:A\ |\ P(x) \}$
it is easy to get non dependent form
$\{S\ |\ T\}$
Unit type 只有一个 element $*$ ，因而当 proposition P 成立时 $\{Unit\ |\ P\}$ 也只有一个 element，而 P 为 False (which is an alias to Void) 时这个类型等于 Void。
在 ITT 中，P 的证明是一个具體的 p : P，而用 refinement type $\{Unit\ |\ P\}\; abbrev \;\{P\}$ 表示 classical logic 的命题就可以把 P 的证明给 squash to trivial。这样显然地，我们有把 constructive proof to classical proof 的 computation procedure $\lambda x.*\in P \implies \{P\}$ ，而反之则不一定成立，从而規避了任意用 classical proof 进行 constructive proof。
然后就要有 double negation rule $\lambda x.* \in \neg\neg P \implies \{P\}$ ： $\neg\neg P$ 表明 P 不为 False，而由于 refinement type 的定义当 P 不为 False 时，因为 $\{ P\}$ 只可能有一个 element，所以很容易就得到它的 computational meaning，也就是 const trivial 这样一个函数。
这样就可以证明 $\forall P : \mathbb{P}\ . \{P\}\implies \neg\neg P$ ，也就是从 classical proposition 到 intutionistic double negation 的 formation。在 NuPRL 中的证明如下。
