プログラマー向けの（？）数理論理学（２）証明と推論規則と仮定

プログラマー向けというか、数理論理学の枠組みをプログラムとして実装したい人とか形式化数学をやりたい人向けの記事かもしれません（形式化数学についてはこちらの記事もどうぞ）。

前回の記事

プログラマー向けの（？）数理論理学（１）数学的言明

証明

前回説明したように、数学における全ての主張は数学的言明として表されましたが、その主張に正当性を与えるのが数学的言明に対する証明の役割です。

つまり、証明とは数学的言明が何故正しいのかという理由を述べたものです。

たとえば、「4は偶数である」という言明の証明を考えると下のようになります。

• 偶数とは2で割り切れる整数のことである。
• 4は整数である。
• 4は2で割り切れる。
• つまり、4は2で割り切れる整数である。
• ゆえに、4は偶数である。

これは「4は偶数である」ことの理由を正しく述べているため、「4は偶数である」という言明の証明と言える訳です。

そして、この証明が与えられたことによって「4は偶数である」という言明が正しいものであると主張することができる訳です。

そして、証明が与えられた数学的言明を定理と呼びます。

それでは、証明はどのような形で与えれば良いのでしょうか？

上の証明をよく見ていただきたいのですが、上の証明のそれぞれの文はそれそのものが何らかの数学的言明となっていることが分かります。

たとえば、「偶数とは2で割り切れる整数のことである」という文は正しいか正しくないかが明確に判断できる数学的な文ですので、数学的言明です。「4は整数である」という文や「4は2で割り切れる」という文も同様です。

また、上の証明の最後の文は「4は偶数である」と言っていて、これは証明したかった数学的言明そのものです。

そして、上の証明を構成する数学的言明は全て正しい数学的言明です。

これらのことから下のことが分かります。

証明というのは正しい数学的言明を何らかの法則で並べることによって最終的に証明したい数学的言明を導き出す作業である。

証明というものの大部分が解明されました。

しかし、最後に残った問題が数学的言明をどのような法則で並べれば（正しい）証明になるのかということです。

推論規則

そこでもう1度上の証明を眺めてみましょう。特に2行目から4行目に注目してみましょう。

• 4は整数である。
• 4は2で割り切れる。
• つまり、4は2で割り切れる整数である。

この証明の一部の最後の行「4は2で割り切れる整数である」は何故正しいと言えるのでしょうか？

それは最初の行の「4は整数である」と次の行の「4は2で割り切れる」が正しいからです。

つまり、この2つのことが正しいと言えているからこそ「4は2で割り切れる整数である」ということが正しいと言える訳です。

ですから、証明というのは既に正しいと分かっている数学的言明から別の正しい数学的言明を導き出す作業を繰り返し、最終的に証明したい数学的言明を導き出すという作業であり、これにより証明したかった数学的言明も正しいと言えることになるということです。そして、このような作業を推論と言います。

また、上の3行から成る証明の一部を一般化すると次のことが言えます。

言明Pが正しいと証明されており、言明Qも正しいと証明されている時、言明P ∧ Qも正しいと言える。

実は私たちが証明を行う際にはこのような法則を暗黙的に使用しており、このような法則のことを推論規則と言います。

普段数学をする時には推論規則は暗黙的に使用しているものですが、勿論どのような推論規則を使っているか明示する形で証明を記述することもできます。

推論規則にも幾つか種類があり、どのような推論規則を使って証明を行うかには流派があるのですが、この連載では自然演繹という流派の推論規則を採用することにします。

たとえば、自然演繹の場合、含意が関連する推論規則には下の2つのものがあります。

• 含意除去規則・・・命題Pと命題P → Qの両方が正しいと証明されている時、命題Qも正しいと言える。
• 含意導入規則・・・命題Qが正しいと証明されている時、命題P → Qも正しいと言える。ただし、命題P → Qの証明からは仮定Pが落ちる。

上の1つ目の推論規則が含意除去規則と呼ばれるのは含意を含む数学的言明から含意を含まない数学的言明を導き出すことができるからです。

また、上の2つ目の推論規則が含意導入規則と呼ばれるのは含意を含まない数学的言明から含意を含む数学的言明を導き出すことができるからです。

