GLの健全性
Lem1を示せば残りは他の様相論理の健全性と同様に示せるので，Lem1だけ示す．
Lem1
フレーム$ F = \lang W, \prec \rangとする．
$ \bf L \equiv \Box(\Box\varphi\to \varphi) \to \Box\varphiは逆整礎かつ推移的なフレームを規定する． すなわち，$ \vDash_F \mathbf{L}$ \iff$ Fは逆整礎かつ推移的 ただし，ここで$ Fが逆整礎とはconverse well-formedのことで， 任意の非空な部分集合$ X \sube Wについて$ Xの極大元が存在すること
すなわち，任意の$ x'に対して$ x_M \not\prec x'となる極大元$ x_M \in Xが存在することとする．
proof
$ \implies: TODO
$ \impliedby
$ Fは逆整礎かつ推移的だとし，任意の付値$ Vと$ w \in Wで$ w \Vdash_{\lang F,V\rang} \Box(\Box\varphi\to \varphi) \to \Box\varphiであることを示す．
以下$ \lang F,V\rangは省略．
$ \Vdashの定義より$ w \nVdash \Box(\Box\varphi \to \varphi)または$ w \Vdash \Box\varphiをいえば良い，さらに言えば次のどちらかが言えれば良い．
1. $ w \Vdash \Box(\Box\varphi \to \varphi) \implies w \Vdash \Box\varphi
2. $ w \nVdash \Box\varphi \implies w \nVdash \Box(\Box\varphi \to \varphi)
2を示す．$ w \nVdash \Box\varphiを仮定する．
$ X := \{ x \in W \mid w \prec x ~\&~ x \nVdash \varphi \}とする．
$ w \nVdash \Box\varphiであるから，$ w \prec xで$ x \nVdash \varphiとなる$ xが存在するので，$ Xは非空である．
よって明らかに$ X \sube Wで$ Xは非空だから整礎性より$ Xに極大元$ x_Mが存在する．
$ x_M \prec yとなる任意の$ yについて考えると，
$ x_Mの極大性より$ y \notin Xである．
更に推移性より$ w \prec x_m \prec yより$ w \prec yだから，$ y \Vdash \varphiが言える．
$ y \nVdash \varphiだった場合，$ w \prec yと合わせて$ y \in Xとなってしまい$ x_Mの極大性に反する．
推移性より$ w \prec x_m \prec yより$ w \prec yである．
よって
$ x_M \Vdash \Box\varphi
$ x_M \nVdash \Box\varphi \to \varphi
$ w \nVdash \Box(\Box\varphi \to \varphi)
以上より
$ w \Vdash \Box(\Box \varphi \to \varphi) \to \Box\varphi