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

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

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

選言除去規則は所謂場合分けです。命題`P ∨ Q`が成り立つと分かっている場合、命題`P`と命題`Q`をそれぞれ仮定してみて同じ命題`R`を結論することができれば命題`P ∨ Q`であるということから命題`R`を結論できたということと同じということです。

### 推論規則の実装

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

---

#### 選言除去規則

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

```js
function create_disjunction_elimination (pr1, pr2, pr3, pr4, pr5, dindex1, dindex2) {
  if (pr1.type !== 'proof') {
    throw new Error('not proof.');
  }
  if (pr2.type !== 'proof') {
    throw new Error('not proof.');
  }
  if (pr3.type !== 'proof') {
    throw new Error('not proof.');
  }
  if (pr4.type !== 'proof') {
    throw new Error('not proof.');
  }
  if (pr5.type !== 'proof') {
    throw new Error('not proof.');
  }
  if (pr4.subtype !== 'prem') {
    throw new Error('not premise.');
  }
  if (pr5.subtype !== 'prem') {
    throw new Error('not premise.');
  }

  if (pr1.conclusion.subtype !== 'disj') {
    throw new Error('not apply.');
  }
  if (!equal(pr1.conclusion.sub1, pr4.conclusion)) {
    throw new Error('not apply.');
  }
  if (!equal(pr1.conclusion.sub2, pr5.conclusion)) {
    throw new Error('not apply.');
  }
  if (!equal(pr2.conclusion, pr3.conclusion)) {
    throw new Error('not apply.');
  }

  var premises = [];
  var premises2 = [];
  gather_unique_obj(premises, pr1.premises);
  gather_unique_obj(premises, pr2.premises);
  gather_unique_obj(premises, pr3.premises);
  for (var i = 0; i < premises.length; i++) {
    if (!equal(premises[i], pr4.conclusion) && !equal(premises[i], pr5.conclusion)) {
      premises2.push(premises[i]);
    }
  }
  var conclusion = pr2.conclusion; //or pr3.conclusion

  var npr4 = shallowcopy(pr4);
  npr4.dindex = dindex1;
  replace(pr2, pr4, npr4);
  if (equal(pr2, pr4)) {
    pr2 = npr4;
  }

  var npr5 = shallowcopy(pr5);
  npr5.dindex = dindex2;
  replace(pr3, pr5, npr5);
  if (equal(pr3, pr5)) {
    pr3 = npr5;
  }

  return {
    type: 'proof',
    subtype: 'disj_elim',
    premises: premises2,
    conclusion: conclusion,
    sub1: pr1,
    sub2: pr2,
    sub3: pr3,
    sub4: npr4,
    sub5: npr5
  };
}
```

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

* 選言除去規則・・・命題`P ∨ Q`が正しいと証明されている時、命題`P`を仮定した場合に命題`R`が正しいと言え、かつ、命題`Q`を仮定した場合にも命題`R`が正しいと言えるならば、命題`R`も正しいと言える。ただし、命題`R`の証明からは仮定`P`と仮定`Q`が落ちる。

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

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

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

また、第2引数の証明を表すオブジェクトの結論を表すオブジェクト（上の規則における命題`P`を仮定した場合における命題`R`を表す）と第3引数の証明を表すオブジェクトの結論を表すオブジェクト（上の規則における命題`Q`を仮定した場合における命題`R`を表す）は同じでなければなりません。

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

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

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

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

また、結論は第2引数の証明を表すオブジェクトの結論を表すオブジェクト（上の規則における命題`P`を仮定した場合における命題`R`を表す）となります。

あるいは、第3引数の証明を表すオブジェクトの結論を表すオブジェクト（上の規則における命題`Q`を仮定した場合における命題`R`を表す）でも構いません。

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

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

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

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

この操作を第5引数の仮定を表すオブジェクトと第3引数の証明を表すオブジェクトに対しても行います。ただし、`dindex1`の代わりに`dindex2`を使います。

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

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

#### 選言導入規則（右）

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

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

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

  return {
    type: 'proof',
    subtype: 'disj_intro_r',
    premises: premises,
    conclusion: conclusion,
    sub1: pr,
    sub2: p
  };
}
```

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

* 選言導入規則（右）・・・命題`P`が正しいと証明されている時、命題`P ∨ Q`も正しいと言える。

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

また、第2引数として上の規則における命題`P ∨ Q`中の命題`Q`を表すオブジェクトを取ります。証明を表すオブジェクトではなく、数学的言明を表すオブジェクトであることに注意してください。

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

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

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

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

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

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

#### 選言導入規則（左）

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

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

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

  return {
    type: 'proof',
    subtype: 'disj_intro_l',
    premises: premises,
    conclusion: conclusion,
    sub1: pr,
    sub2: p
  };
}
```

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

* 選言導入規則（左）・・・命題`Q`が正しいと証明されている時、命題`P ∨ Q`も正しいと言える。

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

また、第2引数として上の規則における命題`P ∨ Q`中の命題`P`を表すオブジェクトを取ります。証明を表すオブジェクトではなく、数学的言明を表すオブジェクトであることに注意してください。

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

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

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

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

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

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

### 今回はここまで

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