『論理学をつくる』で論理学をつくる

導入

記事のタイトルがトートロジーになっています. トートロジーというのは

「トマトはなぜ赤いんだ？」
「赤いから赤いんだよ」

というような, 無意味な同じ言葉の繰り返しのことです.
ところで, 論理学では常に真になる文のことをトートロジーと言います. 例えば「クジラは哺乳類であるか, 哺乳類でないかのどちらかだ」というような文は, クジラについて何もわかっていかなったとしても正しいとわかるトートロジーです.

では以下の文はどうでしょう.

この占い師が信用できるなら, 私の明日旧友と出会う
この占い師は信用できる
よって, 私の明日旧友と出会う

理屈は正しそうです. ではこれはどうでしょう.

この占い師が信用できるなら, 私の明日旧友と出会う
私は翌日旧友と出会った
よって, この占い師は信用できる

予言が当たったのなら本物感はありますが, インチキ占い師が適当なことを言ったのにも関わらず, たまたま予言が当たったという可能性もありそうです. ということでこの理屈は間違っていると言えそうです.

常に正しい文, 論理的に正しい/間違った推論. こういった事柄を厳密に扱うのが論理学です.
なんだ, 論理学は随分当たり前のことを研究するんだなぁと思うかもしれません. しかし, 推論の正しさや矛盾と言った事柄を一般的に, 明確に, 統一的に示すのは難しそうです. 普段行っている論理的判断であっても, それがなぜ正しいのか説明できなかったり, 対象が複雑になると判断がつかなくなったりします.

本書は論理学を全く学んだことのない人のための教科書です.
初学者でも独学できるように丁寧な説明や練習問題が満載です (ちゃんと練習問題に解説がついているのは嬉しいポイントです. というかなぜ大学の教科書のような本にはついてないことが多いのでしょう). 身近な例から始まって, 述語論理, 自然演繹, 非古典論理など, 様々な話題が盛り込まれています.
序文によると, このような欲張りな目標を立てたために本が分厚くなった (B5 版 400 ページ以上) という事情のようです.

論理学というといかにも堅苦しそうな分野ですが, 著者の軽妙な語り口も相まって気負わず読み進められます. 論理学には全く触れたことはないが, きちんと入門してみたいという方におすすめです.

印象に残った点

タイトル通り, 論理というものを厳密に扱うための体系を少しずつ作っていくのが本書のスタイルです. 記号と抽象の奥深い世界が広がっています. 印象的な部分をまとめます.

論理学を「つくる」とはどういうこと？

論理を研究するに当たって最初に行う作業は, 論理を厳密に扱うことができる体系を作ることです. つまり, 論理を扱うのに都合の良い言語を作って, その人口言語を操作することで話が進みます.

なぜ人工言語が必要なのかというと, 自然言語 (日本語や英語などの日常生活で使われる言葉のこと) では論理学が対象とする論理の形式が曖昧になってしまうことがあるからです.
例えば

アリスはボブを愛している
ボブはアリスに愛されている

このペアは同じことを言っているので, 文の骨格を取り出して次のような形式であれば同じだとみなせるように思えます.

A は B を愛している
B は A に愛されている

しかし, 次の例はどうでしょう.

みんなは誰かを愛している
誰かはみんなに愛されている

この 2 文は言っていることが違います. 1 は誰もがそれぞれ愛する人を持っているということであるのに対し, 2 は全員に愛されるアイドルのような人がいるという内容です.
このように, 自然言語では論理の形式が文法によって見えづらくなることがあるわけです. そこで「推論の妥当性を明確にする」という目的に即した言語を作るというわけです.

最初の人工言語 L(Logic の頭文字) は馴染みのあるものです.
「アリスはボブを愛している」というような単純な文を P, Q, R などのアルファベットで表します. そして, 「ならば」は「→」, 「かつ」は「∧」, 「または」は「∨」, 「ではない」は「¬」として記号で置き換えます.

