Path: news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: Re: HP counter-example INPUT cannot possibly exist --- Peter Linz HP Proof
Date: Tue, 24 Jun 2025 11:13:48 +0300
Organization: -
Lines: 120
Message-ID: <103dmns$1t7nc$1@dont-email.me>
References: <YpG1Q.1572310$4AM6.1293015@fx17.ams4> <ab53329d43e0587e58fe949b7a8f1dce83bb580f@i2pn2.org> <1027uhs$r7bj$2@dont-email.me> <6f1855be769b3afc319d871c0d451f381803ba5e@i2pn2.org> <1029hvm$1ah2f$1@dont-email.me> <102bhn6$1t2a1$1@dont-email.me> <102c462$20jl4$10@dont-email.me> <102e2p4$2iugr$1@dont-email.me> <102er47$2ohps$3@dont-email.me> <102gv1s$3cscf$1@dont-email.me> <102hgcp$3gqbm$3@dont-email.me> <102m36e$qohc$1@dont-email.me> <102mm8v$uef9$8@dont-email.me> <102ok6o$1gto6$1@dont-email.me> <102uj28$369b2$1@dont-email.me> <1030gop$3p2jt$1@dont-email.me> <10342se$4ms9$1@dont-email.me> <1035qea$vbnq$1@dont-email.me> <1036q7i$16lpk$1@dont-email.me> <1038et5$dttt$1@dont-email.me> <10399ck$k7rv$1@dont-email.me> <103au67$13olm$1@dont-email.me> <103bpu1$1a3c8$3@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 24 Jun 2025 10:13:49 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="8d9f0d7b9c49dad925bc9e96e863dc8a";
	logging-data="2006764"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/5Vd9RlOJURCpwdh3J1d2O"
User-Agent: Unison/2.2
Cancel-Lock: sha1:1xps4EbVWIlYsZYdtbADLdHrBBk=

On 2025-06-23 14:56:01 +0000, olcott said:

> On 6/23/2025 2:02 AM, Mikko wrote:
>> On 2025-06-22 16:01:23 +0000, olcott said:
>> 
>>> On 6/22/2025 3:29 AM, Mikko wrote:
>>>> On 2025-06-21 17:30:25 +0000, olcott said:
>>>> 
>>>>> On 6/21/2025 3:27 AM, Mikko wrote:
>>>>>> On 2025-06-20 16:39:40 +0000, olcott said:
>>>>>> 
>>>>>>> On 6/19/2025 3:12 AM, Mikko wrote:
>>>>>>>> 
>>>>>>>> But this is not. A proof starts with assumptions that may be true of
>>>>>>>> false. Each statement that is not a definition, axiom, postulate,
>>>>>>>> hypthesis or other assumption follows from some previous statements
>>>>>>>> by an inference rule. The conclusion of a proof is the last statement
>>>>>>>> of the sequence.
>>>>>>> 
>>>>>>> Some proofs begin with definitions instead of assumptions.
>>>>>> 
>>>>>> Definitions often enable a clearer presentation of the assumptions
>>>>>> and of the proof.
>>>>>> 
>>>>> 
>>>>> Some proofs begin with "assumptions" that are defined to be
>>>>> true, thus are not really mere assumptions at all.
>>>>> 
>>>>> <snip>>>>
>>>>>>>> Depending on the style of the proof one can ither prove that
>>>>>>>> the counter example exists or that if a halting decider exists
>>>>>>>> then the caunter example exists, too, and otherwise none is
>>>>>>>> needed.
>>>>>>> 
>>>>>>> No this is counter-factual.
>>>>>>> It has never been possible for *AN ACTUAL INPUT* to do
>>>>>>> the opposite of whatever value that it decider decides.
>>>>>>> *For 90 years no one ever bothered to notice this*
>>>>>> 
>>>>>> There is nothing impossible in Linz' construction of the
>>>>>> counter example. If you think there is you could tell us
>>>>>> the page, paragraph, and sentence in Linz' book that says
>>>>>> someting impossible.
>>>> 
>>>>> https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
>>>>> When M is applied to WM
>>>>> q0 WM ⊢* Ĥ q0 WM WM ⊢* Ĥ∞
>>>>>     if M applied to WM halts, and
>>>>> q0 WM ⊢* Ĥ q0 Wm WM ⊢* Ĥ y1 qn y2
>>>>>     if M applied to WM does not halt.
>>>>> 
>>>>> *From the bottom of page 319 has been adapted to this*
>>>>> When Ĥ is applied to ⟨Ĥ⟩
>>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.∞
>>>>>    if Ĥ applied to ⟨Ĥ⟩ halts
>>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>>>>>    if Ĥ applied to ⟨Ĥ⟩ does not halt
>>>>> 
>>>>> This does not have embedded_H reporting on the
>>>>> behavior specified by its input it has embedded_H
>>>>> reporting on its own behavior.
>>>>> 
>>>>> When embedded_H is a simulating partial halt decider
>>>>> then its transition to Ĥ.qn does correctly report that
>>>>> ⟨Ĥ⟩ ⟨Ĥ⟩ correctly simulated by embedded_H cannot possibly
>>>>> reach its own simulated final halt state of ⟨Ĥ.qn⟩.
>>>>> 
>>>>> *It does this even though embedded_H itself halts. embedded_H*
>>>>> *is not allowed to report on its own behavior. It is only*
>>>>> *allowed to report on the behavior that its input specifies*
>>>>> 
>>>>> When Ĥ is applied to ⟨Ĥ⟩ and embedded_H is a
>>>>> simulating partial halt decider
>>>>> (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 until
>>>>> embedded_H sees the repeating pattern and transitions to Ĥ.qn.
>>>>> 
>>>>> ⟨Ĥ⟩ ⟨Ĥ⟩ correctly simulated by embedded_H cannot possibly
>>>>> reach its own simulated final halt state of ⟨Ĥ.qn⟩ thus can
>>>>> never do the opposite of whatever embedded_H decides.
>>>>> https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
>>>> 
>>>> Nothing above shows that Ĥ cannot be consructed if H is given,
>>>> nor shows any error in the proof that Ĥ <Ĥ> halts if and only if
>>>> H <Ĥ> <Ĥ> says "does not halt".
>>>> 
>>> 
>>> The proof shows that Ĥ <Ĥ> halts when Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
>>> transitions to Ĥ.qn yet Ĥ <Ĥ> is not an input to Ĥ.embedded_H
>> 
>> Not "when" but "if". The proof does not prove that Ĥ <Ĥ> transitions
>> to Ĥ.qn. Instead it proves that if and only if H <Ĥ> <Ĥ> halts in H.qn
>> then Ĥ halts in Ĥ.qn.
>> 
> 
> When we hypothesize that Ĥ.embedded_H is a simulating PHD
> then we know that Ĥ.embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to H.qn
> 
>>> There has never been any HP proof where the actual input
>>> does the opposite of whatever its decider decides.
>> 
>> What proof needs to prove and does prove is that H <Ĥ> <Ĥ> does not
>> do what a halt decider is required to do, from which it then proves
>> that H is not a halt decider.
>> 
> 
> A halt decider is:
> (a) Required to report on its own behavior
> (b) Not allowed to report on its own behavior.

For some inputs (a), for other inputs (b).

-- 
Mikko