【勉強記録】コンピュータサイエンスにおける様相論理

鹿島亮さん著のコンピュータサイエンスにおける様相論理を勉強するにあたって、演習問題や分からなかった箇所、補足などを記録していく。この方が書かれた数理論理学も勉強したことがあり、とても分かりやすかったので安心して読み進めていこうと思う。

第1章 準備：命題論理

以下、断りがない限り p,q,a,b は命題変数、 \phi, \psi は論理式とする。

演習問題1.1.3
結合の強さの順に括弧でくくっていく。

\begin{aligned} (\neg\neg p\rightarrow q)\wedge r\leftrightarrow\neg s\lor t &\iff (\neg(\neg p)\rightarrow q)\wedge r\leftrightarrow(\neg s)\lor t \\ &\iff((\neg(\neg p))\rightarrow q)\wedge r\leftrightarrow(\neg s)\lor t \\ &\iff(((\neg(\neg p))\rightarrow q)\wedge r)\leftrightarrow((\neg s)\lor t) \\ &\iff((((\neg(\neg p))\rightarrow q)\wedge r)\leftrightarrow((\neg s)\lor t)) \end{aligned}

---

演習問題1.1.6
関数型プログラマには慣れたこと！

\mathrm{Lh} はLengthの略。 \mathrm{Lh}(\phi) の定義：

\begin{aligned} &\mathrm{Lh}(\top)=1 \\ &\mathrm{Lh}(\bot)=1 \\ &\mathrm{Lh}(a)=1 \\ &\mathrm{Lh}(\neg \phi)=1+\mathrm{Lh}(\phi) \\ &\mathrm{Lh}(\phi\wedge\psi)=1+\mathrm{Lh}(\phi)+\mathrm{Lh}(\psi) \\ &\mathrm{Lh}(\phi\lor\psi)=1+\mathrm{Lh}(\phi)+\mathrm{Lh}(\psi) \\ &\mathrm{Lh}(\phi\rightarrow\psi)=1+\mathrm{Lh}(\phi)+\mathrm{Lh}(\psi) \\ &\mathrm{Lh}(\phi\leftrightarrow\psi)=1+\mathrm{Lh}(\phi)+\mathrm{Lh}(\psi) \\ \end{aligned}

\mathrm{Sub} はSubformulaの略。Subsetかと思った。 \mathrm{Sub}(\phi) の定義：

\begin{aligned} &\mathrm{Sub}(\top)=\{\top\} \\ &\mathrm{Sub}(\bot)=\{\bot\} \\ &\mathrm{Sub}(a)=\{a\} \\ &\mathrm{Sub}(\neg \phi)=\{\neg \phi\}\cup\mathrm{Sub}(\phi) \\ &\mathrm{Sub}(\phi\wedge\psi)=\{\phi\wedge\psi\}\cup\mathrm{Sub}(\phi)\cup\mathrm{Sub}(\psi) \\ &\mathrm{Sub}(\phi\lor\psi)=\{\phi\lor\psi\}\cup\mathrm{Sub}(\phi)\cup\mathrm{Sub}(\psi) \\ &\mathrm{Sub}(\phi\rightarrow\psi)=\{\phi\rightarrow\psi\}\cup\mathrm{Sub}(\phi)\cup\mathrm{Sub}(\psi) \\ &\mathrm{Sub}(\phi\leftrightarrow\psi)=\{\phi\leftrightarrow\psi\}\cup\mathrm{Sub}(\phi)\cup\mathrm{Sub}(\psi) \\ \end{aligned}

\mathrm{Var} はVariableの略。 \mathrm{Var}(\phi) の定義：

\begin{aligned} &\mathrm{Var}(\top)=\{\} \\ &\mathrm{Var}(\bot)=\{\} \\ &\mathrm{Var}(a)=\{a\}\\ &\mathrm{Var}(\neg \phi)=\mathrm{Var}(\phi) \\ &\mathrm{Var}(\phi\wedge\psi)=\mathrm{Var}(\phi)\cup\mathrm{Var}(\psi) \\ &\mathrm{Var}(\phi\lor\psi)=\mathrm{Var}(\phi)\cup\mathrm{Var}(\psi) \\ &\mathrm{Var}(\phi\rightarrow\psi)=\mathrm{Var}(\phi)\cup\mathrm{Var}(\psi) \\ &\mathrm{Var}(\phi\leftrightarrow\psi)=\mathrm{Var}(\phi)\cup\mathrm{Var}(\psi) \\ \end{aligned}

\phi\{p:=\psi\} の定義：

