Glivenko の定理の代数的証明

なんかいいやり方があったような気がしたけど思い出せなくて考えてたらできたメモ。いまいち証明できた気分にならないので，もしかすると正しくないのかもしれない。

Theorem: 命題論理式 が claissical tautology ⇔ が intuitionistic tautology.

右から左は簡単で，左から右が問題。classical tautology の二重否定をどんなハイティング代数でどう解釈しても 1 になることをいう。

準備

H をハイティング代数とし， とする。また とする。

Lemma 1: H' は H の順序でブール代数になる。

ただし演算の入れ方に注意が必要。meet と complement は H のものでよいけど，H' は join で閉じていない。H での join を とすると，H' の join は で与えられる。

Lemma 2: はハイティング代数の準同型である。

これは 0, 1, meet, join, relative pseudocomplement が二重否定で保存されることをいえばよい。具体的には

• 
• 
• 
• 
• 

がいえればよい。join は H と H' で定義が異なるのでこうなる。

これ，代数的に示すのはだいぶ難しい気がするので，論理式で書いて LJ で証明するのが一番楽だと思う。それか自動証明。

Theorem の証明

論理式 の付値 v での解釈を と書くことにする。

任意のハイティング代数 H とその上の付値 v をとる。 で H' 上の付値を定義する。

は準同型だから任意の論理式 に対して である。

特に が classical tautology の場合，H' がブール代数であることから だから である。H, v は任意だったから は intuitionistic tautology である。