2007/07/14

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。

Labels:

<< 回到主頁