XPost: comp.theory, sci.logic, sci.math

On 9/25/2021 6:55 PM, Ben Bacarisse wrote:

olcott <NoOne@NoWhere.com> writes:

On 9/25/2021 4:24 PM, Ben Bacarisse wrote:

olcott <NoOne@NoWhere.com> writes:

On 9/25/2021 3:43 PM, Ben Bacarisse wrote:

olcott <NoOne@NoWhere.com> writes:

On 9/24/2021 6:22 PM, Ben Bacarisse wrote:

olcott <NoOne@NoWhere.com> writes:

On 9/24/2021 3:54 PM, Ben Bacarisse wrote:

olcott <NoOne@NoWhere.com> writes:

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞ >>>>>>>>>> if the simulated ⟨Ĥ⟩ applied to ⟨Ĥ⟩ halts, and

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
if the simulated ⟨Ĥ⟩ applied to ⟨Ĥ⟩ does not halt >>>>>>>>> This is wrong since, apparently,

"I always used this symbol Ĥ in the context of the Linz proofs and
never used it in any other way"
If Ĥ refers to the Ĥ in Linz's proof your annotations are incorrect, and
if Ĥ is being using "in the context of the Linz proof" but denotes >>>>>>>>> something else (what?) then you are not being serious.

As you have indicated that you have recalled I corrected the error in >>>>>>>> the Linz specification that had two start states by changing one of >>>>>>>> these start states to qx.

Not the issue. (Though I'll note again that you don't use the notation >>>>>>> you came up with in a helpful way. There is no need for qx because it >>>>>>> could be called H.q0 or, better yet, H.0.)

After this I augmented the Linz notation further so that it showed the >>>>>>>> notation when the Linz Ĥ is specifically applied to the Linz ⟨Ĥ⟩ where
the halt decider embedded at qx is a simulating halt decider.

Not the issue but if you used the . notation better this would be much clearer.

Since Linz does not exclude simulating halt deciders this is still the >>>>>>>> Linz Ĥ.

You annotations are incorrect. If you'd like to know why, ask an >>>>>>> intelligent question. But why are you making any claims at all about >>>>>>> TMs that don't exist?

How would you annotate all of the steps of the Linz Ĥ applied to its >>>>>> own machine description?

What new nonsense is this? No one is annotating "all of the steps" of a >>>>> TM. The annotations explain which formal statements apply in which
situations:
Ĥ.q0 ⟨Ĥ⟩ ⊢* ∞ if Ĥ applied to ⟨Ĥ⟩ halts, and >>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qn if Ĥ applied to ⟨Ĥ⟩ does not halt. >>>>

You skipped some Linz specified states.

Your annotations are still wrong. Mine (in fact Linz's) are the correct >>> ones regardless of whether I (or he) includes the states you are so
obsessed with.

As always you can dogmatically assert that I am wrong yet cannot
provide any evidence of my error because there is in fact no error.

What would be the point in copying here what Linz says in his book
again? I have, in fact, gone through the steps from the definition of
the problem to the two lines above but it had no effect. It's right
there in the book -- the simple steps from definition

H.q0 w ⊢* H.qy if H applied to w halts, and
H.q0 w ⊢* H.qn if H applied to w does not halt,

through the construction of H' and H^ to the conclusion above. Do you
think you'd pay attention this time if I went though it all again? No,
you just want to pretend that there is no "evidence" for what I say.

Have another go. See if you can write the two lines about Ĥ.q0 ⟨Ĥ⟩ >>> correctly with intermediate states you love so much.

When the halt decider at Ĥ.qx is a simulating halt decider

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞
if the simulated ⟨Ĥ⟩ applied to ⟨Ĥ⟩ halts, and

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
if the simulated ⟨Ĥ⟩ applied to ⟨Ĥ⟩ does not halt

Provided the first clause applies "if Ĥ applied to ⟨Ĥ⟩ halts", and the second one "if Ĥ applied to ⟨Ĥ⟩ does not halt", you can add any old guff
you like. So just make sure you say something like

That is not what it says and that is not what Linz says.

The halt decider is only at state Ĥ.qx and is only applied to two copies
of the TM description of Ĥ it cannot be applied to Ĥ itself, the input
must be a TM description and not a TM.

When the halt decider at Ĥ is a simulating halt decider then it
transitions to Ĥ.qn on the basis that the simulation of its first TM description ⟨Ĥ⟩ applied to its second TM description ⟨Ĥ⟩ never reaches
its final state whether or not the simulating halt decider at Ĥ.qx ever
stops simulating this input.



--
Copyright 2021 Pete Olcott

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)