一般化と∃除去の仮定の解消

存在除去は下のリンクの記事のような雰囲気の演算のことで、人の普遍的な認識を厳密化したものだと感じます。

例えば「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を演繹しています。

しっくりはこないけど焦りは禁物なのでこんな程度の理解で。