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

Proving that embedded_H at Ĥ.qx correctly maps its inputs ⟨Ĥ⟩ ⟨Ĥ⟩ to Ĥ.qn on the basis of the behavior of the UTM simulation of these inputs.

*My criterion measure with Ben's notational conventions*
H.q0 wM w ⊢* H.qy iff UTM(wM, w) halts
H.q0 wM w ⊢* H.qn iff UTM(wM, w) does not halt

We know that H would correctly decide the halt status of its input on
the basis of correctly deciding the halt status of the UTM simulation of
its input.

We know this because a UTM simulation of the Turing machine description
is computationally equivalent to the direct execution of this same
Turing machine.

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞ iff UTM(⟨Ĥ⟩ ⟨Ĥ⟩) at Ĥ.qx halts.
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn iff UTM(⟨Ĥ⟩ ⟨Ĥ⟩) at Ĥ.qx does not halt.

THIS IS WHERE PEOPLE GET STUCK
THIS IS WHERE PEOPLE GET STUCK
THIS IS WHERE PEOPLE GET STUCK

The criterion measure of H applies recursively such that the UTM would
simulate itself.

The following is the UTM simulation of a single input pair:
(a) copies its input ⟨Ĥ⟩ to ⟨Ĥ⟩
(b) simulates ⟨Ĥ⟩ applied to ⟨Ĥ⟩ with the UTM

We know that this means that when embedded_H computes the mapping from
its input ⟨Ĥ⟩ ⟨Ĥ⟩ to Ĥ.qy or Ĥ.qn on the basis of the behavior of the
UTM simulation of this input that its transition to Ĥ.qn is correct.

https://www.liarparadox.org/Peter_Linz_HP_315-320.pdf

Linz, Peter 1990. An Introduction to Formal Languages and Automata. Lexington/Toronto: D. C. Heath and Company. (315-320)

--
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)