XPost: comp.theory, sci.lang.semantics, comp.ai.philosophy
On 8/20/2020 12:07 PM, Kaz Kylheku wrote:
On 2020-08-20, Newberry <newberryxy@gmail.com> wrote:
Let H(P, n) be a program with two possible outcomes: TRUE and FALSE. The
parameter P is a program and n is its input. Suppose that H(P, n) = TRUE
if and only if P halts on n. Suppose further that if H(P, n) = FALSE
then P does not halt on n, and suppose that H is sound.
What if H does not produce a result? There is the problem that H itself
might not halt.
Such an H is excluded from the solution set.
Let furthermore
P* be a program with itself as a parameter. The claim is that there
exists a program H such that H(H, H*) = FALSE, that is, H proves that it
does not prove that H* halts.
In the halting problemm, H is understood to be a universal halting
decider that works for all possible P and N.
The result which is proven is that there is no such universal H.
For every proposed H, we can apply the devastating self-referential
trick to easily come up with an example input pair which breaks it.
You don't get to cherry-pick a different, hand-crafted H for a given (P,
n) input instance, conveniently ignoring that there exist other cases
for which it doesn't work.
Years ago, I unsuccessfully tried to explain various apsects of this to
our resident Peter Olcott.
Moreover, the halting theorem also proves that you cannot even come up
with all the possible non-universal H functions that are cherry picked
to report a correct answer for a given problem instance.
Proof: such a H function is basically just a constant. For instance,
you give me some (Pi, Ni) input pair. I decide whether it halts or not.
If it halts, I propose the trivial function H(P, N) -> T.
If it doesn't halt, I propose H(P, N) -> F.
I cannot do this for all possible inputs. Why? Because now I have been
tasked with the duty of being a universal halting decider; and the self-referential trick now applies to me.
When the halting problem counter-example is examined concretely instead
of abstractly the key details abstracted away by the abstraction can now
be directly discerned. This changes everything.
--
Copyright 2020 Pete Olcott
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)