[jondgoodwin]

Author here. Cool story about odd perfect examples. That said, my post is not trying to find a way to crack the halting problem, and thereby demonstrate it is not real. Turing wrote a most excellent proof, and I stand by it wholeheartedly. I even cite another famous numeric example of a program we still do not know if it will terminate for all numbers: the Collatz conjecture.

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.

[jondgoodwin]

Important mistype. It should read: "The proof does NOT stop us from knowing that SOME programs will or will not halt.

[jpt4]

You may also be interested in Willard's Self-Verifying Theories: https://en.wikipedia.org/wiki/Self-verifying_theories

[jpt4]

It does however apply to more properties than merely halting: https://en.wikipedia.org/wiki/Rice's_theorem

[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.