Re: A simulating halt decider applied to the The Peter Linz Turing Machine description ⟨Ĥ⟩ -- key details

On 2024-06-01 19:26:55 +0000, olcott said:

On 6/1/2024 1:52 PM, joes wrote:

Am Sat, 01 Jun 2024 09:37:01 -0500 schrieb olcott:

On 6/1/2024 2:52 AM, Mikko wrote:

On 2024-05-31 15:35:18 +0000, olcott said:

 

*A quick summary of the reasoning provided below*
The LHS is behavior that embedded_H is allowed to report on.

There is no restrictions on what embedded_H is allowed to report on.

 embedded_H is only allowed to report on the behavior that its finite
string Turing Machine Description specifies to a UTM.
 embedded_H <is> a UTM except that it stops simulating and reports
non-halting as soon as it correctly recognizes a non-halting behavior
pattern that is specified by its input.

"Except". So it is not an UTM.
 

When Ĥ is applied to ⟨Ĥ⟩
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
 (a) Ĥ copies its input ⟨Ĥ⟩
(b) Ĥ invokes embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
(c) embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(d) simulated ⟨Ĥ⟩ copies its input ⟨Ĥ⟩
(e) simulated ⟨Ĥ⟩ invokes simulated embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
(f) simulated embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(g) goto (d)
 embedded_H is not allowed to be applied to Ĥ ⟨Ĥ⟩ because inputs can
only be finite strings and Ĥ is not a finite string. This means
that embedded_H is not allowed to report on its own actual behavior.

I can't read that notation. What is H^ and what does it look like?
 

 *Here is the whole Linz proof*
I simplified the Linz notation at the bottom of page 2 of the proof.
https://www.liarparadox.org/Linz_Proof.pdf

You are right, that is a sufficient proof. You may change the presentation
but then you must prove that your presentation is equivalent to Linz'.
--
Mikko