Re: Proof that H(D,D) meets its abort criteria --Categorically Exhaustive Reasoning--

On 3/16/2024 2:57 PM, immibis wrote:

On 16/03/24 19:57, olcott wrote:

On 3/16/2024 12:33 PM, immibis wrote:

On 16/03/24 18:04, olcott wrote:

On 3/16/2024 11:53 AM, Richard Damon wrote:

It is a NON-COMPUTABLE requriment.
>
That is not INVALID.
>

>
None-the-less it <is> what you keep insisting is required.

>
To make a halting decider, it is required to compute this requirement.
>
This requirement cannot be computed, so halting deciders cannot be made.

>
In the same {logical impossibility} sort of way that no CAD system can correctly draw a square circle

 That's correct. No CAD system can correctly draw a square circle.
 

and no one can correctly answer this question:
Is this sentence true or false: "This sentence is not true" ?

 This sentence cannot be written in mathematical logic. It is well-known that English contains ambiguous sentences.
 

https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF LP := ~True(LP) is correctly formalized in MTT.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Prolog correctly determines that the structure of the above Prolog expression: "ends up standing for some kind of infinite structure"
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer