様相論理入門
療養中，特にやることもなく（医師曰く，”只管横になって体を休めること！”），仕方がないので小説を読み漁っています．
ジャンルはSFとミステリーが多くて，小川一水さんの本をはじめとして色々読んでいるのですが，
その中で井上真偽の「恋と禁忌の術語論理」がとても印象に残りました．
titleの通り，術語論理のもとに他の人の推理を検証していくだけの話なのですが，その中で様相論理について触れています．
様相論理とは，常に真とは言えない命題を扱えるようにしたもので，□φや♢φで表現されます．
私が学んできた集合論は古典的論理で展開される範疇でしたので，論理学の世界は自分が思っていたよりも奥が深いことを知り衝撃を受けました．
その後，本の中では探偵がモーダス・ポネンスを書き下していくのですが，論理学にいろんな表現があることを知って非常に興味を持ったので，書籍を購入して勉強しました．
良い本です．古典的論理学のはじまりから最近の研究課題まで知ることができます．
しかし初学者には勿論なかなかに難しく，様相論理がどんなものかを知りたかっただけの私は，この書籍で論理学の沼を見てしまいました．
様相論理について学ぶだけなら，第一部第二部を読めば十分でした．
強制法で何が展開されるのか愚かにも興味を持ってしまったのが運の尽きです．第三部の証明は面白いところだけ拾い読みして読むのがおすすめです．
強制法がよく理解できなかったので，Hamkinsの論文(※参考文献)を少しずつ読み進めています．
書籍の中でも，当初の目的の様相論理と認識論理（時間論理を含む）の内容が面白かったので自分のために簡単にまとめておきます．
詳細な証明や厳密な定義は書籍や関連資料に当たってください．
とにかく，タルスキ・クリプキらの功績がすさまじいです．
様相論理
書籍から引用すると，「様相論理とは，伝統的には命題の必然性・可能性・不可能性などの様相概念を扱う論理」で，
必然であることを示す演算子□，可能であることを示す演算子♢を使って表現が拡張された論理です．
この表現によって時制論理や命題動的論理PDLに応用範囲を広げていきます．
命題動的論理はその記述方法自体がプログラムとも関連が深いので計算機界隈の人間ならご存知かもしれません．
ある集合上の二項関係Rについて，その定義可能性は次表で与えられます．
| 分類 | 論理式 | Rの性質 |
|---|---|---|
| T | □p → p | 反射的 |
| B | p → □♢p | 対称的 |
| 4 | □p → □□p | 推移的 |
| 5 | ♢p → □♢p | ユークリッド的 |
| D | □p → ♢p | 継起的 |
| .2 | ♢□p → □♢p | 有向的 |
| L | □(□p→p) → □p | 推移的且つ無限上昇列がない |
この表は正規様相論理の性質を探るうえで非常に重要なので，備忘録用に掲載しています．
様相論理のシークエント計算体系を進めるうえでは，扱う正規様相論理がどの性質を満たしているかによって，実行できる計算内容が変わってきます．
※なお，強制法で拡張された論理はS4.2（T,4,.2を含む正規様相論理）と一致するらしいです．このあたりを詳しく知るために上述した論文を当たっています．
この表にある性質によって，正規様相論理はグラフ構造や関係を表現でき活躍の場を広げていきます．
最初様相論理を知った時には，このような可能性をはらんだ論理で解を一意に定めることができるのかと怪しみました．
小説では，正規様相論理上で決定可能性を検証していくのですが，書籍によると正規様相論理では
・”ある実効的な手続きPが存在して，任意の論理式φをPへ入力したとき，の時にはPが真を出力し，そうでない時は偽を出力する時，決定可能”となります．
認識論理
現実においては，エージェントごとに知識の内容が変わることも多々あります．
エージェントごとに変わる知識内容は，エージェントa∈Aに対して様相演算子（aは~~を知っている）を用いて，例えば正の内省”aがφであることを知っている”を
として表現できます．
このような知識の状態を表現できることに感動しました．
次に，命題が常に真とは限らないものとして，例えば命題”彼は笑っている”は，今は真であってもその後変わるかもしれません．
このような論理について認識論理では，公開告知演算子[φ]ψで表現が拡張されます．
これは，”真なφが公開告知された後にψ”を意味し，状態の変化を表現することが可能になり，詳細な定義は割愛するとモデルMを使って
で[φ]ψの充足表現は定められます．
なお，は，φはMから意味論的に帰結可能であることを意味しています．
書籍では，公開告知演算子と様相演算子で表現しながら，有名なシェリルの誕生日問題を解いています．
難問論理クイズ「幼女とシェリルの誕生日」で有名問題を撃破せよ - 明日は未来だ！
その他雑記
当初の目的の一つだった，恋と禁忌の術語論理で扱われたモーダス・ポネンスのシークエント計算やカット除去法についてもこの本に詳しく記載されていました．
ゲーデル数はコーディング値
強制様相論理ではボタンやスイッチが専門用語として登場してきて，思わず笑ってしまいました．
集合論・論理学をなめていました．数学の表現力はすさまじいです．
参考文献
数学における証明と真理 ―様相論理と数学基礎論― / 菊池 誠 編 佐野 勝彦 倉橋 太志 薄葉 季路 黒川 英徳 菊池 誠 著 | 共立出版
J.D.Hamkins : The modal logic of forcing, https://arxiv.org/pdf/math/0509616.pdf
