存在除去
定義
∃x∈X:A(x)⊢A(c)
WIIS
命題Aを満たす集合Xの元xが存在する場合、∃の除去は妥当な推論である。
またしても分かったような分からんような。
証明の途中で命題の定義を満たすような何がが演繹できたらってことなのだと思いますが、イマイチピンとこない。「もしもある集合の中のxが〇〇という条件を満たすなら、これを一般化する命題は成立するよね」みたいな推論に使うんですかね。
例えば「日本人のPFPファイター」という命題を満たす特定の要素、例えば井上尚弥が存在するなら、その具体例から「日本人の中の誰かはPFPファイターになる可能性がある」と一般化していく認識を一般化したものなのかなと。
他にも
（前提）2より大きな（後者）自然数3が存在する
ならば
（∃除去=一般化）2より大きな自然数は存在する
この推論を厳密化した感じのかなあと。
まだイマイチ日常的な感覚と一致しませんので練習問題探しています。
コメント