ちょうど3年前（2006年10月28日）のエントリー「古典論理は可換環論なんだよ」へのトラックバック、「なんだろな」とか病み上がりのモンヤリ頭でたどってみました。ンガッ。id:tri_iro さん、この書きっぷり、こりゃ基礎論のプロですよね -- 「ゲーデルの不完全性定理を代数学を使って表現してみた」
僕は、古典論理と可換環の関係を、初等的計算を愚直にガリゴリやれば分かる範囲でとりあえず書いてみたのですが、tri_iroさんがより発展的で深い内容、なんと2007年の結果を示唆するようなところまで書いてくれました。「続き」とかいうと失礼になりそう、レベルが違い過ぎますからね。
再帰的可算イデアルとか実効的閉集合とかになると、僕はもうよく知らない。「3. スペクトルの空間： 記述集合論，再帰理論，位相と測度」以降に書いてある話は「ほえー、そんなことがあるんですか」という感じ。いやー、すごいもんですな。
それで思い出してみると、「古典論理と可換環の関係」に何で僕が興味を持ったかというと、「コンパクト性定理はなんで『コンパクト』っていうんだ？」とかどうでもいい好奇心もあったし、「古典論理は可換環論なんだよ」の最後で述べたように、手計算だけ頑張れば割と面白い結果が出るので楽しいって理由があります。
もうひとつの下心として、例によって計算（computation、主にコンピュータの行為）の話に適用できないかなーと探っていた（妄想していた）のです： p, q などを古典論理の命題（構文的には論理式）として、M, N などをモデルとします。M |= p は「Mがpを満足（充当、satisfy）する」ことを表すとしましょう。ライプニッツは「性質で区別できないモノは同じとみなせ」と言ったとか言わないとかなんで、「すべてのpに対して M |= p ⇔ N |= p」のとき M ≡ N と定義します。
いま定義した関係≡はモデル全体の集まりModel（集合かどうかは不明）の上の同値関係になります。Model/≡ は、Modelより小さくなってはいますが、これだけではあまりハッキリとしません。ところが、{p∈命題 | M |= p} のほうはブール代数のイデアル（フィルターと言っても事実上同じ）になり、このイデアルと(Model/≡)の要素が1：1に対応します。多少のゴニョゴニョで、(Model/≡)をハッキリとした位相空間と捉えていいことになります。
モデル全体という茫漠とした集まりに自然な同値関係を入れると、サイズの小さな集合*1になるばかりか、位相まで付いて来るという実にありがたい状況。古典命題論理の場合では、モデルとはいっても、命題変数への真偽値割り当てに過ぎないので、モデル全体をイメージできないわけでもないですが、もっと事情が複雑になると、モデル全体はほんとにとらえどころがありません。
計算で便利に使える論理として、状態遷移による作用を様相オペレータと考えた一種の様相論理があります。そのモデルの全体は余代数の圏としていちおう定式化はできます。が、適当な同値関係で割ってサイズの小さな集合になれば扱いやすいし、なんらかのスペクトルとしての位相（ないしは位相もどき）が入ればもっと扱いやすいでしょう。
ちょと考えた後で、これは、僕の知っている道具、僕の知力・気力ではジェンジェンできそうにない、と判断してサッサとあきらめました。計算向け論理のスペクトルって誰か作っているんかな？ ご存知の方、教えてください。
*1:[追記]日本語が大変曖昧でした。集合のなかでサイズが小さなモノのことではなくて、集合であることがすなわちサイズが小さいことだって意味です。[/追記]
