昨日話題にした型推論とかの関係で、最近また、ソフトウェアの設計・実装に論理をどう応用できるか、とか考えています。まー、応用できるのは当然、つうか、現在のコンピュータシステム自体が論理（数学基礎論）の応用みたいなもんですが、もう少し日常的な感覚で、「論理を現場的に使うにはどうしたらいいの？」みたいな問題意識です。
論理の教科書は、日本語でもいい本がたくさんあります。昔（僕が若い時分）から、竹内外史、前原昭二なんて世界的な泰斗がシッカリした教科書を著してくれていたので、（その道の専門家は別として）普通に勉強するには十分すぎるくらいのテキストがあります。
ただ、技術者／プログラマが実務上の知識を仕入れる目的には本格的過ぎるきらいがあります。若くて時間がある方々には、本格的な勉強をお勧めはしますが、誰でもがタクサン時間を持っているわけでもないですしね。もうちょっとお手軽なショートコースがないものかな、と。命題論理が中心の本とか、哲学っぽいもの、ディベート方向にいっちゃうヤツは、実務者にはまったく向いてないしねぇ。僕は、 小野寛晰・著『情報科学における論理』をたまに眺めます。この本はなんでも書いてあって、辞書的に使うにはとても便利です。が、自習には適していません。
それと、僕が気になっているのは、「命題論理 vs 述語論理」「構文論 vs 意味論」「古典論理 vs 直観論理」みたいな分け方。いや、僕自身もこのテの分類に依拠しているし、教育コースとして伝統的でもあるんだけど、計算機のハナシだと、ここらへんが混じっちゃうんですよ。「分けたらクリアになる」って側面がないとも言えないけど、そういう分類に労力を使うのはかなりバカバカしい。
「論理とはなにか？」で紹介したストラスバーガー（Lutz Strassburger）は、ナントカ論理とかカントカ論とかの区別は捨象した上で、「論理とはプレ順序集合」「論理とは圏」という見方を提示しています。僕は、このような見方に共感します。いろいろな論理達を対等に扱うと、それらの論理（プレ順序集合、圏）のあいだを単調写像や関手で結びつけようという発想が自然に湧いてきます。
現実のコンピュータシステムやソフトウェアを、眼をこらして見てみると、ロジカルシステムがたくさん含まれています。どれが構文領域でどれが意味領域とかいう区別は困難です。そこには、たくさんのロジカルシステムが相互に絡まり重なりながら蠢＜うごめ＞いているという事実があるだけです。
こういう状況の定式化として、現状ではインスティチューションが一番包括的だと思います。ですが、インスティチューションの定義は「圏の圏」（あるいは圏のタバ）の形をしていて、インスティチューションのあいだの準同型を考えると「圏の圏の圏」を扱うことになります。それに、インスティチューションの準同型って概念はあんまりハッキリしてないし。
僕の個人的な印象（錯覚や誤解かもしれません）では、インスティチューションは論理の双対性をうまくキャプチャできてない気がします。この感覚は、「当方記事には過ぎた続編、よみがえる妄想」の妄想として書いた「計算（コンピュータ）向け論理のスペクトル」がうまく定義できない不満、もどかしい感じと同根です。
とまー、いろいろゴチャゴチャ書いたのですが、「技術者／プログラマのための論理」に対して期待することをまとめると次のようでしょう：
- ナントカ論理とかカントカ論とかの区別には拘泥しない
- たくさんのロジカルシステムが絡み合って存在する状況を記述できる
- インスティチューションよりはライトウェイト
- できるならば、双対性をうまく取り出せる
要望を出すだけで、それに応える能力は持ち合わせてないのですが、きわめて断片的にでも、上記の線に沿った「技術者／プログラマのための論理」について考えて書くことがあるかもしれません。
