Is it provably true/false that for a program, there exists a proof whether it halts or not?

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?
Clarification

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?

Actually this is no different from the halting problem unsolvability. If you have any formal system T with a proof verifier program V that can reason about programs (as you desire in your question), then let H be the program that does the following on input (P,X):

  For each string s in length-lexicographic order:

    If V( "Program P halts on input X." , s ) then output "true".

    If V( "Program P does not halt on input X." , s ) then output "false".

Here V(Q,s) outputs "true" if s is a valid proof of Q and "false" otherwise. V always halts, because that is what it means for T to have a proof verifier program. (And we cannot use and do not care about formal systems that do not.)

Now, if for every (P,X) there is always a proof over T of either "Program P halts on input X." or its negation, then H solves the halting problem (because H eventually checks each possible proof), which is impossible.

Here I am assuming that your T is sound for program halting (i.e. does not prove a false statement about program halting). Otherwise, it is possible that T proves the wrong thing and hence H fails to solve the halting problem.

By the way, unsolvability of the halting problem and another computability question called the zero-guessing problem are very important facts that can be used to easily prove the generalized incompleteness theorem, by essentially the same kind of reasoning. Incidentally, Godel proved his incompleteness theorem for PA under an assumption called ω-consistency, which is essentially equivalent to PA being sound for program halting. Rosser removed that assumption by a clever trick. But Rosser's version also can be proven easily using the zero-guessing problem instead of the halting problem.

StackExchange Computer Science Q#152064, answer score: 31