Path: news.eternal-september.org!eternal-september.org!feeder3.eternal-september.org!i2pn.org!i2pn2.org!.POSTED!not-for-mail
From: Richard Damon <richard@damon-family.org>
Newsgroups: comp.theory
Subject: Re: Can Moving the Paradox Code into the SHD Layer Reintroduce the
 Halting Problem?
Date: Sun, 25 May 2025 07:45:07 -0400
Organization: i2pn2 (i2pn.org)
Message-ID: <bbc04d123ea75da627f004b206fb53491bf9734b@i2pn2.org>
References: <XtBYP.501017$wBVe.207428@fx06.ams4>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sun, 25 May 2025 11:45:21 -0000 (UTC)
Injection-Info: i2pn2.org;
	logging-data="1858740"; mail-complaints-to="usenet@i2pn2.org";
	posting-account="diqKR1lalukngNWEqoq9/uFtbkm5U+w3w6FQ0yesrXg";
User-Agent: Mozilla Thunderbird
X-Spam-Checker-Version: SpamAssassin 4.0.0
In-Reply-To: <XtBYP.501017$wBVe.207428@fx06.ams4>
Content-Language: en-US

On 5/25/25 5:33 AM, Mr Flibble wrote:
> Can Moving the Paradox Code into the SHD Layer Reintroduce the Halting
> Problem?
> ================================================================================
> 
> Question:
> ---------
> In the neos solution (Flibble's typed SHD model), programs are split into
> two layers:
> - The SHD layer (meta-level) that analyzes programs.
> - The program layer that cannot reference the SHD.

Why do "Programs" has a SHD layer, since most programs don't use a SHD, 
and how can you tell if code *IS* a SHD. Why can't you just include a 
copy of the code of the SHD in the program layer?

> 
> What happens if you move the paradoxical construction (e.g., D() = if H(D)
> then loop) into the SHD layer itself?
> 
> Analysis:
> ---------
> 
> 1. Stratification Prevents Self-Reference (If Enforced)
> --------------------------------------------------------
> - Typed SHD systems (like Coq, Agda, or neos with layered semantics) can
> prevent self-reference by using type stratification.
> - In this setup, the SHD layer cannot analyze itself.
> - The construction of `D'` within the SHD layer, which calls `H(D')`,
> would be semantically ill-typed and rejected.
> 
> 2. If SHDs Can Analyze Themselves, the Paradox Returns
> -------------------------------------------------------
> - If SHDs are allowed to analyze other SHDs or themselves, you can
> reintroduce the diagonal construction:
>      D': if H(D') then loop forever; else halt;
> - This results in the same contradiction as in the classical halting
> problem proof.

Yes, which means if you can define the layers, you can't prove the 
correctness of the provers, as nothing can prove your top level prover 
to be correct.

> 
> Conclusion:
> -----------
> - Moving the paradox into the SHD layer only prevents the contradiction if
> the SHD layer is **itself** stratified and prevents self-analysis.

Yes, this is why Type Theory tend to define a hierarchy with an 
arbitrary number of layers.

> - The paradox is not avoided merely by code relocation—it is avoided by
> **semantic restriction**.
> - The issue is not *where* the paradox is written, but *what is allowed*
> in the system.
> 
> Final Verdict:
> --------------
> You can't escape the Halting Problem paradox simply by shifting the code
> to a different layer. You must redefine your system's rules to prevent any
> form of self-reference in all layers, including the SHD meta-level.
>