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

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

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

https://github.com/pizyumi/rena

連載まとめ

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

連言に関する推論規則

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

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

連言除去規則（右）・・・命題P ∧ Qが正しいと証明されている時、命題Pも正しいと言える。
連言除去規則（左）・・・命題P ∧ Qが正しいと証明されている時、命題Qも正しいと言える。
連言導入規則・・・命題Pと命題Qの両方が正しいと証明されている時、命題P ∧ Qも正しいと言える。

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

推論規則の実装

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

連言除去規則（右）

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

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

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

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

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

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

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

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

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

連言導入規則

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

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つの推論規則について説明します。