In its most naive form my question boils down to this:
when is a proposition that is provable "by contradiction" also provable "directly"?
IOW, is it possible to know, a priori, that a proposition $p$, if it's provable at all, it can only be proved by contradiction (and therefore that it would be futile to attempt a direct proof)?
Let me try to sharpen my question slightly, by using the terminology and definitions given in this MSE answer. Let $C$ be the set1 of all propositions that are provable using classical logic. Similarly, let $M$ be all the propositions that are provable using minimal logic. Then, according to the cited post, $M \subsetneq C$ ("there are statements that are provable by contradiction that are not provable directly"), or IOW, $C\backslash M \neq \varnothing$.
So my question can be rephrased like this: given some proposition $p \in C$, is it possible to know, a priori (i.e. without necessarily finding a "direct proof" of $p$), whether $p \in M\;$?
In my very limited experience, proofs of results like "$C\backslash M \neq \varnothing$" are very unsatisfying because they rarely illuminate the question of whether a particular $p$ of interest belongs to $M$ or to $C\backslash M$. Is there any theorem from the standard mathematical curriculum but outside of mathematical logic that is known to belong to $C\backslash M$.
1 or class, or family, or whatever works!
Interesting question,
First of all there are 2 main steps between minimal and classical logic.
minimal logic doesn't allow deductions like: $ \vdash P \lor Q ,\vdash \lnot P, \to \vdash Q $ while Intuitionistic logic does allow them.
So i should find two examples but could only think of one
Example Davis–Putnam algorithm
The Davis–Putnam algorithm is a "solution" to the Boolean satisfiability problem and can be used to proof that an satisfiability problem is satisfiable. It does that by replacing the problem by an equisatisfiable but not equivalent problem and if this replacement is satisfiable then so is the original.
In classical logic this is enough, the algorithm proofs doesn't give the solution, for the original problem, it only proofs that a solution for the problem exist (somewhere).
For minimal/ intuitionistic/ constructive logic this is not enough you need to be able to give / construct the solution for the original problem, not for some other problem that is equisatisfiable. (what is that anyway), this algorithm doesn't give the solution, therefore this algorithm doesn't proof anything at all.
I once read a quip on classical logic by some intuitionistic logician.
"Goldbach's conjecture I have proved it, the conjecture is true if and only if $ k = 7 $, it is that simple."
"Is it that simple? you are the first who solved it, but how do you decide what k is?"
" Simple, if Goldbach's conjecture is true then and only then $ k = 7 $. nothing more complex than that."
Off course the modern version is that $ e = 42 $ but ach what is the difference.
You can say classical logic goes a step further in accepting proofs than minimal logic in classical logic the existence of a solution is enough, without having to construct the solution. and you can say that minimal logic is what you need to construct / show solutions. in the other (more fruitful) direction if a problem is not provable in classical logic, it isn't provable in minimal logic.
In many cases there is first a proof in classical logic and only much later a proof in minimal logic.