(A) Every simulation of input P that never halts unless simulating halt
decider H aborts this simulation <is> a non-halting computation. This
remains true even after H stops simulating P.

∃H ∈ Simulating_Halt_Deciders
∀P ∈ Turing_Machine_Descriptions
∀I ∈ Finite_Strings
(UTM(P,I) = ∞) ⊢ (H(P,I) = 0)

Because the simulation of the TM description of a TM on its input by a
UTM is known to be equivalent to the direct execution of a TM on its
input we know that the above mathematical logic is correct.

In English it says that whenever the input (P,I) to UTM would never halt
then a simulating halt decider correctly decides not halting on this input.

By screening out the distinctly different behavior of a UTM from a
simulating halt decider the pathological self-reference error of the
halting theorem is eliminated.

The behavior of the proxy computation forms the halt deciding basis for
the inputs that would otherwise specify the pathological
self-reference error.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On Fri, 21 May 2021 11:33:25 -0500
olcott <NoOne@NoWhere.com> wrote:

> (A) Every simulation of input P that never halts unless simulating
> halt decider H aborts this simulation <is> a non-halting computation.
> This remains true even after H stops simulating P.

If the simulator aborts the simulation then the simulation didn't halt,
the simulator halted the simulation. You cannot assume P is
non-halting simply because your omnishambles cockwomble of a
"partial halt decider" aborted the simulation until you address the
issues of branching logic predicated on arbitrary program input.

>
> ∃H ∈ Simulating_Halt_Deciders
> ∀P ∈ Turing_Machine_Descriptions
> ∀I ∈ Finite_Strings
> (UTM(P,I) = ∞) ⊢ (H(P,I) = 0)

Please refrain from using mathematical symbols that aren't present in
most fonts; Usenet readers often don't support displaying them as they
don't support fallback fonts.

[snip]

/Flibble

["Followup-To:" header set to comp.theory.]
On 2021-05-21, olcott <NoOne@NoWhere.com> wrote:
> (A) Every simulation of input P that never halts unless simulating halt
> decider H aborts this simulation <is> a non-halting computation. This
> remains true even after H stops simulating P.
>
> ∃H ∈ Simulating_Halt_Deciders
> ∀P ∈ Turing_Machine_Descriptions
> ∀I ∈ Finite_Strings
> (UTM(P,I) = ∞) ⊢ (H(P,I) = 0)

This seems to be saying that there exists some simulating decider H such
that H will call all non-halting Turing machines non-halting.

The halting theorem shows that the above is false; and you have
no disproof.

Among those those <P, I> inputs there is one problematic pair:

<P, I> = <H_Hat, H_Hat>

and so on, whose calculation is such that UTM(H_Hat, H_Hat) = ∞ if,
and only if, H(H_Hat, H_Hat) /= 0. Therefore it cannot be true that

(UTM(P,I) = ∞) ⊢ (H(P,I) = 0)

For that <P, I> pair. UTM(P, I) only calculates forever if H(P, I) is
nonzero, otherwise not.

> In English it says that whenever the input (P,I) to UTM would never halt
> then a simulating halt decider correctly decides not halting on this input.

It says that a simulating halt decider exists whuich correctly ...

> By screening out the distinctly different behavior of a UTM from a
> simulating halt decider the pathological self-reference error of the
> halting theorem is eliminated.

You have not "screened out" (and must not) the fact that the set of
<P, I> pairs contains the "eviL" <H_Hat, H_Hat>.

On 5/21/2021 11:54 AM, Kaz Kylheku wrote:
> ["Followup-To:" header set to comp.theory.]
> On 2021-05-21, olcott <NoOne@NoWhere.com> wrote:
>> (A) Every simulation of input P that never halts unless simulating halt
>> decider H aborts this simulation <is> a non-halting computation. This
>> remains true even after H stops simulating P.
>>
>> ∃H ∈ Simulating_Halt_Deciders
>> ∀P ∈ Turing_Machine_Descriptions
>> ∀I ∈ Finite_Strings
>> (UTM(P,I) = ∞) ⊢ (H(P,I) = 0)
>
> This seems to be saying that there exists some simulating decider H such
> that H will call all non-halting Turing machines non-halting.
>

Yes that is one way to look at that. On the other hand it is also saying
that any inputs to a UTM that would never halt are correctly decided as
non halting by a simulating halt decider.

This last aspect in anchored in the fact that the simulation of the TM
description of a TM is known to be computationally equivalent to the
direct execution of this TM.

