ラノベ×論理学という斬新な小説『恋と禁忌の述語論理』の技術的な部分のネタバレを含みます。いや、ネタバレしか含みません。Coqを使います。

Q01. SAT問題(p10)

(¬c→b)⋀¬(¬a→b)⋀(d→a⋀c) の充足解は?

含意を書き換え,二重否定除去で同値変形すると(c⋁b)⋀¬(a⋁b)⋀(¬d⋁(a⋀c)) さらに変形出来て(b⋁c)⋀(¬a⋀¬b)⋀(¬d⋁(a⋀c))

第2項から a,bはFalse。よって第1項からcはTrue。第3項から dはFalseとなり、c: 「私は台所の戸棚の上にいる」のみが正しい言明になる。

なお、主人公はp70において真偽値表を使って解いていた。それに対して硯さんの応答は

できれば選言標準形に展開してほしかったけれど・・・(p71)

というが、CNF/連言標準形の方が簡単に作ることができる。前述の変形をあと1ステップ進めると得られて、¬a⋀¬b⋀(b⋁c)⋀(a⋁¬d)⋀(c⋁¬d)がCNFとなる。

硯さんの指示通りにDNFにしてみよう。CNFの第3項を分配則をつかうとbの方はCNFの第2項を考慮すると⊥となるので展開せずに済むので¬a⋀¬b⋀c⋀(a⋁¬d)⋀(c⋁¬d)となり、第4項に分配則を使うとaについて同様のことが言えて¬a⋀¬b⋀c⋀¬d⋀(c⋁¬d)となり、第5項に分配則を使うと左側は第3項よりTとなり、右側は第4項よりTとなるので、結局¬a⋀¬b⋀c⋀¬dがCNFとなる。充足解は自明に一つしか存在しないことがわかる。

Q02. 行為は故意か？(p85)

Z(行為は故意でない)を証明せよ。仮定: P,Q,R,(P⋀Q)→S,S→T,T⋀R→U,U→Z

Coqで証明

Goal forall P Q R S T U Z: Prop,
 P->Q->R->(P/\Q->S)->(S->T)->(T/\R->U)->(U->Z)->Z.
Proof. intros. apply H5. apply H4. split.
- apply H3. apply H2. split;assumption.
- assumption. Qed.

硯さんは証明としては正しいが、仮定のうち U→Z つまり「必要のない行為を行ったならば行為は故意ではない」が妥当ではないと指摘し、正しい推論となっていないことを指摘する(p86)。

彼女は、正しい仮定を補うことで、¬Zつまり行為が故意である、という全く逆の結論を証明した(p93)。

¬Zを証明せよ。仮定: Y→¬Z,P,Q,R,S,T,T⋀Q⋀R→U,U⋀S→V,P⋀V→Y

Coqで証明

Goal forall P Q R S T U V Y Z:Prop,
  (Y->~Z)->P->Q->R->S->T->(T/\Q/\R->U)->
  (U/\S->V)->(P/\V->Y)->~Z.
Proof. intros. apply H. apply H7. split;try assumption.
apply H6. split;try assumption. apply H5. split;try assumption.
split; assumption. Qed.

印象的だったのは、『櫁川さんがそれがしきみの実だと認識してあえて渡したこと』から『行為が故意である』ことが形式的に証明され、それが現行法では殺意があると解釈されるということ。

Q03. 幽霊には足が無い？(p150)

硯さんは中尊寺先輩の推論を正しいと認めたうえで、排中律を使っていることを指摘した。排中律の使用、特に対偶命題による証明は様々な奇妙な推論を生み出す。ヘルペスのカラスの議論を敷衍して、彼女の家に住む幽霊に足が無いことを証明して見せた(p151)

私はできるわ。この家の『足』があるものを全て持ってきて。人間、人形、冷蔵庫のタコ、椅子、それらは全て『足』があるけれど、どれも幽霊じゃないわよね。だから『足があるものは幽霊ではない』すなわち『幽霊ならば足はない』

Coqで証明:

Axiom classic: forall (P:Prop), P \/ ~P.

Goal forall (thing:Type) (x:thing) (Leg:thing->Prop) (Ghost:thing->Prop),
  (Leg x -> ~Ghost x) -> Ghost x -> ~Leg x.
Proof. intros. destruct (classic (Leg x)) as [C|C]; try assumption.
exfalso. apply H; assumption. Qed.

Q04. 様相により証明が妥当でなくなる時(p263)

¬Qを証明せよ。仮定: P→I,Q→O,I->O->⊥,P

Coq で証明:

Goal forall P Q I O:Prop,
 (P->I)->(Q->O)->(I->O->False)->P->~Q.
Proof. intros. intro. apply H1.
- apply H. assumption.
- apply H0. assumption. Qed.

ところが少し仮定を様相的に変更するだけで、¬Qの証明ができなくなってしまう。

¬Qの反例を挙げよ。仮定: P→□I, Q→◇O, I⋀O->⊥, P

世界w が自身に到達できない時、P,Oを真、Q,Iを偽とする付値において、wにおいて仮定は充足するが¬Qは充足しない。