Glivenko Theorem

還沒正式開始看《Lectures on the Curry-Howard Isomorphism》（讓我喘兩天吧 XD），隨手翻，看到 Glivenko theorem：A formula $\phi$ is a classical tautology iff $\neg\neg\phi$ is an intuitionistic tautology。所以我在〈NJEdit〉裡面講的「p 在 classical logic 裡有效（但可能在 intuitionistic logic 裡無效）時，~~p 會在 intuitionistic logic 有效」只是這個定理的一個方向。Max 演習課是不是有提到這個定理？XD

--
此定理的證明是 exercise XD。