プログラマー向けの（？）数理論理学（６）否定に関する推論規則 #JavaScript

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

なお、ソースコード全体はGitHubにあります。

https://github.com/pizyumi/rena

連載まとめ

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

否定に関する推論規則

今回は否定に関する3つの推論規則について説明します。

自然演繹の場合、否定に関する推論規則は下の3つとなります。

否定除去規則・・・命題Pと命題￢Pの両方が正しいと証明されている時、命題⊥も正しいと言える。
否定導入規則・・・命題⊥が正しいと証明されている時、命題￢Pも正しいと言える。ただし、命題￢Pの証明からは仮定Pが落ちる。
背理法（RAA）・・・命題⊥が正しいと証明されている時、命題Pも正しいと言える。ただし、命題Pの証明からは仮定￢Pが落ちる。

ここで⊥という見たことのない命題が出てきました。これは何でしょうか？

⊥というのは矛盾を表す特殊な命題です。

矛盾というのは任意の命題Pとその否定￢Pが同時に成り立っている状態です。

つまり、「Pである」ということと「Pでない」ということが同時に成り立っているということであり、正に矛盾している状態です。

そして、この「矛盾している」という状態を1つの数学的命題として捉えたのが⊥です。

ですから、上の否定除去規則というのはこの⊥の定義を述べたものとなっています。つまり、⊥の定義を推論規則としたのが否定除去規則です。

また、数学において矛盾している状態はあり得ません。つまり、「Pである」ということと「Pでない」ということが同時に成り立ってしまったら数学は無意味なものになってしまいます。

たとえば、「2は素数である」という言明と「2は素数でない」という言明の両方が成り立ってしまったら数学は崩壊します。数学において「Pである」ということと「Pでない」ということが同時に成り立ってはならないのです。

そのため、⊥は数学において常に正しくない命題です。矛盾がないのが数学なのですから、矛盾があるというのは常に正しくてはならないのです。

それでは、上の否定導入規則に現れる命題Pを仮定した場合に命題⊥が得られるというのはどういう状態でしょうか？

これはもし命題Pが成り立つならば⊥、つまり、Pならば⊥ということです。

これをP → ⊥という命題として考えた時、命題Pと命題P → ⊥の真偽はどうなるでしょうか？

下のようになります。

`P`	`⊥`	`P → ⊥`
`T`	`F`	`F`
`F`	`F`	`T`

このように、P → ⊥が真になるのは命題Pが偽である時のみであることが分かります。

つまり、命題Pを仮定した場合に命題⊥が得られたならば必ず命題Pは偽であるということです。

ということは命題￢Pは必ず真です。

ですから、命題Pを仮定した場合に命題⊥が得られたならば命題￢Pが正しいと結論できます。

これが否定導入規則が言っていることです。

同様に、命題￢Pを仮定した場合に命題⊥が得られたならば命題Pが正しいと結論できます。

これが背理法が言っていることです。

推論規則の実装

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

矛盾

まず矛盾を表す命題⊥を作成するための関数を実装します。

function create_contradiction () {
  return {
    type: 'prop',
    subtype: 'contra'
  };
}

⊥は命題なので、typeプロパティの値はpropとなります。

また、subtypeプロパティの値はcontraとすることにしました。

否定除去規則

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

function create_negation_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 !== 'neg') {
    throw new Error('not apply.');
  }
  if (!equal(pr1.conclusion, pr2.conclusion.sub)) {
    throw new Error('not apply.');
  }

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

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

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

否定除去規則・・・命題Pと命題￢Pの両方が正しいと証明されている時、命題⊥も正しいと言える。

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

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

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

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

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

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

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

そして、結論は命題⊥となりますのでcreate_contradiction関数を使用して矛盾を表すオブジェクトを作成しています。

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

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

否定導入規則

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

function create_negation_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.');
  }

  if (pr1.conclusion.subtype !== 'contra') {
    throw new Error('not apply.');
  }

  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_negation(pr2.conclusion);

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

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

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

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

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

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

そして、第3引数は含意導入規則の場合と同様に、この規則の適用によって落とされる仮定を表すオブジェクトに付加される番号となります。

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

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

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

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

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

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

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

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

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

背理法

次に背理法を適用する操作を特定の形の証明を作る操作としてcreate_raa関数において実装します。

function create_raa (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.');
  }

  if (pr1.conclusion.subtype !== 'contra') {
    throw new Error('not apply.');
  }
  if (pr2.conclusion.subtype !== 'neg') {
    throw new Error('not apply.');
  }

  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 = pr2.conclusion.sub;

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

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

上で述べた背理法（下に再掲）を忠実に実装しています。

背理法（RAA）・・・命題⊥が正しいと証明されている時、命題Pも正しいと言える。ただし、命題Pの証明からは仮定￢Pが落ちる。

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

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

そして、第3引数は含意導入規則や否定導入規則の場合と同様に、この規則の適用によって落とされる仮定を表すオブジェクトに付加される番号となります。

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

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

また、結論は第2引数の仮定を表すオブジェクトの結論を表すオブジェクトのsubプロパティの値（上の規則における仮定￢P中の命題Pを表す）となります。

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

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

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

なお、背理法の適用を表すオブジェクトのsubtypeプロパティの値はraaとすることにしました。

今回はここまで

今回はここまでとします。次回は連言に関する3つの推論規則について説明します。