しかし、含意除去規則に関しては理解できるかと思いますが、含意導入規則を理解するためには自然演繹の「仮定」という概念について知らなければなりません。

仮定

数学的言明の証明を行う際には仮定というテクニックを使うことができる場合があります。

仮定という概念を知るために下のような(P → (Q → R)) → (Q → (P → R))という言明の証明を見てみましょう。

• (P → (Q → R))が正しいと仮定する。
• Pが正しいと仮定する。
• すると、Pが正しく、(P → (Q → R))も正しいので、Q → Rである。
• Qが正しいと仮定する。
• すると、Qが正しく、Q → Rも正しいので、Rである。
• すると、Pが正しいと仮定していたので、P → Rである。
• すると、Qが正しいと仮定していたので、Q → (P → R)である。
• すると、(P → (Q → R))が正しいと仮定していたので、(P → (Q → R)) → (Q → (P → R))である。

このように、数学的言明を仮定すると、その数学的言明は証明済みの数学的言明と同じように証明において推論規則の適用の際に使用することができるようになります。

つまり、仮定した数学的言明は既に正しいと証明されているものと見做すことができます。

ただし、1つ非常に重要なことがあって、それは仮定は最終的には落とさなければならないということです。

たとえば、上の証明の5行目では「Rである」ことが主張されていますが、これは無条件に「Rである」と主張している訳ではありません。「Rである」という言明は(P → (Q → R))、P、Qという3つの言明を仮定して得られたものですので、あくまでも「この3つの仮定の下ではRである」ということが主張されているに過ぎません。

ですから、「Rである」という言明の証明にはなっていません。

正しい証明と言えるためには仮定が全て取り去られていなければならないのです。

証明の過程で仮定を取り去るには仮定を取り去ることのできる推論規則を使用します。

たとえば、上の含意導入規則は仮定を取り去ることのできる推論規則の例であり、上の証明の最後の3行では正にこの含意導入規則を適用して仮定を落とし、最終的に証明したかった言明である(P → (Q → R)) → (Q → (P → R))を導いています。

このように、自然演繹では推論規則の他に「仮定を置く」という機構が用意されています。また、推論規則の中には仮定を取り去ることのできる能力を有するものが幾つか存在します。

自然演繹では仮定を置いたり落としたりしながら推論規則を使用して様々な数学的言明の証明を行います。

自然演繹の推論規則は上で挙げた2つ以外にも幾つもありますが、このままでは説明ばかり長くなってしまいますので、今回は数理論理学の領域の説明はここまでにして、ここからは証明や仮定や推論規則などのプログラムにおける実装について話したいと思います。その他の推論規則については何回か後の記事で取り上げます。

証明の取り扱い（プログラム上）

ここから下は証明をプログラムでどう実装するかという話なので、プログラミングに興味のない方は飛ばして次の記事に進んでください。

---

プログラムにおいて証明という概念を上手く取り扱うのに必要なのは「仮定を置くことも（不完全な）証明である」、「推論規則の適用も証明である」という気付きです。

どういうことかというと、たとえば、「Pであると仮定する」ということは「Pである」という言明に対する不完全な証明を作ったと見做すことができるということです。

証明が不完全なものになってしまうのは仮定が落ちていないからです。「Pである」と仮定すると「Pである」という仮定が導入されることになるので仮定が落ちていない状態となります。したがって、この証明は不完全なものとなります。

また、たとえば、含意除去規則を使って既に証明されているP → QとPという言明からQという言明を導くのは言明P → Qに対する証明と言明Pに対する証明を材料として言明Qに対する証明を作ったと見做すことができます。

このように、仮定を置くという操作や推論規則の適用という操作はそれ自体証明の一種であると考えることができ、プログラム的には証明を表すオブジェクトを作成する操作と考えることができます。

そして、前回数学的言明に対して行ったのと同様に、仮定を置くという操作や推論規則の適用という操作をコマンド化して、ユーザーに自由にコマンドを入力してもらうことにより証明の作成を自由に行ってもらうことができるようにすることができます。

