存在除去は下のリンクの記事のような雰囲気の演算のことで、人の普遍的な認識を厳密化したものだと感じます。
例えば「1より大きな数は存在する」というありふれた人の認識は、厳密には「2は1より大きな数は数である」という暗黙的な前提が元になっています。
∃除去で仮定を解消してよいのは、この文脈が背後にあるからだろうって解釈しました。
論理学で参考にしている本の例題を引用します。
ちなみにこれ、∃y(y=3∧U(y))って論理式に意味を与えようとしてはいけません。
意味はなく、ただ規則を適用していくとこんな形になるよね、こんな規則だと人の認識に近いよねって話なので、深入りすると混乱します。
存在除去と一般化
証明
1.[y=3∧U(y)](前提)
2.y=3,U(y)(∧除去)
3.U(3)(代入)
4.3=3(代入)
5.3=3∧U(3)(∧導入)
6.∃y(y=3∧U(y))(∃導入)
7.3=3∧U(3)(∃除去)
8.U(3)(∧除去)
9.∃x(y=3∧U(y))→U(3)
6行目で∃導入をしているのは、次の∃除去で1行目の仮定を解消する為です。
逆にU(3)からの∃x(y=3∧U(y))の演繹に挑戦。
1.U(3)
2.3=3,U(3)
3.3=3∧U(3)
4.∃y(y=3∧U(y))
5.U(3)→∃y(y=3∧U(y))
2行目はU(3)をU(3)∧y=3へ演繹してもいいって規則をググれなかったので、U(y=3)だと勝手に解釈してU(3)∧y=3を演繹しています。
しっくりはこないけど焦りは禁物なのでこんな程度の理解で。
Bitly
amzn.to
コメント