Skip to main content
MathOverflow

Return to Answer

added 27 characters in body
Source Link
Antonio E. Porreca
Antonio E. Porreca
  • 1.2k
  • 1
  • 9
  • 14

It is true that $H(A)$ implies that we have a proof of $H(A)$, and we can find it by enumeration: as you noted, a proof of $H(A)$ is just a finite sequence of configurations or states of program $i$ on input $x$, each one of them reachable from the previous one according to the rules described by program $i$ itself (hence, such a proof is algorithmically verifiable).

The problem with your argument is that $\neg H(A)$ does not necessarily imply that we have a proof of it, as you assume when saying “But now we have a proof of $\neg H(A)$”. SomeSome programs can indeed have a non termination-termination proof; for instance, a finite sequence of configurations of the program that repeat cyclically. But other programs can go through an infinite number of non-recurring configurations: thus, the notion of non-termination proof as a finite sequence of configurations is flawed.

Even by giving a lot of thought to the question, you won’t probably find any satisfying notion of “non-termination proof” applicable to all programs. The reason is that such a notion is (provably)provably nonexistent (formally, the set of non-halting programs is not recursively enumerable).

It is true that $H(A)$ implies that we have a proof of $H(A)$, and we can find it by enumeration: as you noted, a proof of $H(A)$ is just a finite sequence of configurations or states of program $i$ on input $x$, each one of them reachable from the previous one according to the rules described by program $i$ itself (hence, such a proof is algorithmically verifiable).

The problem with your argument is that $\neg H(A)$ does not necessarily imply that we have a proof of it, as you assume when saying “But now we have a proof of $\neg H(A)$”. Some programs can indeed have a non termination proof; for instance, a finite sequence of configurations of the program that repeat cyclically. But other programs can go through an infinite number of non-recurring configurations: thus, the notion of non-termination proof as a finite sequence of configurations is flawed.

Even by giving a lot of thought to the question, you won’t probably find any satisfying notion of “non-termination proof”. The reason is that such a notion is (provably) nonexistent (formally, the set of non-halting programs is not recursively enumerable).

It is true that $H(A)$ implies that we have a proof of $H(A)$, and we can find it by enumeration: as you noted, a proof of $H(A)$ is just a finite sequence of configurations or states of program $i$ on input $x$, each one of them reachable from the previous one according to the rules described by program $i$ itself (hence, such a proof is algorithmically verifiable).

The problem with your argument is that $\neg H(A)$ does not necessarily imply that we have a proof of it, as you assume when saying “But now we have a proof of $\neg H(A)$”. Some programs can indeed have a non-termination proof; for instance, a finite sequence of configurations of the program that repeat cyclically. But other programs can go through an infinite number of non-recurring configurations: thus, the notion of non-termination proof as a finite sequence of configurations is flawed.

Even by giving a lot of thought to the question, you won’t probably find any satisfying notion of “non-termination proof” applicable to all programs. The reason is that such a notion is provably nonexistent (formally, the set of non-halting programs is not recursively enumerable).

Source Link
Antonio E. Porreca
Antonio E. Porreca
  • 1.2k
  • 1
  • 9
  • 14

It is true that $H(A)$ implies that we have a proof of $H(A)$, and we can find it by enumeration: as you noted, a proof of $H(A)$ is just a finite sequence of configurations or states of program $i$ on input $x$, each one of them reachable from the previous one according to the rules described by program $i$ itself (hence, such a proof is algorithmically verifiable).

The problem with your argument is that $\neg H(A)$ does not necessarily imply that we have a proof of it, as you assume when saying “But now we have a proof of $\neg H(A)$”. Some programs can indeed have a non termination proof; for instance, a finite sequence of configurations of the program that repeat cyclically. But other programs can go through an infinite number of non-recurring configurations: thus, the notion of non-termination proof as a finite sequence of configurations is flawed.

Even by giving a lot of thought to the question, you won’t probably find any satisfying notion of “non-termination proof”. The reason is that such a notion is (provably) nonexistent (formally, the set of non-halting programs is not recursively enumerable).