論証の例を見てみます.

トムは東京か大阪にいる
トムが大阪にいるならば, ジェリーも大阪にいる
ジェリーは今大阪にいない
よって, トムは今東京にいる

これは次のように記号化できます.

P ∨ Q
Q → R
¬Q
よって, P

PQR の意味は次のとおりです.

P: トムは東京にいる
Q: トムは大阪にいる
R: ジェリーは大阪にいる

「P」, 「Q → R」のような式のことを論理式と呼ぶことにします.
ここで, 各論理式の真偽には関係がありそうです. 例えば, Q が真なら¬Q は偽である, というような関係です. これを真理値表をとして定義しておきます.
例えば∨の真理値表は次のようにします. もちろん他の記号 (∧, ¬, →. これらを論理結合子と呼ぶ) についても定義します.

1
2
3
4
5
6
| P   | Q   | P ∨ Q |
| --- | --- | ----- |
| 0   | 0   | 0     |
| 0   | 1   | 1     |
| 1   | 0   | 1     |
| 1   | 1   | 1     |

さて, いよいよこの論証が正しいかどうかを確認します. 論証が正しいとは, 前提 (P ∨ Q, Q → R, ¬Q) がすべて真になっているとき, 必ず結論 (P) も真になることだと言えそうです.
というわけで真理値表を書いて分析します.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
| P   | Q   | R   | P ∨ Q | Q → R | ¬Q  | P   |
| --- | --- | --- | ----- | ----- | --- | --- |
| 0   | 0   | 0   | 0     | 1     | 1   | 0   |
| 0   | 0   | 1   | 0     | 1     | 1   | 0   |
| 0   | 1   | 0   | 1     | 0     | 0   | 0   |
| 0   | 1   | 1   | 1     | 1     | 0   | 0   |
| 1   | 0   | 0   | 1     | 0     | 1   | 1   |
| 1   | 0   | 1   | 1     | 1     | 1   | 1   |
| 1   | 1   | 0   | 1     | 0     | 0   | 1   |
| 1   | 1   | 1   | 1     | 1     | 0   | 1   |

真理値表を見ると, 前提がすべて真になるのは下から 3 行目の場合のみで, このとき結論も真になっています. よってこの論証は正しいと言えます.
逆に, 前提がすべて 1 なのに結論が 0 になる組み合わせがある場合, その論証は正しくないと言えるわけです. 例えば「a^2=1 の答えは a=1 です. なぜなら a=1 を代入すると a^2=1 になるからです」という論証は正しくありません. P: a = 1, Q: a^2 = 1 として真理値表を書いてみると明らかになります.
このように, すべての論理式を同時に 1 にする真理値の割り当てが存在しない論理式の集合は矛盾していると言います.

真理値表は見慣れたものですが, 「→」については説明が必要かもしれません. 「P → Q」が 0 になるのは, P = 1, Q = 0 のときのみです.
これは「もし明日雨が降ったら延期します」という発言が嘘になるのは「明日雨が降った」かつ「延期しなかった」ときに限られるということを考えると, 妥当な気もします. もっとも, 日本語を正確に翻訳できるわけではないので, 多少現実的な感覚と乖離があるのは仕方ありません.

L を拡張して対象を広げる

L を手に入れたので, どんな論証でも記号化して真理値表を書けば正しさを確認できそうな気がしてきました. しかし, 次の論証はどうでしょう.

ゲーマーは負けず嫌いである
アリスはゲーマーである
よって, アリスは負けず嫌いである

これは正しい論証だとわかりますが, L ではその正しさを分析できません. 記号化しようとしても「P, Q, よって R」の形にしかできません. 「ゲーマーである → 負けず嫌いである」のようになんとか分解を試みても限界があります.
そこで「A は B である」という述語の形式を以下のように記号化します.

1
2
3
Px: x はゲーマーである
Qx: x は負けず嫌いである
a: アリス

