リンデンバウム代数とエルブラン・モデル

「セオリーと証明の圏」とか「圏論的形式言語理論の問題」とかに謎なことが書いてある。今読むと分からん！ 解釈し直さないと。

命題論理の場合のリンデンバウム（Lindenbaum）代数はハッキリしている。ブール代数（束）とかハイティング代数（束）だ。この場合、真偽値の代数だけど、値を対象、順序を射とすれば圏だから、リンデンバウム圏といってもよい。つまり、意味付与すべき世界（セマンティクス）を構文と演繹系だけから絞り出している。

白旗さんが、論理系CMLL(A)（Aはベースとする圏）に対してコンパクト閉圏を構成しているけど、これもリンデンバウム構成といえるだろう。やはり演繹系から圏を絞り出している。

エルブラン（Herbrand）・モデルがリンデンバウム構成とは微妙に異なるのは、真偽値が古典ブール束だと決めつけている点だろう。エルブラン基底の部分集合をモデルと同一視する所でこのこと（古典2値なこと）は明らか。ほんとのリンデンバウム構成をするなら、閉原子論理式の集合＝エルブラン基底に、演繹に基づいた同値関係（p≡q とは |- p⇔q）を入れるべきだろう。

エルブラン・モデルは、リンデンバウム・モデルの真偽値の部分を無理矢理ブール代数にしてしまったようなものかな？ となると、真偽値のリンデンバウム代数からブール代数への写像とエルブラン・モデルが1：1対応するはず。

ん？ なんかの論理代数（束）から古典ブール代数への準同型の全体って、ストーン双対みたいなもんじゃないのか？ 論理代数Aに対してA^* = hom(A, B)（Bが古典ブール代数）。「エルブラン・モデルの全体＝リンデンバウム代数の双対」かな？ そうだとカッコイイ。