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.

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

*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.

We know that the copy of H is at Ĥ.qx (AKA embedded_H) applies this
same criterion measure to every instance of embedded_H to any recursive
depth.

We know that this means that embedded_H is examining the behavior of Ĥ
applied to ⟨Ĥ⟩ as if embedded_H was (hypothetically) replaced by a UTM.

We know that the behavior of this hypothetical machine is the criterion
measure for embedded_H.

We know that Ĥ applied to ⟨Ĥ⟩ would never stop running if embedded_H was
replaced by a UTM because Ĥ applied to ⟨Ĥ⟩ copies its input then UTM ⟨Ĥ⟩
⟨Ĥ⟩ would repeat this cycle ...

We know that this means that when embedded_H computes the mapping from
its input ⟨Ĥ⟩ ⟨Ĥ⟩ to Ĥ.qy or Ĥ.qn on the basis 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

On 12/28/2021 6:32 PM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> *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
>
> You think the means something different to this:
>
> H.q0 wM w ⊢* H.qy iff M applied to w halts
> H.q0 wM w ⊢* H.qn iff M applied to w does not halt
>

I agree that the above two are the same.

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.

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

*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.

We know that the copy of H is at Ĥ.qx (AKA embedded_H) applies this
same criterion measure to every instance of embedded_H to any recursive
depth.

We know that this means that embedded_H is examining the behavior of Ĥ
applied to ⟨Ĥ⟩ as if embedded_H was (hypothetically) replaced by a UTM.

We know that the behavior of this hypothetical machine is the criterion
measure for embedded_H.

We know that Ĥ applied to ⟨Ĥ⟩ would never stop running if embedded_H was
replaced by a UTM because Ĥ applied to ⟨Ĥ⟩ copies its input then UTM ⟨Ĥ⟩
⟨Ĥ⟩ would repeat this cycle ...

We know that this means that when embedded_H computes the mapping from
its input ⟨Ĥ⟩ ⟨Ĥ⟩ to Ĥ.qy or Ĥ.qn on the basis 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