さらに, 上記の 1 は特定の誰かというわけではなく, ゲーマーならばみんな負けず嫌いであるという内容です. この「みんな」というのを以下のような記号で表します.

1
2
どんな x に対しても (Px → Qx)
∀x(Px → Qx)

∀は All の A に由来していて, 全称記号と言います. これらの記号を用いて, 上記の論証は以下のように記号化できます.

∀x(Px → Qx)
Pa
よって, Qa

「¬∀x(Px → Qx)」という記号の意味は, 日本語で言うとどうなるでしょう. 「すべてのゲーマーが負けず嫌いであるというわけではない」, つまり負けず嫌いでないゲーマーもいるという意味です.
この「~も存在する」を∃という記号を使って表すことにします (Exist の E から来ていて, 存在記号と呼ばれます).
このように, 述語を取り入れたバージョンの L を MPL と名付けます (Monadic Predicate Logic. Monadic の意味は後でわかります).

さて, MPL では論証の分析をどのように行えば良いでしょうか.
論理式の集まりが矛盾しているかどうか判定するタブローの方法という便利なものがあります. タブローの方法とは, 前提がすべて真というところから出発して, 前提が真であるならば真でなければならない論理式を書き連ねていくことで, 最終的に前提と結論すべてを真にできるかどうかを判定するアルゴリズムです.

例として次の式が矛盾しているかどうか (=同時に 1 になることがあり得ないか) を判定してみます.

P ∧ Q
¬P ∨ ¬Q

P, Q のどの 01 の組み合わせでも 1, 2 両方が 1 になることはないので, この 2 つの式は矛盾していると言えそうです. これをタブローの方法で確認してみます.

1
2
3
4
5
6
7
8
 P ∧ Q
¬P ∨ ¬Q
--------
   P    (P ∧ Q: P=1 and Q=1)
   Q
  / \
 ¬P ¬Q  (¬P ∨ ¬Q: ¬P=1 or ¬Q=1)
 X   X  (すでに P, Q なので¬P, ¬Q は矛盾)

まず最初に論理式を書き, その後∧や∨の規則に従って論理式を分解していきます. 最終的にすべての枝に X が付けば矛盾です.
逆に一つでも X が付かない枝があれば, その枝ではどの論理式も 1 にできるということなので矛盾ではありません.

タブローの方法を使って論証が正しいことを確認するには, 結論を否定して矛盾することを示せばよいです (背理法ですね).
アリスが負けず嫌いであることを確認するには, 次の論理式から出発します.

∀x(Px → Qx)
Pa
¬Qa

1
2
3
4
5
6
7
8
 ∀x(Px → Qx)
    Pa
   ¬Qa
-------------
 Pa → Qa  (∀x(Px → Qx))
   / \
¬Pa   Qa  (Pa → Qa: Pa=0 or Qa=1)
 X     X  (すでに Pa, ¬Qa なので¬Pa, Qa は矛盾)

∀x というのはすべての x について当てはまるという意味なので, 当然 a についても当てはまります. そのため「∀x(Px → Qx)」の一例として「Pa → Qa」も成り立っていると言えます.

MPL のさらなる拡張

拡張は更に続きます.

マリンバはパーカッションである
ということは, マリンバ奏者はパーカッショニストである

この論証は明らかに正しいですが, MPL で正しさを分析するためにはマリンバとマリンバ奏者という関係を記号化する必要がありそうです.
これは「Pxy: x は y を演奏する」という記号を導入すると, 以下のように表せます.

∀x(Mx → Px)
∀x((Hx ∧ ∃y(Qxy ∧ My)) → (Hx ∧ ∃y(Qxy ∧ Py)))

突然複雑になりましたが「マリンバ奏者」を以下のように記号化しています.

「マリンバ奏者」 = 「x は人である ∧ x はマリンバを演奏する」
「x はマリンバを演奏する」 = ∃y(Qxy ∧ My)
「マリンバ奏者」 = Hx ∧ ∃y(Qxy ∧ My)

