I've recently started learning First-Order Logic and I have been doing some Natural Deduction exercises. I understand the principles behind most of the Inference Rules but when it comes to applying Classical Rules such as the law of excluded middle, I struggle to reason why it has been used.
In the proof for:
(φ → ∃x. ψ) ⊢ ∃x. (φ → ψ)
- φ → ∃xψ (hypothesis)
φ ∨ ¬φ (law of excluded middle)
∃x. (φ → ψ)
The solution proceeds by using law of excluded middle for φ so that you can use the ∃ elimination rule to reach the conclusion. I understand the solution but I cannot understand why someone has thought to use law of excluded middle to proceed. Is there any intuition behind this, or is it just a 'trick'?