I want to prove the following using natural deduction:
$\quad ∃( ()) → ∃(K ()) ⊢ ∃(K ()) ∨ ∀(¬ ()) $
If I were to rewrite $ ∃( ()) → ∃(K ())$ to $ ¬∃( ()) ∨ ∃(K ())$ then I would know how to prove it, but I'm not allowed to do that.
I feel stuck and I would really appreciate some help on how to prove this!
Here is a proof sketch. This sketch assumes an instance of the law of excluded middle. If proving the LEM is unfamiliar, let me know and I'll include a brief excerpt on how to prove that.
For your proof, you'll want to start with (either by proving or citing LEM) $\exists x F(x) \lor\neg\exists x F(x)$. Then you can use disjunction elimination, i.e. case on the instance of LEM. In the first case, you can use implication elimination on the assumption of you proof, which will conclude $\exists x K(x)$. Then use disjunction introduction to derive the desired claim. Then you need to treat the other case. So you'll have $\neg\exists x F(x)$ as an assumption. But, this is equivalent to (and from which you can prove) $\forall x\neg F(x)$. Then use disjunction introduction. Now you are in a postion to apply disjunction elimination.
I have left things somewhat vague and I hope it is a useful exercise to fully write out a real proof.