このような方針で証明というものをプログラムとして実装することにしましょう。

仮定

まずは仮定を置くという操作を仮定という種類の証明を作る操作として実装します。

function create_premise (p) {
  if (p.type !== 'prop') {
    throw new Error('not prop.');
  }

  return {
    type: 'proof',
    subtype: 'prem',
    premises: [p],
    conclusion: p,
    sub: p
  };
}

仮定を置くという操作はあらゆる数学的言明に対して行うことができますので、引数として数学的言明を表すオブジェクトを取ります。

そして、これを材料にして証明を表すオブジェクトを作成します。

証明を表すオブジェクトのtypeプロパティの値はproofということにします。

また、証明を表すオブジェクトの中でも仮定を表すオブジェクトのsubtypeプロパティの値はpremということにします。

証明を表すオブジェクトにはpremisesプロパティとconclusionプロパティを指定します。

premisesプロパティにはオブジェクトが表している証明の全ての（まだ落とされていない）仮定を格納するものとします。仮定は複数である場合もありますので、配列として格納することにします。

conclusionプロパティはオブジェクトがどのような数学的言明の証明を表しているのかを示すものとします。つまり、conclusionプロパティには証明が対象としている数学的言明そのものを格納します。なお、証明が対象としている数学的言明のことを結論と言います。

ですから、pという仮定を置いただけの（不完全な）証明を表すオブジェクトのpremisesプロパティの値は[p]となり、conclusionプロパティの値はpとなります。つまり、これは仮定がpであり、結論がpであるような証明です。

含意除去規則

次に含意除去規則を適用する操作を特定の形の証明を作る操作としてcreate_implication_elimination関数において実装します。

function create_implication_elimination (pr1, pr2) {
  if (pr1.type !== 'proof') {
    throw new Error('not proof.');
  }
  if (pr2.type !== 'proof') {
    throw new Error('not proof.');
  }

  if (pr2.conclusion.subtype !== 'imp') {
    throw new Error('not apply.');
  }
  if (!equal(pr1.conclusion, pr2.conclusion.sub1)) {
    throw new Error('not apply.');
  }

  var premises = [];
  gather_unique_obj(premises, pr1.premises);
  gather_unique_obj(premises, pr2.premises);
  var conclusion = pr2.conclusion.sub2;

  return {
    type: 'proof',
    subtype: 'imp_elim',
    premises: premises,
    conclusion: conclusion,
    sub1: pr1,
    sub2: pr2
  };
}

function gather_unique_obj (outs, ins) {
  for (var i = 0; i < ins.length; i++) {
    var f = true;
    for (var j = 0; j < outs.length; j++) {
      if (equal(ins[i], outs[j])) {
        f = false;
        break;
      }
    }
    if (f) {
      outs.push(ins[i]);
    }
  }
}

function equal (obj1, obj2) {
  if (obj1.type !== obj2.type) {
    return false;
  }
  if (obj1.subtype !== obj2.subtype) {
    return false;
  }

  if (obj1.type === 'prop' && obj2.type === 'prop') {
    if (obj1.subtype === 'atom' && obj2.subtype === 'atom') {
      return obj1.index === obj2.index;
    }
    else if (obj1.subtype === 'neg' && obj2.subtype === 'neg') {
      return equal(obj1.sub, obj2.sub);
    }
    else if (obj1.subtype === 'conj' && obj2.subtype === 'conj') {
      return equal(obj1.sub1, obj2.sub1) && equal(obj1.sub2, obj2.sub2);
    }
    else if (obj1.subtype === 'disj' && obj2.subtype === 'disj') {
      return equal(obj1.sub1, obj2.sub1) && equal(obj1.sub2, obj2.sub2);
    }
    else if (obj1.subtype === 'imp' && obj2.subtype === 'imp') {
      return equal(obj1.sub1, obj2.sub1) && equal(obj1.sub2, obj2.sub2);
    }
    else if (obj1.subtype === 'equiv' && obj2.subtype === 'equiv') {
      return equal(obj1.sub1, obj2.sub1) && equal(obj1.sub2, obj2.sub2);
    }
    else {
      throw new Error('not supported object.');
    }
  }
  else if (obj1.type === 'proof' && obj2.type === 'proof') {
    if (obj1.premises.length !== obj2.premises.length) {
      return false;
    }
    for (var i = 0; i < obj1.premises.length; i++) {
      var f = false;
      for (var j = 0; j < obj2.premises.length; j++) {
        if (equal(obj1.premises[i], obj2.premises[j])) {
          f = true;
          break;
        }
      }
      if (!f) {
        return false;
      }
    }
    return equal(obj1.conclusion, obj2.conclusion) && obj1.dindex == obj2.dindex;
  }
  else {
    throw new Error('not supported type.');
  }
}

