You are all familiar with the halting problem so I won't repeat it.
Suppose $H$ is a Turing machine which takes as input an encoding of another Turing machine $M$, then searches all possible proof strings until it finds a proof that $M$ halts or a proof that $M$ does not halt. Of course, if there is no such proof then it will search forever, so I do not claim that $H$ decides the halting problem.
Suppose $Q$ is the usual counterexample that first invokes $H$ on $Q$ as a subroutine (this is possible using quine techniques). Then if $H$ reports that $Q$ doesn't halt, it halts. If $H$ reports that $Q$ does halt, it enters a trivial infinite loop.
Now consider what the subroutine $H$ returns. If $H$ would report that $Q$ would halt, that would mean it had found a specific proof that $Q$ would halt, despite the fact that $Q$ obviously would not halt and we could see it enter a trivial infinite loop after a finite number of steps. Assuming that the proof system is consistent, we can be certain that there is no proof that $Q$ halts. Likewise, we can be certain that there is no proof that $Q$ does not halt.
Since there is no proof that $Q$ halts and no proof that $Q$ does not halt, we can be certain that $H$ will never find either one, therefore the $H$ subroutine of $Q$ will continue searching proofs forever, QED. We have proved that $Q$ does not halt.
Wait, what? The fact there is no proof gives a proof. Of course, if there is a proof, that proof is wrong. What's going on here? Where is the error in my reasoning?
(Credits to raoof for the "proof" sketch)