シーケント計算の完全性定理（線形論理） - 曇りなき眼で見定めブログ

　前回こんなことを書いたけれど更に完全性定理について

cut-elimination.hatenablog.com

　Troelstra先生の本を読んで線形論理の代数的意味論の完全性定理を勉強しているところなのだけれど、

Lectures on Linear Logic (Lecture Notes Book 29) (English Edition)

作者:Troelstra, A. S.
Center for the Study of Language and Inf

シーケント計算と代数を対応させるというのはこうやるのだなあ。代数論理を全然知らなかったので驚いた。またもや完全性定理の驚き。ちなみにここでいう代数というのは半順序集合に結びやら交わりやらモノイド構造やら随伴やらを入れたものである（かなり圏論が意識されている）。

　健全性は帰納法をゴリゴリやれば示せる。 $\Gamma \Rightarrow \Delta$ が証明できる時に任意のモデルで $[\Gamma] \leq [\Delta ]$ が言えれば良い（[]は対応する代数の元）。

　で、完全性はどうか。完全性とはなんらかのモデルで $[\Gamma] \leq [\Delta ]$ の時に $\Gamma \Rightarrow \Delta$ が言えることである。前回書いたような無矛盾な理論のモデルを作るのとは違う。

　まず、全てのモデルで $[\Gamma] \leq [\Delta ]$ の時でなくなんらかのモデルのみの話でええんかと思ったが、しかし「任意のモデルで〜」よりも条件が強くなっている訳だからこれで良い。そらそうだ。いずれにせよ。健全性定理もあるので $\Gamma \Rightarrow \Delta$ が証明出来れば任意のモデルで $[\Gamma] \leq [\Delta ]$ が妥当になる。てことはここで言う完全性定理となんらかのモデルでの妥当性が言えれば任意のモデルでの妥当性も言えちゃうのである。

　そしてこのなんらかのモデルというやつなのだが、やはり前回のようにシーケントという言語的なものを使って構成される。シーケントの $\Rightarrow$ は前順序であるから、「 $\Gamma \Rightarrow \Delta$ かつ $\Delta \Rightarrow \Gamma$ 」という同値関係で同値類を作れば半順序集合が得られる。そこから閉包作用素でごちゃごちゃやって〜とするとモデルが得られてしかもこのモデルの $\leq$ （このモデルでは $\subset$ がこれに当たる）は $\Rightarrow$ を含意しちゃったりする。

　リンデンバウム代数とかいう手法だが私はよく知らない。まあ前回の完全性定理の驚きがやはりここでもあって面白いのである。