Can one introduce an existential twice?

OpenLogicProject / fitch-checker

JavaScript/PHP Fitch-style natural deduction proof editor and checker (NO LONGER MAINTAINED)

GNU General Public License v3.0

51 stars 5 forks source link

Can one introduce an existential twice? #9

Closed FrankHubeny closed 5 years ago

FrankHubeny commented 5 years ago

Looking at a post on Philosophy Stack Exchange I was able to reproduce what a user claimed a professor said was a correct derivation: https://philosophy.stackexchange.com/q/60866/29944

03022019-2

However, I am puzzled why this is correct, but perhaps it is.

rzach commented 5 years ago

You may infer (∃x)A from any formula A[t/x] (the result of replacing every free occurrence of x in A by t). If A is (∃x)Fx then x has no free occurrences in it, so A[t/x] is just (∃x)Fx. Hence, you may infer (∃x)(∃x)Fx from (∃x)Fx by ∃I. (This is called vacuous quantification).