Re: Flibble’s Leap: Why Behavioral Divergence Implies a Type Distinction in the Halting Problem

On 5/12/25 11:22 AM, olcott wrote:

On 5/11/2025 9:48 AM, Mr Flibble wrote:

On Sun, 11 May 2025 15:44:44 +0100, Richard Heathfield wrote:
>

On 11/05/2025 14:21, Mr Flibble wrote:

This reframing dissolves the paradox by making the Halting Problem
itself an ill-posed question.

>
"P is a syntactically correct program in some well-defined
Turing-complete language. Does P stop when it is applied to this data
X?" is a meaningful and well-formed question. It's not a Carrollian
question like Olcott's "what time is it, yes or no?" It has a sensible
answer. Either P stops for X, or it doesn't.
>
It's a question that can in many (but not all) cases be answered quickly
and easily enough (and correctly) by humans, often requiring no more
than a brief glimpse. (I say 'not all' only because it is not beyond the
wit of mankind to trump up extraordinarily complicated and deliberately
obfuscated code that might easily defeat a programmer's casual glance.)
>
Some simple examples in K&R C:
>
main(){}
>
main(){for(;;);}
>
main(){puts("Hello");}
>
#include <stdio.h>
main(){long c=0;int ch; while((ch = getchar()) !=
EOF)++c;printf("%ld\n", c);} /* input: the complete works of Shakespeare
*/
>
Any competent C programmer can solve these at a glance - Halts, Loops,
Halts, Halts, in that order - so why shouldn't a programmer be able to?
>
The Halting Problem asks a more complicated question. ``Is it possible
to write a program that answers the above question for arbitrary P and
arbitrary X?"
>
Again, the question is meaningful and well-formed. It's syntactically
and grammatically adequate, and anyone claiming not to know what it
means is laying themselves open to a charge of disingenuousness. The
only difficult part is the answer, but there's nothing
self-contradictory or self-referential or paradoxical about the
question.

>
It is insufficient for the question to be syntactically correct, it needs
to be SEMANTICALLY correct too.
>
/Flibble

 A very important point.
Prolog detects that the Liar Paradox is semantically
incorrect because it specifies the same infinite
recursion as the Halting Problem proofs.

Meaningless, as Prolog can't handle the logic needed for the problem.

 Unlike formal systems that simply get stuck in
infinite recursion, algorithms are smarter. They
can detect and reject them.

but programs *ARE* "Formal Systems".

 Tarski anchored his whole undefinability theorem
in the nonsense of the Liar Paradox.
 

Nope, on the power of Godel's proof of incompleteness, allowing the existance of the Truth Predicate to force the system to need to define the results of the Liar's Paradox, which means the Truth Predicate can't exist.