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

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

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

 

 When Ĥ is applied to ⟨Ĥ⟩
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

 Of those two lines one is false.
As embedded_H is a copy of H both lines imply that H is not a halt decider.
 

*Formalizing the Linz Proof structure*
∃H  ∈ Turing_Machines
∀x  ∈ Turing_Machine_Descriptions
∀y  ∈ Finite_Strings
such that H(x,y) = Halts(x,y)

 As already noted, the above is not a part of a proof structure.
 

 Unless and until you provide reasoning to back that up it counts
as if you said nothing about it.