…ょうか？論理に戻ると古典論理の形式的体系（証明系）からそのリンデンバウム代数を作るとブール代数になります。そして、形式的体系におけるセオリー（定理集合）は、対応するブール代数のフィルターに対応します。矛盾するセオリー（すべての命題を定理にしてしまった定理集合）は最大のフィルターとなり、論理的真しか認めないセオリー（トートロジーだけを定理とする定理集合）が最小のフィルターへと対応しますね。古典論理の形式的体系（証明系）からリンデンバウム代数を作る構成を関手と考えて、Lind:C…

…多寡＜たか＞によって古典論理と直観主義的論理、その他のナンタラ論理に別れるし、様相記号や、さらにもっと目新しい論理記号を入れた体系もあります。（形式的）証明もヒルベルト方式、ゲンツェン方式（シーケント計算）、タブロー方式なんてのがありますね。こういう多様性は「論理の豊饒＜ほうじょう＞さ」を示すものでしょうが、僕は、「なんだか博物学・分類学みたいだなー」とも感じます。ストラスバーガーの質問と答えは、こういう不満感を多少は解消してくれます。続くのかな実は1回読み切りで書き切ろうと…

…記号としての含意だ。古典論理なら、A⊃B は ¬A∨B で置き換えてもよいので、記号「⊃」は不要だともいえる。が、含意記号がないのは気持ち悪い。記号「→」はシーケントの前件（前提）と後件（結論）を区切る記号、なんて読むか知らない。「→」を"entails"という人もいるし、僕もそう読むときもあるが、意味的帰結（上記の記号では「|⇒」）と区別が付かなくなる。「|⇒」は、前提と結論の概念を意味的（モデル論的）な主張（assertion, judgement)として定義したもので、…

…明”とは仕様記述言語（または制約記述言語）レベルの証明で、古典的な“プログラムの証明”とはどうもストレートに結びつかないのです。プログラムの証明は、厳密なソースコードレビューみたいなもんだけど、ソースコードに対応するフォーマルな概念が見あたらないのね。だから、ソースレベルの変換とか合成とかを記述すべき場所が分からない。ホーア式のような形でSenΣのなかにソース断片を押し込めるけど、なんか気色悪いよ。で、「ソースコード（構文的対象）に対応する圏論的概念てなによ？」が最近の疑問。

…。[/追記]証明系が古典論理に基づく標準的なシステムなら、極大セオリーTは次の性質を持ちます。 任意のf∈Lに対して、f∈T か ¬f∈T のどちらか一方が必ず成り立つ。 ¬fはfの古典的否定です。もし、f∈T かつ ¬f∈T ならば、(f∧¬f)∈Tのはずです、これは証明系が fとgからf∧gを導くからですね。(f∧¬f)はfalseですから、false∈Tとなり、さらにfalseを仮定してどんな論理式でも導出できるんで、T = L となり無矛盾の仮定に反します。よって、「…

…pace）になるが、古典論理に限定すれば、論理的対象は標数2の体を基礎体とする環付き空間と思える。非古典論理まで一般化するとしても、適当な代数系（環じゃないかもしれない）が付いた空間としてlogical varietyが定義できそうだ。日常の素朴な推論とかも含めて、この世には小さな（大きいのもあるけど）論理系が無闇とたくさんあるだろう。それらはそれぞれにモデルの世界を持つ。「矛盾する」とか「妥当性がある」とかは、実はモデルに対して相対的なもんだ（純構文的な概念もあるにはあるが…

…持つことになる。これは、コンパクト性定理の主張に他ならない。以上のことから、コンパクト性定理は、モデル空間のコンパクト性とほぼ同じ内容であることがわかったろう。ところで、今までの議論ではハウスドルフ性を使ってない。古典論理以外の論理を考えたりすると、モデル空間Xがハウスドルフであることは保証できない気がするが、僕はよくわかってない。一般的なモデル空間としては、必ずしもハウスドルフとは限らない局所コンパクト空間が出現するような気がするのだけど、気がするだけで、確証も確信もない。

…学を考えたら、それは古典論理になってしまう、ってことは、ある人々には自明のことでしょう。僕にとっては自明ってわけではなかったのだけど、「たぶん、そうだろうな」程度の感触はありました、二、三十年前のことだけど。そのことを論理の専門家（少なくとも論理で学位は持っている）に話したら不審な顔をしていたし、代数幾何の専門家（少なくとも代数幾何で学位は持っている）に話したらまったく興味がない様子でした。確かに、「こことあそこを架橋してみて、何がうれいしか？」と問われると、答えに窮＜きゅう…