# Are there some programs for which the only proof of termination, is running of the program, and waiting to see if it stops, no matter how long?

The halting problem is semi-decidable, which means that if a program terminates then it will always be able to be determined.

Some programs can be proven to terminate without running them, with say:

• induction
• typed theories, such as typed lambda calculus.
• Ackermann function

Are there some programs for which there is no other proof system except for the computation itself, where no properties of the program is know in advanced? And hence if so, it would make sense that some non-terminating programs, even though it can be proven to terminate eventually, we don't know how long that proof would take to compute, because it would not be known if the program simply needs to run for longer, because as stated above, not even the property of how long the program should run before we can determine if it should have terminated yet, is known in advanced.

Are there some programs for which the only proof of termination, is the actual running of the program, and waiting to see if it stops, no matter how long it takes to complete?

• I suspect you can prove this as yes, for Turing machines, using something very similar to the halting problem uncomputability proof Oct 11, 2022 at 14:11
• A problem with your question seems to be that "proof" depends on the theory (axioms and derivation rules) that you choose. If you fix the theory you may well be able to show the existence of programs for which there is no proof of termination (in the chosen axiomatic system). The question then reminds one a little of Godels incompleteness results. I don't think your question as stated can be answered because of the lack of a specific theory in which your proofs are developed. Oct 11, 2022 at 14:43
• In my previous comment, I was referring to proving that no program can determine that some programs halt in n steps, using less than n steps - which is a more exact specification than the question Oct 11, 2022 at 14:44