文脈付きモーダス・ポネンスについて
Def: lenient version Modus Ponens
$ \Gamma_1,\Gamma_2は論理式の集まりとする.$ \Gamma_1 \vdash \varphi \to \psi \quad \Gamma_2 \vdash \varphi \over \Gamma_1 \cup \Gamma_2 \vdash \psiをlenient version modus ponens(寛大なモーダスポネンス)$ \mathrm{(lMP)}とする.
一方,厳しいバージョンも考えてみる.
Def: strict version modus ponens
$ \Gammaは論理式の集まりとする.$ \Gamma \vdash \varphi \to \psi \quad \Gamma \vdash \varphi \over \Gamma \vdash \psiをstrict version modus ponens(厳格なモーダスポネンス)$ \mathrm{(sMP)}とする.
Observation
$ \mathrm{(lMP)}を持つ演繹体系は当然$ \mathrm{(sMP)}を持っていると考えて良い.
$ \Gamma_1 = \Gamma_2 = \Gamma = \Gamma \cup \Gammaより.
逆: $ \mathrm{(sMP)} \implies \mathrm{(lMP)}は成り立つのか?(そうだとして,常にそうなのか?)を調査してない
Memo
おそらくこの違いは形式化における技術的な問題で,紙とペン上の証明なら別に無視して文脈なし演繹体系で組み立てるべき(あまりにも煩雑すぎる)非本質的な疑念な気もする.