プログラマー向けの（？）数理論理学（７）連言に関する推論規則

プログラマー向けというか、数理論理学の枠組みをプログラムとして実装したい人とか形式化数学をやりたい人向けの記事かもしれません（形式化数学については[こちらの記事](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 ∧ Q`が正しいと証明されている時、命題`P`も正しいと言える。
* **連言除去規則（左）**・・・命題`P ∧ Q`が正しいと証明されている時、命題`Q`も正しいと言える。
* **連言導入規則**・・・命題`P`と命題`Q`の両方が正しいと証明されている時、命題`P ∧ Q`も正しいと言える。

`∧`が「かつ」という意味であったことを考えればこれらの規則が妥当であることは理解できるかと思います。

### 推論規則の実装

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

---

#### 連言除去規則（右）

最初に連言除去規則（右）を適用する操作を特定の形の証明を作る操作として`create_conjunction_elimination_right`関数において実装します。

```js
function create_conjunction_elimination_right (pr) {
  if (pr.type !== 'proof') {
    throw new Error('not proof.');
  }

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

  var premises = [];
  gather_unique_obj(premises, pr.premises);
  var conclusion = pr.conclusion.sub1;

  return {
    type: 'proof',
    subtype: 'conj_elim_r',
    premises: premises,
    conclusion: conclusion,
    sub: pr
  };
}
```

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

* 連言除去規則（右）・・・命題`P ∧ Q`が正しいと証明されている時、命題`P`も正しいと言える。

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

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

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

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

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

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

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

なお、連言除去規則（右）の適用を表すオブジェクトの`subtype`プロパティの値は`conj_elim_r`とすることにしました。

#### 連言除去規則（左）

次に連言除去規則（左）を適用する操作を特定の形の証明を作る操作として`create_conjunction_elimination_left`関数において実装します。

```js
function create_conjunction_elimination_left (pr) {
  if (pr.type !== 'proof') {
    throw new Error('not proof.');
  }

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

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

  return {
    type: 'proof',
    subtype: 'conj_elim_l',
    premises: premises,
    conclusion: conclusion,
    sub: pr
  };
}
```

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

* 連言除去規則（左）・・・命題`P ∧ Q`が正しいと証明されている時、命題`Q`も正しいと言える。

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

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

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

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

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

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

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

なお、連言除去規則（左）の適用を表すオブジェクトの`subtype`プロパティの値は`conj_elim_l`とすることにしました。

#### 連言導入規則

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

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

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

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

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

* 連言導入規則・・・命題`P`と命題`Q`の両方が正しいと証明されている時、命題`P ∧ Q`も正しいと言える。

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

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

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

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

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

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

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

### 今回はここまで

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