上で述べた含意除去規則（下に再掲）を忠実に実装しています。

• 含意除去規則・・・命題Pと命題P → Qの両方が正しいと証明されている時、命題Qも正しいと言える。

第1引数として上の規則における命題Pの証明を表すオブジェクトを取り、第2引数として命題P → Qの証明を表すオブジェクトを取ります。

そのため、第2引数の証明を表すオブジェクトの結論を表すオブジェクト（上の規則における命題P → Qを表す）のsubtypeプロパティはimpでなければなりません。

また、第1引数の証明を表すオブジェクトの結論を表すオブジェクト（上の規則における命題Pを表す）と第2引数の証明を表すオブジェクトの結論を表すオブジェクトのsub1プロパティの値（上の規則における命題P → Q中の命題Pを表す）は同じでなければなりません。

このチェックを行うためにequal関数を実装し、使用しています。

equal関数は第1引数と第2引数として比較する2つのオブジェクトを取り、それぞれのオブジェクトが数学的言明を表すオブジェクトである場合にはそれぞれのオブジェクトの材料が同じであるかチェックし、証明を表すオブジェクトである場合には仮定と結論とdindexプロパティの値が同じであるかチェックしています（dindexプロパティについては後述）。

続いてcreate_implication_elimination関数では新たに作成する証明を表すオブジェクトの仮定と結論を作成しています。

仮定は第1引数と第2引数の証明を表すオブジェクトの仮定を併せたものとなります。

ただし、重複は取り除かなければなりませんので、そのためにgather_unique_obj関数を実装し、使用しています。

そして、結論は第2引数の証明を表すオブジェクトの結論を表すオブジェクトのsub2プロパティの値（上の規則における命題P → Q中の命題Qを表す）となります。

そして、この仮定と結論を使って新たな証明を表すオブジェクトを作成しています。

なお、含意除去規則の適用を表すオブジェクトのsubtypeプロパティの値はimp_elimとすることにしました。

含意導入規則

次に含意導入規則を適用する操作を特定の形の証明を作る操作としてcreate_implication_introduction関数において実装します。

function create_implication_introduction (pr1, pr2, dindex) {
  if (pr1.type !== 'proof') {
    throw new Error('not proof.');
  }
  if (pr2.type !== 'proof') {
    throw new Error('not proof.');
  }
  if (pr2.subtype !== 'prem') {
    throw new Error('not premise.');
  }

  var premises = [];
  for (var i = 0; i < pr1.premises.length; i++) {
    if (!equal(pr1.premises[i], pr2.conclusion)) {
      premises.push(pr1.premises[i]);
    }
  }
  var conclusion = create_implication(pr2.conclusion, pr1.conclusion);

  var npr2 = shallowcopy(pr2);
  npr2.dindex = dindex;
  replace(pr1, pr2, npr2);
  if (equal(pr1, pr2)) {
    pr1 = npr2;
  }

  return {
    type: 'proof',
    subtype: 'imp_intro',
    premises: premises,
    conclusion: conclusion,
    sub1: pr1,
    sub2: npr2
  };
}

function shallowcopy (obj) {
  if (obj.type === 'proof') {
    if (obj.subtype === 'prem') {
      return {
        type: 'proof',
        subtype: 'prem',
        premises: obj.premises,
        conclusion: obj.conclusion,
        sub: obj.sub
      };
    }
    else {
      throw new Error('not supported subtype.');
    }
  }
  else {
    throw new Error('not supported type.');
  }
}

