1. 証明とは何か
論証とは、ある結論がいくつかの前提から導かれるという主張です。証明とは、その主張に決着をつけるもの、つまり誰もが一行ずつ読んで納得できる有限で検証可能な対象であり、あなたの言葉を信じる必要はありません。証明の要点は説得力ではありません。よい演説にも説得力はあります。要点は、その一歩一歩が他のようにはなりえなかったということです。
これは聞こえるより厳しい要求です。「雨が降っている、だから地面は濡れている」は理にかなった言い方ですが、雨と地面についてあなたが知っていることに寄りかかっています。形式論理はそれを取り払い、より狭い問いを立てます。文の形だけを見て、前提が真で結論が偽になる道が一つでもあるか。もし一つもなければ論証は妥当であり、証明とはなぜ一つもないのかの記録です。
このガイドは、その記録を作る一つの方法、すなわち真理の木とも呼ばれる意味論的タブローの方法を扱います。計算機に論証を入力したとき、このサイトが使っているのがこの方法です。一度たどってしまえば、ペン一本で紙の上の論証を検査できるようになります。
2. 妥当であること、そしてそれをどう知るか
論証を帰結記号で書きます。左に前提、右に結論です。p → q, ¬q ⊨ ¬p という主張は、条件法とその後件の否定から前件の否定が導かれる、と述べています。帰結記号はもう一つの結合子ではありません。両側の論理式についての主張であり、正しいか誤っているかのどちらかです。
妥当性の定義は、その検査法をそのまま指し示します。変数への真と偽の割り当てをすべてたどり、前提をすべて真にして結論を偽にするものがあるかを見ればよいのです。真理表がしているのはこれで、変数が二つ三つならまったく問題ありません。困るのは、表が 2ⁿ で膨らむことです。変数が十個なら千行、二十個なら百万行必要になり、しかも表はどの行が効いたのかを何も語りません。
タブローは同じ問いに反対側から取り組みます。あらゆる可能性を並べて悪いものを探すのではなく、悪いものが存在すると仮定してそれを組み立てようとします。その試みが取りうるどの経路でも矛盾に崩れるなら、そのような割り当ては存在せず、論証は妥当です。試みが成功すれば、組み上がったものがそのまま読み取れる反例です。
3. タブローの方法
タブローは符号つき論理式の木です。各行は先頭に T か F を置いた論理式で、符号はその枝がその論理式について何を仮定しているかを示します。真理値が何であるかではなく、論証が破綻するためには何でなければならないか、です。方法全体は四つの手順です。
- 各前提を T つきで書きます。論証の前提がすべて成り立つと仮定しているのです。
- 結論を F つきで書きます。それでも結論は破綻すると仮定しているのであり、これが反駁しようとしている仮定です。
- まだ原子でない行を一つ取り、その主結合子と符号に対応する規則を適用し、規則が生むものをその行を通るすべての枝の末尾に加えます。
- 同じ論理式 A について T A と F A の両方を持った時点で、その枝を閉じます。すべての枝が閉じたとき、または分解すべき行がなくなったときに終了します。
この繰り返しに機転も戦略の選択も要りません。各行に対応する規則はちょうど一つで、どの順に適用しても同じ判定になります。だから機械にもできるのであり、だから機械がやった結果を信頼できるのです。
4. 規則
結合子ごと、符号ごとに規則が一つずつ、合わせて十あります。規則は二種類に分かれ、その違いこそタブローが一覧ではなく木である理由のすべてです。α 規則は複数のことが同時に成り立たねばならないと述べるので、結果を枝に沿って積み上げます。β 規則は二つのうち一方が成り立たねばならないと述べるので、枝を二つに分け、それぞれの場合を別々の道に進ませます。
| 行 | 生成 | 形 |
|---|---|---|
T ¬A | F A | 積み上げ |
F ¬A | T A | 積み上げ |
T (A∧B) | T A, T B | 積み上げ |
F (A∧B) | F AF B | 分岐 |
T (A∨B) | T AT B | 分岐 |
F (A∨B) | F A, F B | 積み上げ |
T (A→B) | F AT B | 分岐 |
F (A→B) | T A, F B | 積み上げ |
T (A↔B) | T A, T BF A, F B | 分岐 |
F (A↔B) | T A, F BF A, T B | 分岐 |
どの規則も、その結合子の真理条件を逆から読んだだけのものです。連言は両辺が真のときだけ真なので、T (A ∧ B) は T A と T B を積み上げます。連言は少なくとも一方が偽なら偽ですが、論理式はどちらかを言わないので、F (A ∧ B) は両方を試すほかありません。だから分岐します。選言では同じ非対称が逆向きに働き、条件法が偽であるとは前件が成り立ち後件が破綻したということ、含意が壊れる唯一の場合です。
規則が決してしないことに注目してください。規則は論理式を作り出しません。規則が生むものはすべて、元の行の一部分です。この性質、すなわち部分論理式性こそが方法を有限にしており、後ほど改めて触れます。
5. 枝を閉じる
枝は一本の推論の筋道です。根から葉まで読めば、仮定の完全な一組が得られます。枝が閉じるのは、それらの仮定が真っ向から矛盾するとき、つまり同一の論理式について T A と F A の両方を担っているときです。A がどれほど複雑でも、二つの行がどれほど離れていても関係ありません。ある論理式が真でも偽でもあることを枝が要求するなら、それを満たすものは何もありません。
閉じた枝には × を付け、閉じた二つの行を書き添えて、その枝の作業をやめます。もともと不可能だった仮定から、これ以上学べることはありません。
すべての枝が閉じればタブローは閉じており、それが証明です。出発点の想定、すなわち前提はすべて真で結論は偽である、という想定が、取りうるどの経路でも矛盾に至ることを示しているからです。経路が残らなかった以上そのような割り当ては存在せず、論証は妥当です。これは背理法を、どの場合も見落とせないように並べたものです。
6. 一行ずつたどる証明
modus tollens、p → q, ¬q ⊨ ¬p を取り上げます。行 1 と 2 は真と仮定した前提です。行 3 は偽と仮定した結論で、結論が ¬p である以上、それを偽と仮定することは p を真と仮定することであり、行 5 がそれを記録しています。行 4 は行 2 に否定規則を適用したもので、¬q が真なら q は偽です。結合子が残っている行は行 1 の条件法だけで、これは β 規則なので、木は二股に分かれます。
- 1真: p→q前提
- 2真: ¬q前提
- 3偽: ¬p結論の否定
- 4偽: q2 行目から
- 5真: p3 行目から
- 6偽: p1 行目から
枝が閉じました: 6 行目は 5 行目と矛盾します。
- 7真: q1 行目から
枝が閉じました: 7 行目は 4 行目と矛盾します。
閉じた枝
左の枝は、前件が破綻したから条件法が成り立ったと仮定します。しかし行 5 ですでに p は真なので、枝は自己矛盾を起こして閉じます。右の枝は、後件が真だったから成り立ったと仮定します。しかし行 4 ですでに q は偽なので、こちらも閉じます。
両方の枝が閉じたので、¬p が偽のまま p → q と ¬q を真にする方法はありません。論証は妥当であり、その理由がこの木です。証明が雨にも地面にも、p と q が何を表すかにも一切触れていないことに注目してください。触れる必要がなかったのです。
7. 枝が開いたまま残るとき
すべての論証が妥当なわけではなく、そこでこの方法は真価を発揮します。ある枝を、もう何も分解できなくなるまで、つまり原子と否定された原子しか残らなくなるまで進めても閉じないなら、その枝は飽和しており開いています。早く切り上げたから閉じなかったのではありません。試すべきことがもう残っていないのです。
開いた枝は「妥当でない」という判定以上のものです。その原子の符号を読み取れば割り当てが得られます。T の付いた原子は真、F の付いた原子は偽です。この割り当ては前提をすべて真にし結論を偽にします。それこそ反例そのものです。論理学者はこれを反モデルと呼びます。これは「なぜだめなのか」への具体的な答えであって、拒絶ではありません。
後件肯定、p → q, q ⊨ p が定番の例です。そのタブローは p を偽、q を真として枝を開いたまま残します。条件法が成り立ち後件も成り立つのに前件は成り立たない、という状況です。この一つの割り当てだけで論証は反駁されます。
8. なぜ必ず終わるのか
どの規則も論理式をその部分論理式に置き換え、部分論理式は元の論理式より必ず短くなります。したがってどの枝も永遠に伸びることはできません。各段階はもとの論証の断片からなる有限の梯子を降りていき、梯子には底があります。やがて枝の各行は原子かその否定になり、することがなくなります。
これは希望ではなく本物の保証です。この方法が命題論理の決定手続きであることを意味します。どんな論証にかけても停止し、閉じた木か開いた枝のどちらかを返し、肩をすくめて終わることはありません。このサイトの証明器はさらにノード数の上限を設けていますが、それは病的な論理式がブラウザのタブを食い尽くすのを防ぐためだけであり、数学そのものにそんな制限は要りません。
9. ほかの証明体系
タブローはいくつかある証明体系の一つで、反駁の形をしたものです。失敗を排除することで働きます。自然演繹は逆向きに、modus ponens や条件証明といった規則で前提から結論へ前向きに組み上げていき、数学者が散文で論じるやり方にずっと近く読めます。自然演繹の証明はたいてい短くなりますが、見つけるにはたいてい多くの着想が要ります。
シークエント計算は帰結記号そのものを形式化し、帰結の主張を対象として扱うため、証明についての事柄を証明したいときの定番の道具になります。導出原理はすべてを節と単一の規則に還元します。読んで面白いものではありませんが実行は非常に速く、自動定理証明器や SAT ソルバーの多くはこれを土台にしています。
どの命題論証が妥当かについては、いずれの体系も一致します。異なるのは証明の見た目と、何が見つけやすいかです。学ぶうえでいちばん親切なのはタブローです。証明に失敗しても行き止まりではなく、反例が手に入るからです。
10. 練習
この方法を学ぶ最短の道は、実際に走らせてみることです。⊨、⊢ または |= を使って計算機に論証を入力すると、真理表の隣にタブローが描かれるので、木と行を突き合わせられます。そのうえで、答えを見る前にいくつかの証明を紙の上でやってみてください。