On 25/04/2026 15:25, olcott wrote:>>>>>> That does not help if it is not known whether such sequence ofOn 4/25/2026 3:20 AM, Mikko wrote:
typedef int (*ptr)();The halting problem counter-example is grounded. One of the followinginference steps exists.>
It does help for the halting problem counter-example input
and it does help for the 1931 Incompleteness Theorem. Both
of these are ruled ungrounded rather than undecidable.
statements is true per the definition of "halting decider":
- The proposed decider accepts the counter-example.
- The proposed decider rejects the counter-example.
- The proposed decider is not a halting decider.
It is not necessary to know which one is true. Each one is sufficient
to infer that the propsed decider is not a halting decider.
Whether a halting oracle is possible is another problem. Accordint to
the CHurch-Turing thesis it isn't but there is no known proof.
int HHH(ptr P);
int DD()
{
int Halt_Status = HHH(DD);
if (Halt_Status)
HERE: goto HERE;
return Halt_Status;
}
int main()
{
HHH(DD);
}
Proof theoretic halt prover HHH is fully operational
code since 2022 can correctly rejects its input DD
as lacking a well-founded justification tree.
HHH is on line 1081
https://github.com/plolcott/x86utm/blob/master/Halt7.c
HHH is a proof-theoretic-semantics halt prover:
it accepts exactly those programs whose simulation
admits a finite, well-founded justification tree,
and rejects those whose simulation is non-well-founded.
Under the operational semantics of C as implemented
by HHH, the simulation of DD induces a recursive
self-reference cycle; therefore, no finite, well-founded
justification tree exists for DD under HHH.
--
Copyright 2026 Olcott
My 28 year goal has been to make
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
The complete structure of this system is now defined.
This required establishing a new foundation
Les messages affichés proviennent d'usenet.