I'm fascinated by a proof that the Sorgenfrey plane $\mathbb{R}_l^2$ is not normal, given in Munkres' Topology. Instead of explicitly finding two disjoint closed sets whose disjoint neighborhoods don't exist, the proof is by contradiction.
Asserting classical first-order logic, since $\exists \neg ≡ \neg \forall$, the proof goes $\forall (\text{something}) → \bot$.
The textbook asks to find an explicit example in Exercise 9 of Section 31, though I've not solved it yet.
This arises the following question:
Is there a statement in $\Sigma_n^0$ (where $n > 0$) which cannot be proven by an example (or at least, such examples cannot be found by a computation), yet it is actually proven?