Groups | Search | Server Info | Login | Register


Groups > comp.software-eng > #3923

Re: Proof theoretic semantics based halt prover correctly rejects its input

Subject Re: Proof theoretic semantics based halt prover correctly rejects its input
Newsgroups comp.theory, sci.logic, sci.math, comp.lang.prolog, sci.lang, comp.software-eng
References <10llfbr$33j0o$1@dont-email.me> <10loc3o$2mjv$1@dont-email.me>
From Richard Damon <Richard@Damon-Family.org>
Message-ID <CuRfR.659142$ZkQ4.236143@fx47.iad> (permalink)
Organization Forte - www.forteinc.com
Date 2026-02-01 18:39 -0500

Cross-posted to 6 groups.

Show all headers | View raw


On 2/1/26 3:12 PM, olcott wrote:
>  > So. It the above the full definition of the "input program" or not.
> Look inside the C file to see the full definition of everything
> *It is total bullshit that you even ask for this*
> *It is total bullshit that you even ask for this*
> *It is total bullshit that you even ask for this*

So, what are you defining as "the program to decide on"?

Your reply just shows you don't understand what you are talking about.

Your STATEMENT of what DD is, says it is just the code you present, and 
your arguement needs for it to be just that, or you are caught in your 
lie about HHH not being what you claim it to be, sincd it is just a 
partial simulator that uses unsound logic to reach a wrong answer about 
the program when it actually is fully defined to what it needs to be to 
actually ask the question.

> 
> *The only thing that you need to know is that*
> *The only thing that you need to know is that*
> *The only thing that you need to know is that*
>  > HHH simulates DD step-by-step according to
>  > the semantics of the C programming language.

No it doesn't, as it doesn't SEE any "C Progrmming Language" to simulate.

Sorry, you are just proving how deranged you are.

It seens x86 code, that is the result of a C complier converting the C 
programming language.

And it doesn't "correctly simuate" that code, as it stops part way.

Since the CORRECT simulation of that exact code halts, their *IS* a 
proof that it is a halting input.

Thus your claims are just more of your lies, proving you just don't knwo 
what you are talking about, and are so disconnected from reality you 
have no idea what you are actually talking about.

> 
> On 1/31/2026 11:49 AM, 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.
>>
>> HHH correctly determines that DD does not have a well-founded
>> justification tree within Proof theoretic semantics.
>>
>> When HHH is construed as a proof theoretic halting prover
>> HHH detects the pathological-self-reference of its input and
>> rejects DD as non-well-founded on this basis.
>>
>> % 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 formally rejected by Prolog
>> occurs_check for this same reason.
>>
>> occurs_check correctly determines that LP does not
>> have a well-founded justification tree within Proof
>> theoretic semantics.
>>
> 
> 

Back to comp.software-eng | Previous | NextPrevious in thread | Next in thread | Find similar


Thread

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