プログラマー向けというか、数理論理学の枠組みをプログラムとして実装したい人とか形式化数学をやりたい人向けの記事かもしれません(形式化数学についてはこちらの記事もどうぞ)。
なお、ソースコード全体は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つの推論規則について説明します。