3
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

『恋と禁忌の述語論理』における論理学

Posted at

ラノベ×論理学 という斬新な小説『恋と禁忌の述語論理』の技術的な部分のネタバレを含みます。いや、ネタバレしか含みません。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は充足しない。

3
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
3
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?