I've recently been listening to lectures about constructible mathematics and I had an idea I haven't seen anywhere else (but I can't imagine is novel).

I'm interested in whether there are proofs of the form:

1. Suppose P is not provable.
2. Derive a contradiction.
3. Therefore P is provable.
4. Therefore P.

And especially if there exists a statement P (say in PA) which is only provable by means of such a contradiction.

Say we define a new term: "Constructible proof". This refers to any proof in classical mathematics for a proposition P where the fact "P is provable or P is not provable" is not used (which I believe is equivalent to this kind of proof by contradiction). Just to be clear, if P is constructibly provable by this definition, that doesn't make any assertion that the arguments in the proof are constructible ones, just that the proof itself can be constructed. (I.e. proof by contradiction is allowed just not on the proposition "P is provable".)

Then I'm interested in the proposition:

There exists a statement P in some formal system such that P is provable but P is not constructibly provable.

This is similar in form to Gödel's incompleteness theorem just with provable swapped for "constructibly provable" and true swapped with "provable".

I'd be interested to hear if this is a concept that makes any sense, whether you've heard something similar before, or just generally what people's thoughts are on this.

Thanks!