Groups | Search | Server Info | Login | Register
Groups > comp.software-eng > #3969
| From | olcott <polcott333@gmail.com> |
|---|---|
| Newsgroups | comp.theory, sci.logic, sci.math, comp.lang.prolog, sci.lang, comp.software-eng |
| Subject | Re: Proof theoretic semantics based halt prover correctly rejects its input |
| Date | 2026-02-05 23:26 -0600 |
| Organization | A noiseless patient Spider |
| Message-ID | <10m3u2g$3s8cl$1@dont-email.me> (permalink) |
| References | (19 earlier) <10m3psr$3qssu$1@dont-email.me> <10m3qrc$3r86a$1@dont-email.me> <10m3r4k$3qssu$2@dont-email.me> <10m3sjn$3rnsa$1@dont-email.me> <10m3tpt$3s4vg$1@dont-email.me> |
Cross-posted to 6 groups.
On 2/5/2026 11:22 PM, dart200 wrote:
> On 2/5/26 9:01 PM, olcott wrote:
>> On 2/5/2026 10:36 PM, dart200 wrote:
>>> On 2/5/26 8:31 PM, olcott wrote:
>>>> On 2/5/2026 10:15 PM, dart200 wrote:
>>>>> On 2/5/26 8:08 PM, olcott wrote:
>>>>>> On 2/5/2026 9:23 PM, dart200 wrote:
>>>>>>> On 2/5/26 7:11 PM, olcott wrote:
>>>>>>>> On 2/5/2026 8:49 PM, dart200 wrote:
>>>>>>>>> On 2/5/26 12:20 PM, olcott wrote:
>>>>>>>>>> On 2/5/2026 12:06 PM, dart200 wrote:
>>>>>>>>>>> On 2/4/26 7:04 PM, olcott wrote:
>>>>>>>>>>>> On 2/4/2026 8:52 PM, dart200 wrote:
>>>>>>>>>>>>> On 2/4/26 6:50 PM, olcott wrote:
>>>>>>>>>>>>>> On 2/4/2026 8:42 PM, dart200 wrote:
>>>>>>>>>>>>>>> On 2/4/26 4:00 PM, olcott wrote:
>>>>>>>>>>>>>>>> On 2/4/2026 5:43 PM, dart200 wrote:
>>>>>>>>>>>>>>>>> On 2/4/26 2:27 PM, olcott wrote:
>>>>>>>>>>>>>>>>>> On 2/4/2026 4:19 PM, dart200 wrote:
>>>>>>>>>>>>>>>>>>> On 2/4/26 2:15 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>> On 2/4/2026 2:41 PM, dart200 wrote:
>>>>>>>>>>>>>>>>>>>>> On 2/1/26 9:35 AM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>> On 2/1/2026 6:11 AM, Richard Damon wrote:
>>>>>>>>>>>>>>>>>>>>>>> On 1/31/26 12:49 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>> Source code of fully operational system
>>>>>>>>>>>>>>>>>>>>>>>> https://github.com/plolcott/x86utm/blob/master/
>>>>>>>>>>>>>>>>>>>>>>>> Halt7.c
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> int DD()
>>>>>>>>>>>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>>>>>>>>>>> int Halt_Status = HHH(DD);
>>>>>>>>>>>>>>>>>>>>>>>> if (Halt_Status)
>>>>>>>>>>>>>>>>>>>>>>>> HERE: goto HERE;
>>>>>>>>>>>>>>>>>>>>>>>> return Halt_Status;
>>>>>>>>>>>>>>>>>>>>>>>> }
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> HHH simulates DD step-by-step according to
>>>>>>>>>>>>>>>>>>>>>>>> the semantics of the C programming language.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> IT CAN'T, as you have been told, as your above
>>>>>>>>>>>>>>>>>>>>>>> program, without the C CODE for HHH, has
>>>>>>>>>>>>>>>>>>>>>>> undefined behavior by the semantics of the C
>>>>>>>>>>>>>>>>>>>>>>> programming language.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> HHH as executed by polcott is exhibiting a
>>>>>>>>>>>>>>>>>>>>> classifier interface i'm calling a *partial
>>>>>>>>>>>>>>>>>>>>> recognizer*
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> (machine) -> {
>>>>>>>>>>>>>>>>>>>>> TRUE iff machine HALTS and DECIDABLE,
>>>>>>>>>>>>>>>>>>>>> FALSE iff machine LOOPS or UNDECIDABLE,
>>>>>>>>>>>>>>>>>>>>> }
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> it doesn't do so quite so intelligently, but
>>>>>>>>>>>>>>>>>>>>> HHH(DD) needs to return FALSE because DD is an
>>>>>>>>>>>>>>>>>>>>> UNDECIDABLE input to HHH
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> polcott does this by detecting the infinite
>>>>>>>>>>>>>>>>>>>>> recursion and returning FALSE because of that
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> this approach of returning FALSE upon encountering
>>>>>>>>>>>>>>>>>>>>> an infinite recursion on self (which i believe all
>>>>>>>>>>>>>>>>>>>>> paradoxes will involve) will either be accurate or
>>>>>>>>>>>>>>>>>>>>> inaccurate in regards to actually halting/ not...
>>>>>>>>>>>>>>>>>>>>> but it doesn't matter because returning FALSE for
>>>>>>>>>>>>>>>>>>>>> halting yet UNDECIDABLE input is acceptable for a
>>>>>>>>>>>>>>>>>>>>> *partial recognizer*
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> where this wouldn't work is:
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> int ND()
>>>>>>>>>>>>>>>>>>>>> {
>>>>>>>>>>>>>>>>>>>>> int Halt_Status = HHH(ND);
>>>>>>>>>>>>>>>>>>>>> return Halt_Status;
>>>>>>>>>>>>>>>>>>>>> }
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> HHH(ND) -> FALSE because HHH(ND) will recognize the
>>>>>>>>>>>>>>>>>>>>> infinite recursion and return FALSE ... but that's
>>>>>>>>>>>>>>>>>>>>> not an acceptable response for a *partial
>>>>>>>>>>>>>>>>>>>>> recognizer* for ND because ND is not an UNDECIDABLE
>>>>>>>>>>>>>>>>>>>>> input, and it clearly should HALT
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> sorry polcott
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> That is merely a text message that has not been
>>>>>>>>>>>>>>>>>>>> updated.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> See my other post:
>>>>>>>>>>>>>>>>>>>> When halt provers are allowed to reject bad
>>>>>>>>>>>>>>>>>>>> inputs the remaining domain is decidable
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> A bad input is any input that does not have
>>>>>>>>>>>>>>>>>>>> *a well-founded justification tree within Proof*
>>>>>>>>>>>>>>>>>>>> *theoretic semantics*
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> For a simulating halt prover as soon as it detects
>>>>>>>>>>>>>>>>>>>> that its simulated input cannot possibly reach its
>>>>>>>>>>>>>>>>>>>> own simulated final halt state for any reason
>>>>>>>>>>>>>>>>>>>> what-so-ever then this input <is> a bad input.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> so ur just banning self-referential analysis?
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> When we reject inputs not having
>>>>>>>>>>>>>>>>>> *a well-founded justification tree within Proof*
>>>>>>>>>>>>>>>>>> *theoretic semantics*
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Then undecidability utterly ceases to exist.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> i agree it's impossible to demonstrated undecidability
>>>>>>>>>>>>>>>>> without self- reference,
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> and filtering out paradoxes is a path to turing
>>>>>>>>>>>>>>>>> complete and fully decidable subset of turing machines,
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> but ND is a halting function, and i don't see a
>>>>>>>>>>>>>>>>> particular reason why a more intelligent HHH couldn't
>>>>>>>>>>>>>>>>> return that given a more in- depth analysis of how the
>>>>>>>>>>>>>>>>> self-reference interplays with the rest of the machine
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> It cannot do that because that is not what it sees.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> once it sees the infinite recursion on itself ...
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> why can't it do analysis on the effects of various
>>>>>>>>>>>>>>> possible return values for itself ... like what we do
>>>>>>>>>>>>>>> when we talk thru it?
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> The job of a simulating halt prover is to determine
>>>>>>>>>>>>>> whether or not it must abort its simulation to prevent
>>>>>>>>>>>>>> its own non-termination. If for-any-reason the answer
>>>>>>>>>>>>>> is yes then it is always correct to abort and reject
>>>>>>>>>>>>>> this input.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> it's still a partial recognizer, just with worse power than
>>>>>>>>>>>>> perhaps a more optimal one that can do more than just abort
>>>>>>>>>>>>> it's simulation, but upon doing so recognize the self-
>>>>>>>>>>>>> reference and perform more in- depth analysis beyond pure
>>>>>>>>>>>>> simulation.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> Like I tell the LLM systems it is a partial halt prover
>>>>>>>>>>>
>>>>>>>>>>> i simple see that a more powerful partial halting recognizer
>>>>>>>>>>> can return TRUE to the input ND just fine,
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> When an input does the opposite of whatever value
>>>>>>>>>
>>>>>>>>> bro u didn't read what i posted before, please refer to the
>>>>>>>>> definition:
>>>>>>>>>
>>>>>>>>> int ND()
>>>>>>>>> {
>>>>>>>>> int Halt_Status = HHH(ND);
>>>>>>>>> return Halt_Status;
>>>>>>>>> }
>>>>>>>>>
>>>>>>>>> *ND* does not do the oppose of whatever HHH(ND) reports , it
>>>>>>>>> halts regardless of what HHH(ND) reports.
>>>>>>>>>
>>>>>>>>> yet HHH will still fail to report it's behavior properly
>>>>>>>>> because HHH will decide that the self-referential recursion
>>>>>>>>> implies an infinite execution that doesn't actually execute.
>>>>>>>>>
>>>>>>>>
>>>>>>>> When HHH is a simulating proof theoretic halt prover (SPTHP)
>>>>>>>> any input that does not have a well-founded justification
>>>>>>>> tree is a bad input. Your input meets that requirement.
>>>>>>>
>>>>>>> yeah but clearly we can know what's going to happen here
>>>>>>>
>>>>>>> if ur theory doesn't capture that intuition somehow then i can't
>>>>>>> agree it's complete as much as it can be.
>>>>>>>
>>>>>>
>>>>>> All undecidability is an example of can't be proven.
>>>>>
>>>>> in computing: it's not that the output can't be computed, it's that
>>>>> the output can't be computed *thru a particular interface*
>>>>>
>>>>
>>>> Any input that does the opposite of whatever its
>>>> decider reports is merely the liar paradox in disguise.
>>>> After 2000 years there is not even an accepted
>>>> resolution to that.
>>>>
>>>> "This sentence in not true"
>>>> has the same truth value as this one:
>>>> "What time is it?"
>>>
>>> lol, but ND does not do the opposite and yet ur algo still messes it up
>>>
>>> ND is not a liar's paradox yet u still reject as invalid input
>>>
>>> sorry polcott, not buying it
>>>
>>
>> It is specifying recursive simulation to HHH.
>> You can accept that or deny that. The actual
>> truth remains the same either way.
>
> yeah but it's not contradicting the analysis so calling it a liar's
> paradox is wrong
>
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The liar paradox is also rejected because it does
not have a well-founded justification tree. Its
evaluation gets stuck in finite recursion.
--
Copyright 2026 Olcott<br><br>
My 28 year goal has been to make <br>
"true on the basis of meaning expressed in language"<br>
reliably computable for the entire body of knowledge.<br><br>
This required establishing a new foundation<br>
Back to comp.software-eng | Previous | Next — Previous in thread | Next in thread | Find similar
Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-01-31 11:49 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <news.x.richarddamon@xoxy.net> - 2026-02-01 07:11 -0500
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 11:35 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 13:31 -0500
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 12:36 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 13:48 -0500
Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-04 12:41 -0800
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-04 16:15 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-04 14:19 -0800
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-04 16:27 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-04 15:43 -0800
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-04 18:00 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-04 18:42 -0800
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-04 20:50 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-04 18:52 -0800
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-04 21:04 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 10:06 -0800
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-05 14:20 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 18:49 -0800
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-05 21:11 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 19:23 -0800
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-05 22:08 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 20:15 -0800
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-05 22:31 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 20:36 -0800
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-05 23:01 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 21:22 -0800
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-05 23:26 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input dart200 <user7160@newsgrouper.org.invalid> - 2026-02-05 23:42 -0800
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-06 08:58 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <news.x.richarddamon@xoxy.net> - 2026-02-06 10:21 -0500
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 13:35 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 15:03 -0500
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 14:12 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 18:39 -0500
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 17:45 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 18:55 -0500
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 18:00 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 19:15 -0500
Re: Proof theoretic semantics based halt prover correctly rejects its input olcott <polcott333@gmail.com> - 2026-02-01 18:28 -0600
Re: Proof theoretic semantics based halt prover correctly rejects its input Richard Damon <Richard@Damon-Family.org> - 2026-02-01 20:33 -0500
csiph-web