さらに次のような例はどうでしょう.

この大会の唯一の優勝者はトロフィーを手にした
アリスはこの大会の優勝者である
アリスはトロフィーを手にした

これは「唯一の」という点がポイントで, 同一性を表す記号 (a=b) を導入することで表現できるようになります.

このように, 最初に作った人工言語を徐々に拡張して扱う対象を広げていくのが本書の大筋です.
この記事で紹介した流れでは, L の文法, 論証の妥当性, L の完全性 (=L でどんな論理式でも表せるか), 矛盾といったことを曖昧にしか説明していません. 実際には厳密な定義や証明がつけられていて,

L の式は一通りにしか解釈できないのか? 別の読み方が生まれてしまわないか
述語論理 MPL における真理値の割り当てとはどのようなものか? ∀などをどう扱うか
タブローの方法は正しいのか

と言ったようなことが証明の題材になっています. 「L の文法規則に従うと, あらゆる論理式の ( と ) の数は一致する」という当たり前に思えるようなものでもちゃんと証明が書かれていて, 練習になります (私はそれほど興味を惹かれなかったので, 面白そうな証明以外は飛ばし読みしてしまいましたが).

最初は日常生活に根ざした例を扱うところから出発して, 抽象化と証明によって一歩ずつ構築を進めていくという流れは面白いです.
もともと論証の正しさや矛盾といったことを厳密に扱うことを目標としていたのに, いつしか抽象化を重ねてどんな長さの論理式をも対象にできるようになったり, L 自体が興味深い研究対象になったりするところに奥深さを感じました.

シンタックスの視点から論理学を見る

これまで紹介した内容は, それぞれの論理結合子 (∧や→など) にどのような意味があるかを考えた上で話を進めていました. それに対して, 結合子は意味を持たないただの記号だと考えて, 純粋に式の形のみに注目する立場もあります. それぞれセマンティクス (意味論), シンタックス (構文論) と呼ばれています.

シンタックスの立場では, 最初に絶対に正しいと思えるようなトートロジー(常に真になる論理式) と, トートロジーを変形して別のトートロジーを作り出すための変形規則を設定します. この出発点と変形規則を合わせて公理系と言います.
本書で主に扱われる公理系 APL(Axiomatic system for Propositinal Logic) は以下のようなものです. A が出発点, R が変形規則です.

1
2
3
4
A1. A → (B → A)
A2. (A → (B → C)) → ((A → B) → (A → C))
A3. (¬B → ¬A) → ((¬B → A) → B)
R1. A と A → B から B を引き出して良い

この公理系のもとでは「P → P」の証明は以下のようになります.

1
2
3
4
5
1. P → ((P → P) → P)                                A1
2. (P → ((P → P) → P)) → ((P → (P → P)) → (P → P))  A2
3. (P → (P → P)) → (P → P)                          1, 2 から R1 より
4. P → (P → P)                                      A1
5. P → P                                            3, 4 から R1 より

「P → P」なんて当たり前だと思うかもしれませんが, それはセマンティクス的な見方です. シンタックスでは記号の意味は考えないので, 公理系から「P → P」が導出されるのは当たり前ではありません.

このようにちょっとした証明でもかなり大変ですが, 実は自然演繹という便利な方法があります. これは前提から結論を一歩ずつ引き出す方法です. タブローの方法は与えられた論証が矛盾か妥当か評価するものでしたが, それに対して自然演繹は前提から結論を導くという手続きを構築する方法です.
例として, 「P → (Q → R) から Q → (P → R)」を導出する過程は以下のようになります.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
| P → (Q → R) Prem
|---------------------
| | Q Prem
| |-------------------
| | | P Prem
| | |-----------------
| | | P → (Q → R) Reit
| | | Q → R →elim
| | | R →elim
| | P → R →intro
| Q → (P → R) →intro

