『論理学入門』

執筆日時：

論理学入門 (ちくま学芸文庫)

論理学入門 (ちくま学芸文庫)

“タブロー”という証明方法を使った入門書。

タブローの方法(英 tableau method)とは、真理の木(truth tree)あるいは意味論的タブロー(semantic tableau)または分析タブロー(analytic tableau)と呼ばれるものを用いて、論証の妥当性や、論理式が矛盾しているかやトートロジーであるかを機械的に調べる判定手続き(decision procedure)の一種である。ヤーッコ・ヒンティッカらのモデル集合という考え方を応用して作られ、レイモンド・スマリヤンによって広められた。

タブローの方法 - Wikipedia

複雑な論理式をバラバラにして、末端に残った矛盾をツブしていく感じ。

たとえば、 A \land B が true ならば、A = True と B = True バラせる。

けれど、A \lor B が true ならば、A = True, B = False という組み合わせと、A = False, B = True という組み合わせの二つにバラせる（枝分かれ）。

そんな感じに全部バラバラにしていって、最初の true と枝先があってるかをみればよい……という仕組みのようだ。

たとえば、(p \to q) \land (\neg p \to q) \to q という論理式の場合、これ全体を False と仮定し、

F:(p \to q) \land (\neg p \to q) \to q ……(1)

まず、最後にある \to をバラす。 F:A \to B ならば A：True、B：False なので（その逆もアリじゃない？　って自分は思ったんだけど。後述）、

T:(p \to q) \land (\neg p \to q) ……(2)

F:q ……(3)

このようにバラせる。(3) はバラしきったので、次は (2) をバラす。論理和で繋がれた式が真ならば、両方真のはず。

T:p \to q ……(4)

T:\neg p \to q ……(5)

あれ、ちょっとわかんなくなってきた。やっぱり、p.58 の“タブローの一般的な規則”を頭に叩き込んで、機械的な手続きでバラせるように訓練しなきゃいけないみたい。

最初 \to の部分があまり納得いかなかったが、「～ならば」と考えるのがだめであって、C# でいえば

return A ? (B ? true : false) : false;

だと考えれば至極もっともだった。「“A ならば B”が真だったら、“A が真、B が偽”っていう組み合わせとその逆があるだろ」というわけじゃない。“A が偽”だった時点で評価は終わり、論理式自体が 偽 になる。

よって、(4) と (5) はバラすときに分岐が発生する。先に (4) をバラす。

\left\{\begin{array}{l}F:p \\ T:q\end{array}\right.

後ろの分岐は (3) と矛盾するから閉じる。

F:p……(6)

次に (5) をバラす。

\left\{\begin{array}{l}F:\neg p \\ T:q\end{array}\right.

さっきと同様、後ろの分岐は (3) と矛盾するから閉じる。

F:\neg p……(7)

これは

T:p……(7)

にバラせるが、(6) と矛盾するので閉じる。

よって、すべてが矛盾で閉じられたので、F:(p \to q) \land (\neg p \to q) \to q は常に偽、つまり (p \to q) \land (\neg p \to q) \to q は常に真（トートロジー）。

おぉ……ちょっとだけわかった気がする。論理記号が、または・かつ・ならば・でない じゃなくて、単なる論理操作を表すモノに見えるまで訓練しないとだめだなぁ。