\begin{aligned} &\top\{p:=\psi\}=\top \\ &\bot\{p:=\psi\}=\bot \\ &p\{p:=\psi\}=\psi \\ &q\{p:=\psi\}=q \\ &(\neg \phi)\{p:=\psi\}=\neg(\phi\{p:=\psi\}) \\ &(\phi_1\wedge\phi_2)\{p:=\psi\}=\phi_1\{p:=\psi\}\wedge\phi_2\{p:=\psi\} \\ &(\phi_1\lor\phi_2)\{p:=\psi\}=\phi_1\{p:=\psi\}\lor\phi_2\{p:=\psi\} \\ &(\phi_1\rightarrow\phi_2)\{p:=\psi\}=\phi_1\{p:=\psi\}\rightarrow\phi_2\{p:=\psi\} \\ &(\phi_1\leftrightarrow\phi_2)\{p:=\psi\}=\phi_1\{p:=\psi\}\leftrightarrow\phi_2\{p:=\psi\} \\ \end{aligned}

---

演習問題1.1.7
\mathrm{Sub}(\phi) の要素数を |(\mathrm{Sub}(\phi)| と表すことにする。

\phi=\top, \bot, a のとき

|\mathrm{Sub}(\phi)|=1\leqq\mathrm{Lh}(\phi)=1

\phi=\neg\psi のとき
|\mathrm{Sub}(\psi)|\leqq\mathrm{Lh}(\psi) を帰納法の仮定とする。

\begin{aligned} |\mathrm{Sub}(\phi)|&=|\{\neg\psi\}\cup\mathrm{Sub}(\psi)| \\ &\leqq 1+|\mathrm{Sub}(\psi)| \\ &\leqq 1+\mathrm{Lh}(\psi) \\ &=\mathrm{Lh}(\phi) \end{aligned}

\phi=\psi_1\wedge\psi_2, \psi_1\lor\psi_2, \psi_1\rightarrow\psi_2, \psi_1\leftrightarrow\psi_2 のとき
|\mathrm{Sub}(\psi_1)|\leqq\mathrm{Lh}(\psi_1),~|\mathrm{Sub}(\psi_2)|\leqq\mathrm{Lh}(\psi_2) を帰納法の仮定とする。

\begin{aligned} |\mathrm{Sub}(\phi)|&=|\{\phi\}\cup\mathrm{Sub}(\psi_1)\cup\mathrm{Sub}(\psi_2)| \\ &\leqq 1+|\mathrm{Sub}(\psi_1)|+|\mathrm{Sub}(\psi_2)| \\ &\leqq 1+\mathrm{Lh}(\psi_1)+\mathrm{Lh}(\psi_2) \\ &=\mathrm{Lh}(\phi) \end{aligned}

以上より、任意の論理式 \phi について、 |\mathrm{Sub}(\phi)|\leqq\mathrm{Lh}(\phi) が成り立つ。 \Box

---

演習問題1.2.8
真理値表を丁寧に埋めていけば、トートロジーである論理式の列はすべて true になる。それを確かめる。

---

演習問題1.2.9
(1)

• \top\equiv p\rightarrow p
  p\rightarrow pはトートロジーであるから、任意の付値関数 f に対して f\vDash p\rightarrow p である。また、定義から f\vDash\top である。以上から \top\equiv p\rightarrow p~~\Box
• \bot\equiv\neg(p\rightarrow p)
  p\rightarrow p\iff\neg(\neg(p\rightarrow p))より、任意の付値関数 f に対して f\vDash\neg(\neg(p\rightarrow p)) である。したがって、 定義からf\nvDash\neg(p\rightarrow p)である。また、定義から f\nvDash\bot である。以上から \bot\equiv\neg(p\rightarrow p)~~\Box
• \phi\wedge\psi\equiv\neg(\phi\rightarrow\neg\psi)
  上2つのように定義の式をコネコネして示すのは難しそうなので、真理値表に頼ろう。朧げながら浮かんできた真理値表から、論理式 \phi\wedge\psi と \neg(\phi\rightarrow\neg\psi) 列のパターンが等しいので \phi\wedge\psi\equiv\neg(\phi\rightarrow\neg\psi)~~\Box
• \phi\lor\psi\equiv\neg\phi\rightarrow\psi
  1つ上と同様に考えて \phi\lor\psi\equiv\neg\phi\rightarrow\psi~~\Box

(2)

\begin{aligned} \phi\leftrightarrow\psi&\iff(\phi\rightarrow\psi)\wedge(\psi\rightarrow\phi) \\ &\iff\neg((\phi\rightarrow\psi)\rightarrow\neg(\psi\rightarrow\phi)) \end{aligned}

---