On 2/29/24 3:08 PM, olcott wrote:
On 2/29/2024 1:28 PM, Mikko wrote:
On 2024-02-29 10:31:13 +0000, immibis said:
On 28/02/24 23:18, olcott wrote:
// Ĥ.q0 ⟨Ĥ⟩ copies its input then transitions to Ĥ.Hq0
// Ĥ.Hq0 is the first state of The Linz hypothetical halt decider
// H transitions to Ĥ.Hqy for halts and Ĥ.Hqn for does not halt
// ∞ means an infinite loop has been appended to the Ĥ.Hqy state
//
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn // Ĥ applied to ⟨Ĥ⟩ does not
halt
When Ĥ is applied to ⟨Ĥ⟩ it contradicts whatever value that Ĥ.H >>>> returns making Ĥ self-contradictory.
Turing machine/input pairs are never self-contradictory. Ĥ is only
contradictory with its intended specification, which is not itself.
There is no intended specification of Ĥ.
Assuming that Peter Linz has a mind then he intended this specification
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn // Ĥ applied to ⟨Ĥ⟩ does not halt
But the comments are the carry over of the specification of H.
H^ exists if, and only if, H is defined.
If you shows that an H^ meeting that "specification" fails to exist,
then H must not exist either.
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)