自然演繹、Mizar、SerND

Natural Deduction	Mizar	SerND
→ introduction	assume	assume + use
→ elimination	–	apply
∧ introduction	thus	concat
∧ elimination	–	select
∨ introduction	–	add
∨ elimination	per cases	cases
∀ introduction	let	for
∀ elimination	–	instantiate
∃ introduction	take	introduce
∃ elimination	consider	choice

特にキーワードがないのは、

1. ⇒除去 apply モダスポネンス
2. ∧除去 select
3. ∨導入 add
4. ∀除去 instantiate

いずれも then, thus, byあたりで済ますのだろう。SerNDでも取り入れられるか。

A
then
B by A⇒B // apply to

A∧B
then // select
A

from A∧B // select
A

A
then // add
A∨B

from A // add
A∨B

∀x.P
then // instantiate
P(t)

from ∀x.P // instantiate
P(a)

やっぱり、明白さに欠ける。