Re: embedded_H applied to ⟨Ĥ⟩ ⟨Ĥ⟩ computes the mapping from its input to Ĥ.qn

On 7/30/2024 1:37 AM, Mikko wrote:

On 2024-07-29 16:16:13 +0000, olcott said:
 

On 7/28/2024 3:02 AM, Mikko wrote:

On 2024-07-27 14:08:10 +0000, olcott said:
 

On 7/27/2024 2:21 AM, Mikko wrote:

On 2024-07-26 14:08:11 +0000, olcott said:
 

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

 

 The above is merely simplified syntax for the top of page 3
https://www.liarparadox.org/Linz_Proof.pdf
The above is the whole original Linz proof.

 And even more simplified semantics.
 

(a) Ĥ copies its input ⟨Ĥ⟩
(b) Ĥ invokes embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
(c) embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(d) simulated ⟨Ĥ⟩ copies its input ⟨Ĥ⟩
(e) simulated ⟨Ĥ⟩ invokes simulated embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
(f) simulated embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(g) goto (d) with one more level of simulation
 You are supposed to evaluate the above as a contiguous
sequence of moves such that non-halting behavior is
identified.

 The above is an obvious tight loop of (d), (e), (f), and (g).
Its relevance (it any) to the topic of the discussion is not
obvious.
 

 When we compute the mapping from the input to embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
to the behavior specified by this input we know that embedded_H
is correct to transition to Ĥ.qn.

 The meaning of "correct" in this context is that if the transition of
embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ to Ĥ.qn is correct if H ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to H.qn but
incorrect otherwise.

 No you are wrong.