What's the intuition behind using Law of Excluded Middle in Natural Deduction? 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. For example: In the proof for: (φ → ∃x. ψ) ⊢ ∃x. (φ → ψ) 1. φ → ∃xψ (hypothesis) 2. φ ∨ ¬φ (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'?

As per @Sudix's answer above, the intuition behind the use of the Law of Excluded Middle in the proof of :

> $(φ → ∃x ψ) ⊢ ∃x (φ → ψ)$

is to apply a "case analysis".

_(i)_ Assume that $φ$ does not hold, i.e. assume $¬φ$.

This means (by the truth-table for the _conditional_ ) that $φ → ψ$ is TRUE, and thus also $∃x (φ → ψ)$ is TRUE.

_(ii)_ Now assume that $φ$ holds, i.e. assume $φ$.

We know that the premise $(φ → ∃x ψ)$ holds, and this means (again by the truth-table for the _conditional_ ) that also $∃x ψ$ is TRUE, i.e. that $ψ$ is TRUE for some $x$.

Thus, $φ → ψ$ is TRUE for some $x$, i.e. $∃x (φ → ψ)$ is TRUE.