# Question on instantiation

If I have ∃x(Fx implies P) then I can clearly instantiate to (Fy implies P) by existential instantiation. What if I have instead ((∃x Fx) implies P) then can I existentially instantiate to (Fy implies P)?

• NO; if you are working with e.g.Natural Deduction or Fitch, you must first "unpack" the formula ((∃x Fx) → P) according to the main "logical opearor", that in this case is . – Mauro ALLEGRANZA Nov 2 '17 at 19:05
• Maybe you have to start assuming Fx, derive (∃x Fx) by ∃-intro and finally use →-elim to derive P from ((∃x Fx) → P). – Mauro ALLEGRANZA Nov 2 '17 at 19:06
• I think this actually requires the Axiom of Choice. Most automatic prover programs assume it implicitly. You may have an infinity of `x`s meeting condition `F(x)`, but that doesn't mean you can choose a specific one! – barrycarter Nov 3 '17 at 17:00

Yes, every y instantiates (Fy implies P):

``````Choose any y at all.

We are given that ((Exists x: Fx) implies P).
Then either P is true or (Exists x: Fx) is false.

Assume P is true.
Then (Fy implies P), because anything implies true.

Otherwise, (Exists x: Fx) is false.
Therefore Fy is false for our y.
Then (Fy implies P), because false implies anything.
``````
• I don't understand "Then (Fy implies P), because anything implies true." While it is true that ((False or True) implies True) is always True, I don't see how it is relevant, perhaps I'm missing your point? – Clclstdnt Nov 2 '17 at 19:18
• What would make it true but not relevant, in your interpretation of what is going on? This proof fails for logics that involve a notion of relevance: proof-theory, constructive reasoning, Intuitionism, etc. But normal classical logic based on models just doesn't have such a concept AFAIK. – user9166 Nov 2 '17 at 20:53
```{1}     1.  Ǝx[Fx] → P             Prem.
{2}     2.  Ǝy[Fy]                 Assum.
{3}     3.  Fa                     Assum. TD(a)
{3}     4.  Ǝx[Fx]                 3 EI
{1,3}   5.  P                      1,4 MP
{1,2}   6.  P                      2,3,5 EE
{1}     7.  Ǝy[Fy] → P             2,6 CP
```