3
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

More than 5 years have passed since last update.

@pizyumi(ゆりな🎀)

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

3
Posted at

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

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

https://github.com/pizyumi/rena

連載まとめ

選言に関する推論規則

今回は選言に関する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関数において実装します。

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

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

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

3
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
3
1

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?