Logic

constructive logic proves that the law of the excluded middle is positively not refuted (its double negation is constructively true).

refute : 其 negation 可以被证明.

“not refuted” 与 “its double negation is constructively true”

$\phi\,\mathsf{true}$ 表示 $\phi$ 存在一个证明.

$\phi$ refuted, 表示 $\lnot \phi \,\mathsf{true}$.

那么 ”$\phi$ not refuted” 表示的, 实际上是 $\lnot\lnot\phi\,\mathsf{true}$. 这两个 $\lnot$ 是不能省掉的! 注意! (好别扭啊, 直觉上双否定就肯定了).