- 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.
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."
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.
Notice my description: "Turing proved that no general algorithm can be formulated that can answer this question across all possible programs." The operative part here is "across ALL possible programs". The proof does stop us from knowing that SOME programs will or will not halt. It only stops us from being able to determine this for EVERY possible program. My post explores a very specific subset of programs that we can prove will terminate, then asks what pattern(s) underlie such programs, and then explores the use of such patterns in a variety of interesting problems. It is this last result that most intrigued me, and caused me to write about it.