一番上に仮定を書きます. Q を仮定すると…(中略)…「P → R」ということが導出される, よって「Q → (P → R)」というような流れです.

自然演繹によって導出されたものも公理系での証明と同等に扱ってよいという定理があるので, シンタックス的論理学において自然演繹をかなり有用です. そして, 一度証明されたトートロジーは別の証明にも使って良いので, だんだん使えるトートロジーが増えていくことになります.

非古典論理という世界があるらしい

本書で主に扱われているのは古典論理と呼ばれる分野です. 古典と言っても古いという意味はなく, 1900 年頃にまとめられた論理学の基本となる体系のことを指します.

非古典論理を置き換える, 新たな論理体系が考案されています. 例えばすべての論理式が真か偽のどちらかの値しか取らないという点に疑問を投げかけて生まれたファジー論理があります. 真理値はもはや 0 か 1 ではなく, その中間の値も取る連続した値になります.
確かに現実では真偽の区別が微妙なものもあります. 例えば「重い」の基準は曖昧です. 50kg 以上なら重い, 50kg 未満なら重くないなどとすることもできますが, では重いものを 0.1g 減らしただけで重くなくなるのかというと, そうではない気がします.
すべての人はハゲであることを証明する有名な帰納法の証明も, このファジー論理のもとでは間違っていると言えるようになります (髪が 0 本の人はハゲである, ハゲの人に髪を 1 本増やしてもハゲである, よって髪が何本あってもハゲであるというやつ).

古典論理を置き換えるのではなく拡張しようとする立場もあります. 代表的なものは様相論理で, 「必ず~である」を意味する演算子□と「~が可能である」を意味する演算子◇を導入したものです. 他にも述語を関数化に拡張した言語 FOL(First-Order Logic) や, FOL を拡張して述語を量化することを認める第 2 階の論理があります.

古典論理だけでも消化しきれていない身からすると次々と新たな論理体系が出てきてオーバーフローという感じですが, さらに論理学の学びを深めていく際には参考になりそうです.

結び: 論理学とプログラミング

読んでいる途中, 論理学とプログラミングには関係がありそうだと思いました.
真理値表は見慣れたものですし, 他にもいくつかのアナロジーを思いつきました.

シンタックス的論理学で使える規則を証明して増やす vs. プログラムで新たな関数を定義して演算子を増やす
述語を量化して扱う第 2 階の論理 vs. 関数を変数として扱う高階関数

本書では「機械もすなる論理学」という章でタブローの方法が紹介されています.
タブローの方法はもともとコンピュータで実行することを念頭に置かれたアルゴリズムのようですし, 論証の妥当性を機械的に判定するというような試みは歴史が長いのかもしれません.
このあたりでプログラミング言語の　ML　を思い出しました. 当時 (OCaml に入門したとき) は証明のためのプログラミング言語と聞いてもイメージが付来ませんでしたが, 本書を読んだ今となっては, そういう発想が出てくるのは自然なことに思えます.

そもそも現代のコンピュータ自体がブール演算を基礎とした論理コンピュータなわけですから, 論理学とプログラミングに関連があるのは当たり前かもしれません.
おそらくプログラムを分析するための体系を作って, 正しさを検証したり完全性を調べたりする分野があるのではないかと思います.

これまで論理学というものを学んだことはなかったが, これで入口に立つことはできたのではないかと思います.
論理学を学んでも論理的に物事を考えられるようになるとかいうわけではなさそうですが, 言語を作って抽象的な記号の操作をするという営みには神秘的な雰囲気を感じます. 次のステップとしては, プログラミングと論理学の関係について勉強してみようと思います.

導入#

印象に残った点#

論理学を「つくる」とはどういうこと？#

L を拡張して対象を広げる#

MPL のさらなる拡張#

シンタックスの視点から論理学を見る#

非古典論理という世界があるらしい#

結び: 論理学とプログラミング#

導入