待てよ、前のエントリーと同じこと、スペクトルとモデルの関係について以前書いたのだった。 「コンパクト空間と論理／モデル論」 「仕様技術への道 -- インスティチューションを縮めてみる」 ある形式系が採用している論理が古典論理なら、そのリンデンバウ…

Sをソート集合、Vを変数記号の集合で、V→Sでソート付き変数が定義されているとする。ρ:S→|C|がSの圏Cでの解釈として、ρによりVを圏Cに上江州アタッチできる。これを詳しく記述。 終状態セットが複数あるオートマトン。

指標を単なる有向グラフと考えるのはとてもいいとわかってきた。等式的セオリーまず、等式的セオリーとグラフのあいだには次の関係がある。 指標 圏の生成グラフ ソート 対象の生成集合 関数記号 射の生成集合 項形成規則 自由構成 項 射 等式系 グラフの（…

本編のコレだけど、部分関数／部分演算を等式的一階述語論理でどう扱うかの例題として面白いかもしれない。次のような体系も考えるといいかも。 domu（id(dom(-))に対応）とcoduを持つ体系 「…が存在する」を意味する述語E(-)を持つ体系

「セオリーと証明の圏」とか「圏論的形式言語理論の問題」とかに謎なことが書いてある。今読むと分からん！ 解釈し直さないと。命題論理の場合のリンデンバウム（Lindenbaum）代数はハッキリしている。ブール代数（束）とかハイティング代数（束）だ。この場…

本編で、"What is a logic, and what is a proof?" (April 8, 2005) by Lutz Strassburger（http://citeseer.ist.psu.edu/723320.html）を紹介したことがある（けっこう良く書けている）のだけど、（ほぼ）同じ題名の論文： Title: What is a Logic? Authors…