[j-pb]

A bit tangential, but turings proof only works with some very strict assumptions.

- Clasical logic as the foundation for math.

- Proofs by contradiction work.

- That the church turing thesis holds.

I guess these are kinda two sides of the same coin. But still worth noting.

[remexre]

I believe that it's not a proof by contradiction, but a direct proof of a negative statement. Subtle distinction:

Direct proof of negative statement: Assuming P is true, there is a contradiction. Thus, P is false.

Proof by contradiction: Assuming P is not true, there is a contradiction. Thus, P is true.

The key bit is that in constructive mathematics, "P is not true" does not imply "P is false."

[j-pb]

After some digging I found several blogs that make the same distinction as you do.

However, basically all of literature calls the undecidability of the halting problem a proof by contradiction.

So I guess that there are some intuitionists that make that distinction. I'm not sure that I'd call it a direct or constructive proof though.

The thing is that if you follow constructive reasoning and you assume that the church turing thesis is true, then all of math becomes somewhat small. No more uncountably infinite stuff, no dense reals, computable objects only e.t.c.

I feel like we've painted mathematics into a dogmatic corner, and tbh I have no idea how to get out of it.