function replace (obj1, obj2, obj3) {
  if (obj1.type === 'proof') {
    if (obj1.subtype === 'prem') {
      return;
    }
    else if (obj1.subtype === 'imp_elim' || obj1.subtype === 'imp_intro') {
      if (equal(obj1.sub1, obj2)) {
        obj1.sub1 = obj3;
      }
      else {
        replace(obj1.sub1, obj2, obj3);
      }
      if (equal(obj1.sub2, obj2)) {
        obj1.sub2 = obj3;
      }
      else {
        replace(obj1.sub2, obj2, obj3);
      }
    }
    else {
      throw new Error('not supported subtype.');
    }
  }
  else {
    throw new Error('not supported type.');
  }
}

上で述べた含意導入規則（下に再掲）を忠実に実装しています。

• 含意導入規則・・・命題Qが正しいと証明されている時、命題P → Qも正しいと言える。ただし、命題P → Qの証明からは仮定Pが落ちる。

第1引数として上の規則における命題Qの証明を表すオブジェクトを取り、第2引数として上の規則における仮定Pを表すオブジェクトを取ります。

そして、第3引数はちょっと特殊です。

含意導入規則は「仮定が落ちる」規則ですが、仮定を落とした際には落とした仮定を識別できるようにする必要があります。

これは証明全体において識別できなければなりませんので、引数として一意な番号を受け取ることにします。そして、それをdindexと呼ぶことにしました。

ですから、第3引数というのはこの規則の適用によって落とされる仮定を表すオブジェクトに付加される番号となります。

create_implication_introduction関数ではまず新たに作成する証明を表すオブジェクトの仮定と結論を作成しています。

仮定は第1引数の証明を表すオブジェクトの仮定から第2引数の仮定を表すオブジェクトの結論を取り除いたものとなります。

また、結論は第2引数の仮定を表すオブジェクトの結論を表すオブジェクト（上の規則における仮定Pを表す）と第1引数の証明を表すオブジェクトの結論を表すオブジェクト（上の規則における命題Qを表す）を材料として作成した含意を表すオブジェクト（上の規則における命題P → Qを表す）となります。

次にcreate_implication_introduction関数では第2引数の仮定を表すオブジェクトをコピーします。このためにshallowcopy関数を実装し、使用しています。

そして、コピーしたオブジェクトにdindexをdindexプロパティとして与えます。

このままでは第1引数の証明を表すオブジェクトに含まれるオブジェクトがコピー前のオブジェクトである可能性がありますので、オブジェクトの置換を行います。このためにreplace関数を実装し、使用しています。

また、第1引数の証明を表すオブジェクト自体がコピー前のオブジェクトそのものである可能性もありますので、その場合にはコピー後のオブジェクトに置き換えます。

そして、ここまでで作成したオブジェクトを使って新たな証明を表すオブジェクトを作成しています。

なお、含意導入規則の適用を表すオブジェクトのsubtypeプロパティの値はimp_introとすることにしました。

コマンドによる証明の作成

前回と同様に、単純なコマンドを呼び出すことで自由に証明を組み立てていけるようにしましょう。

そのためにはまずtohtml関数を下のように変更します。

function tohtml (obj) {
  if (obj.type === 'prop') {
    if (obj.subtype === 'atom') {
      return 'P' + '<sub>' + obj.index + '</sub>';
    }
    else if (obj.subtype === 'neg') {
      return '( ' + '￢' + tohtml(obj.sub) + ' )';
    }
    else if (obj.subtype === 'conj') {
      return '( ' + tohtml(obj.sub1) + ' ∧ ' + tohtml(obj.sub2) + ' )';
    }
    else if (obj.subtype === 'disj') {
      return '( ' + tohtml(obj.sub1) + ' ∨ ' + tohtml(obj.sub2) + ' )';
    }
    else if (obj.subtype === 'imp') {
      return '( ' + tohtml(obj.sub1) + ' → ' + tohtml(obj.sub2) + ' )';
    }
    else if (obj.subtype === 'equiv') {
      return '( ' + tohtml(obj.sub1) + ' ↔ ' + tohtml(obj.sub2) + ' )';
    }
    else {
      throw new Error('not supported subtype.');
    }
  }
  else if (obj.type === 'proof') {
    var premises = [];
    for (var i = 0; i < obj.premises.length; i++) {
      premises.push(tohtml(obj.premises[i]));
    }
    return premises.join(', ') + ' ├ ' + tohtml(obj.conclusion);
  }
  else {
    throw new Error('not supported type.');
  }
}

