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

プログラマー向けというか、数理論理学の枠組みをプログラムとして実装したい人とか形式化数学をやりたい人向けの記事かもしれません（形式化数学については[こちらの記事](https://qiita.com/pizyumi/items/24e5ba843133059fd74a)もどうぞ）。

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

[https://github.com/pizyumi/rena](https://github.com/pizyumi/rena)

### 連載まとめ

* [プログラマー向けの（？）数理論理学](https://qiita.com/pizyumi/items/5def02eac4f01baa9f02)

### 否定に関する推論規則

今回は否定に関する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つの推論規則をプログラムでどう実装するかという話なので、プログラミングに興味のない方は飛ばして次の記事に進んでください。

---

#### 矛盾

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

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

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

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

#### 否定除去規則

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

```js
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`関数において実装します。

```js
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`関数において実装します。

```js
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`を表すオブジェクトを取ります。

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

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

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

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

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

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

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

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

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

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

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

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

### 今回はここまで

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