A standalone statement of my question
Given a program that takes no argument, we are interested in whether the program will eventually terminate. My question is this:
Theoretically speaking, can we always find a proof of the termination/non-termination of a program?
Unlike the general halting problem, this problem does not require a mechanical procedure to generate a proof for each program which can potentially depend on the procedure itself, but instead, it allows the proof to depend on the specified program. It is thus a much weaker version.
There are obviously some proofs for some terminations and some non-terminations, and there are cases that remain unknown to this day (such as the evaluation of incrementing a number until finding a counter example of Collatz conjecture).
But more generally, is there any result on this? Is it always possible to prove whether the program terminates or not? Or is it provable that some programs cannot be proved either ways?
(Note that the answer to this question does not require solving, say, Collatz conjecture because it will only say there is a proof maybe that it terminates or maybe that it does not)
What I have thought about?
Cases that are easy are these two:
- If it terminates, we just run the program and the termination proves itself.
- If it falls into some repetitive periods, we track the history of all variables and we can prove that it does not terminate by remarking that it goes into a loop after certain step.
One case remains where the non-termination will never fall into periods and keep visiting new states. In this case, my first thought is that it comes down (almost) to prove the unboundedness (of some sort) of a sequence (of some kind of structures) defined by a program. So maybe a weaker version of my question would be: Is the unboundedness of a sequence of natural numbers (generated by the program) always provable?