XPost: comp.theory, sci.logic, sci.math
For simplicity we will refer to the copy of Linz H at Ĥ.qx embedded_H.
Simplified syntax adapted from bottom of page 319:
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
Instead of defining what embedded_H actually does we are defining the
set of behaviors such that every embedded_H having these behaviors is necessarily correct.
It can be easily seen that the simulated input to embedded_H never
reaches the final state of this input no matter how many steps are
simulated.
These steps would keep repeating:
Ĥ copies its input ⟨Ĥ⟩ to ⟨Ĥ⟩ then embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩...
computation that halts
...the Turing machine will halt whenever it enters a final state (Linz:1990:234)
That a simulated input cannot possibly reach it final state conclusively
proves that this input never halts.
This proves that every simulating halt decider at Ĥ.qx that somehow
computes the mapping from its input ⟨Ĥ⟩ ⟨Ĥ⟩ to Ĥ.qn it is necessarily
correct.
Peter Linz HP Proof
https://www.liarparadox.org/Peter_Linz_HP_315-320.pdf
--
Copyright 2021 Pete Olcott
Talent hits a target no one else can hit;
Genius hits a target no one else can see.
Arthur Schopenhauer
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)