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: Mon, 23 Jun 2025 10:02:32 +0300
Organization: -
Lines: 106
Message-ID: <103au67$13olm$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>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 23 Jun 2025 09:02:32 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="ff9eeb82472defb391a609f5929552bc";
	logging-data="1172150"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18mRbcAOs6g19fzUcQCwJwy"
User-Agent: Unison/2.2
Cancel-Lock: sha1:PEImDO1I4CN0wrvHhgnvbXNn13c=

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.

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

-- 
Mikko