この関数では引数のオブジェクトが証明を表すオブジェクトである場合には証明の全ての仮定を,で結合し、これと証明の結論を├で結合したものを出力しています。

これにより、一目で証明の仮定と結論が分かるようになり、便利です。

そして、initialize_context関数を下のように変更します。

function initialize_context (context) {
	context.pindex = 0;
	context.dindex = 0;
	context.sindex = 0;
	context.ss = new Map();
}

新たにdindexプロパティの初期化を追加しました。

また、execute_command関数を下のように変更します。

function execute_command (context, command) {
  var cs = command.split(' ');

  if (cs[0] === 'prop') {
（省略）
  }
  else if (cs[0] === 'neg') {
（省略）
  }
  else if (cs[0] === 'conj') {
（省略）
  }
  else if (cs[0] === 'disj') {
（省略）
  }
  else if (cs[0] === 'imp') {
（省略）
  }
  else if (cs[0] === 'equiv') {
（省略）
  }
  else if (cs[0] === 'prem') {
    var objs = get_n_objects_from_args(context, 1, cs);
    var p = create_premise(objs[0]);

    add_object(context, p);

    return p;
  }
  else if (cs[0] === 'imp_elim') {
    var objs = get_n_objects_from_args(context, 2, cs);
    var p = create_implication_elimination(objs[0], objs[1]);

    add_object(context, p);

    return p;
  }
  else if (cs[0] === 'imp_intro') {
	context.dindex++;
    var objs = get_n_objects_from_args(context, 2, cs);
    var p = create_implication_introduction(objs[0], objs[1], context.dindex);

    add_object(context, p);

    return p;
  }
  else {
    throw new Error('not supported command.');
  }
}

仮定を置くためにpremコマンド、含意除去規則を適用するためにimp_elimコマンド、含意導入規則を適用するためにimp_introコマンドを追加しました。

これらのコマンドを前回実装した数学的言明を作るためのコマンドと一緒に使用することで、含意のみに関する数学的言明を証明することができるようになりました。

実際の証明の例

たとえば、上で述べた(P → (Q → R)) → (Q → (P → R))という言明と同形の(P1 → (P2 → P3)) → (P2 → (P1 → P3))という言明を証明するには下のようなコマンドを順番に実行します。

prop
prop
prop
imp 2 3
imp 1 4
prem 5
prem 1
imp_elim 7 6
prem 2
imp_elim 9 8
imp_intro 10 7
imp_intro 11 9
imp_intro 12 6

すると、順番に下のような数学的言明や証明を表すオブジェクトが作成され、最終的に上の数学的言明が証明されたことが分かります。

[1]P1
[2]P2
[3]P3
[4]( P2 → P3 )
[5]( P1 → ( P2 → P3 ) )
[6]( P1 → ( P2 → P3 ) ) |- ( P1 → ( P2 → P3 ) )
[7]P1 |- P1
[8]P1, ( P1 → ( P2 → P3 ) ) |- ( P2 → P3 )
[9]P2 |- P2
[10]P2, P1, ( P1 → ( P2 → P3 ) ) |- P3
[11]P2, ( P1 → ( P2 → P3 ) ) |- ( P1 → P3 )
[12]( P1 → ( P2 → P3 ) ) |- ( P2 → ( P1 → P3 ) )
[13] |- ( ( P1 → ( P2 → P3 ) ) → ( P2 → ( P1 → P3 ) ) )

これで含意のみに関する数学的言明は証明できるようになった訳ですが、このプログラムを証明を行うツールとして見た時、まだ機能が少な過ぎて、このまま実際の証明を行うのに使っていくのは面倒です。

そこで次回ではここまで作ってきたプログラムをウェブアプリ化し、幾つか便利な機能を追加することで、もう少し使いやすいものにしたいと思います。