一般化の雰囲気

一般化の雰囲気

暇つぶしに見て

2023.10.01

∃除去の話の続き。
∃除去、導入の推論規則を読んだだけだと、どうしてそれが必要なのかが感じられない。なんとなく、人が法則を一般化させる認識が根底にはあるんだろうな、とは感じられますが、しっくりはこない。

参考にしている本にこんな記述が。

というわけで自作の例題を元に考え見ます。

1.[1+x](前提)
2.[x=0](仮定)
3.1+0(代入)
4.1+0=1(加法定義)
4.∃x(1+x=1)(∃導入)
5.1+x→∃x(1+x=1)(→導入)

面倒なので同値関係などの細かいの証明は省きました。
上の本の引用は、4行目のように∃導入を適用する時に2行目の仮定を解消していいよってことかなあと。

1+xはx=0の時に1+x=1を満たします。この場合は人は、固定されたx=1という仮定を解消することで「〇〇を満たす☓☓が存在する」と認識を一般化し、法則の適用範囲を広げようとします。

存在導入の仮定の解消の規則はこんな文脈から発生しているのではなかと。

もう少し分かり易い別の例を考えてみます。

1.∀x(x-x=0)(前提)
2.a-a=0(∀除去)
3.∃y(a-y=0)(∃導入)
4.∃y∀x(x-y=0)(∀導入)
5.∀x(x-x=0)→∃y∀x(x-y=0)

翻訳すると、任意のxでx-x=0が成り立つなら、x-y=0を満たす任意のxに対して必ずyが存在する。

例題も演繹も翻訳も我流ですので悪しからず。ただなんとなく問題ないだろうとは思ってます。

存在導入で仮定を解消して良いのは∀除去の後の演繹を繋いでおいて良いのと同じかなあと。とりあえずはこの理解で進めます。