(∃x)(∃y)(Jxy v Kxy) ⊃ (∃x)Lx : Why can this not be instantiated?

Question

_{Source: p 502, A Concise Introduction to Logic (12 Ed, 2014) by Patrick Hurley}

Because line 1 cannot be instantiated, the only strategy is to derive the antecedent of the conditional with the aim of deriving the consequent via modus ponens. [...]

1. Why is the bolded true? Why can you not instantly replace 1A with 9, and 1C with 13?

2. This proof appears overcomplicated.
   Instead of an Indirect Proof, why not use Conditional Proof?
   Then using 1A as the Assumption of the Conditional Proof, you can start the proof at 11;
   3-10 above can be skipped and would never be needed.

Answer 1

Because UI and EI rules "works" only with outermost quantifiers, i.e. when we have e.g. (∃x)Px.

If we have instead (∃x)Px ⊃ (∃y)Qy, we cannot apply the quantifier rules to remove them.

---

According to your question 2, you think that the proof should be 'simpler' as follows :

[1A] i.e. 11) (∃x)(∃y)(Jxy ∨ Kxy)   --- premise

[1C] i.e. 12) (∃x)Lx         --- premise

2) (x)(y)(Lx ⊃ ¬Ly)         --- premise

13) Lo               --- from 12) by EI

14)-15) Lo ⊃ ¬Lo          --- from 2) by UI twice

16) ¬Lo              --- from 13) and 15) by MP

17) Lo ∧ ¬Lo            --- from 13) and 16) by Conj

Now we have a contradiction and thus - according to the IP rule - we have to "discharge" one of the premises to derive this one premise's negation. We may discharge 12), deriving :

18) ¬(∃x)Lx.

The derivation is formally correct, but what we have proved is:

from the premises : (∃x)(∃y)(Jxy ∨ Kxy), (∃x)Lx, (x)(y)(Lx ⊃ ¬Ly),

it follows ¬(∃x)Lx.

Please, note that the derivation does not use [1A] at all; thus (as we can imagine) the derivation boils down to :

(x)(y)(Lx ⊃ ¬Ly) implies ¬(∃x)Lx.

The textbook's original proof was instead :

from the premises : (∃x)(∃y)(Jxy ∨ Kxy) ⊃ (∃x)Lx, (x)(y)(Lx ⊃ ¬Ly),

it follows (x)(y)¬Jxy,

which is quite different.

Answer 2

1. "If there are licorns then there are horses with horns" does not entail that there are licorns. Equivalently in logic, "(∃x)(Lx) ⊃(∃x)(Hx)" does not entail "(∃x)(Lx)". The existentials cannot be directly instantiated because they are nested in a more complex logical form.

2. The assumption (3) is used to derive a contradiction. Then we can say that the assumption was false: (18) is the negation of (3). If we assume (11) instead we will not prove (18) but the negation of (11) which is not what we're looking for.