> The halting theorem shows that the above is false; and you have
> no disproof.
>
> Among those those <P, I> inputs there is one problematic pair:
>
> <P, I> = <H_Hat, H_Hat>
>
> and so on, whose calculation is such that UTM(H_Hat, H_Hat) = ∞ if,
> and only if, H(H_Hat, H_Hat) /= 0. Therefore it cannot be true that
>
> (UTM(P,I) = ∞) ⊢ (H(P,I) = 0)
>
> For that <P, I> pair. UTM(P, I) only calculates forever if H(P, I) is
> nonzero, otherwise not.
>

Ĥ.q0 wM ⊢* Ĥ.qx wM wM ⊢* Ĥ.qy ∞
Ĥ.q0 wM ⊢* Ĥ.qx wM wM ⊢* Ĥ.qn

In the concrete case of replacing the simulating halt decider at state
Ĥ.qx with a UTM it is known that Ĥ([Ĥ]) would not halt thus meeting the
LHS of this: (UTM(P,I) = ∞) ⊢ (H(P,I) = 0)

Yes this is a different computation none-the-less it is a valid proxy
when the original computation was a simulating halt decider.

As soon as you understand this you will understand that my refutation of
the halting theorem is correct.

Ĥ([Ĥ]) never halts when the simulating halt decider at state Ĥ.qx is
replaced with a UTM, thus conclusively proving that the only possible
reason that Ĥ([Ĥ]) would halt is when the simulation of its input is
terminated at some point.

As soon as you understand that this is a truism you will understand that
my refutation of the halting theorem is correct:

(A) Every simulation of input P that never halts unless simulating halt
decider H aborts this simulation <is> a non-halting computation. This
remains true even after H stops simulating P.

>> In English it says that whenever the input (P,I) to UTM would never halt
>> then a simulating halt decider correctly decides not halting on this input.
>
> It says that a simulating halt decider exists whuich correctly ...
>
>> By screening out the distinctly different behavior of a UTM from a
>> simulating halt decider the pathological self-reference error of the
>> halting theorem is eliminated.
>
> You have not "screened out" (and must not) the fact that the set of
> <P, I> pairs contains the "eviL" <H_Hat, H_Hat>.
>

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 2021-05-21, olcott <NoOne@NoWhere.com> wrote:
> Ĥ([Ĥ]) never halts when the simulating halt decider at state Ĥ.qx is
> replaced with a UTM, thus conclusively proving that the only possible

You cannot perform replacements on the constituents of mathematical
objects.

When we say "replace a part of Ĥ([Ĥ])", that is just informal language
which means "determine a new object Ĥ2([Ĥ2]) which is similar to
Ĥ([Ĥ]), except that a specific part is substituted".

Small lesson in ANSI Common Lisp:

Define a global variable list which holds (A B C D):

[1]> (defvar list '(a b c d))
LIST
[2]> list
(A B C D)

Now let's substitute 3 for C in that list:

[3]> (subst 3 'c list)
(A B 3 D)

But that doesn't mean list has changed in any way:

[4]> list
(A B C D)

Look, it's still (A B C D). What "substitute 3 for C" means is "make a
new list which is based on that one, but where 3 appears instead of C".

In your muddled thinking, you are replacing things *ad hoc*,
confusing their identities.

On 5/21/2021 1:20 PM, Kaz Kylheku wrote:
> On 2021-05-21, olcott <NoOne@NoWhere.com> wrote:
>> Ĥ([Ĥ]) never halts when the simulating halt decider at state Ĥ.qx is
>> replaced with a UTM, thus conclusively proving that the only possible
>
> You cannot perform replacements on the constituents of mathematical
> objects.
>
> When we say "replace a part of Ĥ([Ĥ])", that is just informal language
> which means "determine a new object Ĥ2([Ĥ2]) which is similar to
> Ĥ([Ĥ]), except that a specific part is substituted".
>

Yes and the behavior of this new object is a valid proxy for the
behavior of the prior object in the case where the prior object is a
simulating halt decider and the new object is a simulator.

We are only answering the question:
Would the input P to the simulating halt decider H halt if its
simulation was never aborted?

This question <is> correctly answered by the proxy:
Would the input P to a simulator S halt?

> Small lesson in ANSI Common Lisp:
>
> Define a global variable list which holds (A B C D):
>
> [1]> (defvar list '(a b c d))
> LIST
> [2]> list
> (A B C D)
>
> Now let's substitute 3 for C in that list:
>
> [3]> (subst 3 'c list)
> (A B 3 D)
>
> But that doesn't mean list has changed in any way:
>
> [4]> list
> (A B C D)
>
> Look, it's still (A B C D). What "substitute 3 for C" means is "make a
> new list which is based on that one, but where 3 appears instead of C".
>
> In your muddled thinking, you are replacing things *ad hoc*,
> confusing their identities.
>

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein