∀導入定義の人の認識を結びつけるために藻掻きます。
全称導入と仮定の解消
定義
これが全称導入の定義
A(c)⊢∀x∈X:A(x)
WIIS
A(c)の論理式を満たすようなcは集合Xの任意の要素xに対しても成立する。
cは全てのXの要素を表現するものでなければならず、もしも論理式Aが特定のx_1においてのみ成立するのなら∀導入の適用は許されません。
1.x=0(前提)
2.∀x(x=0)(∀導入)
つまりこれはダメ。
xの値が定まったままでは∀導入の推論規則は適用できないと言っています。その意味を考えます。
下の演繹は似てるようで上とは少し異なります。
1.[x=0]
2.x=0
3.x=0→x=0(→導入)
4.∀x(x=0→x=0)(∀導入)
これなら∀導入を認めてよいはずです。
任意のxにおいてx=0ならばx=0。
当たり前っちゃ当たり前なんですが。→導入で前提を解消し、暗黙的な「もしも〜だったら」を導入しています。この場合は「もしもx=0だったら」。
演繹図で「全ての〜」を表現するならx=0という特定の値を示す仮定を解消するってこと。
もう少し僕の解釈を補足すると。
1.[x=0]
2.∀x(x=0)(∀導入)
3.x=0→∀x(x=0)(→導入)
これは「x=0ならば、全てのxにおいてx=0が成り立つ」。
前件でx=0と言っているのに、後件で全てのxと言い直していて意味不明で人の認識では理解できない形になってしまいます。
特定のx=0をを示す仮定を解消するか、しないかってだけですが、異なる意味になるので、もし特定の仮定があるのなら、全称導入をする前に仮定の解消をしておく必要があるだろうってことです。
全称導入の定義には一つ、こんな文脈があるだろうって人の認識と推論規則を一致させる僕なりの解釈です。
もしも特定のxを解消しないまま∀導入を適用してしまうと、意味不明な式が演繹できてしまいます。
コメント