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

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-01 17:45 -0600
Organization	A noiseless patient Spider
Message-ID	<10looi8$6rti$1@dont-email.me> (permalink)
References	<10llfbr$33j0o$1@dont-email.me>

Cross-posted to 6 groups.

Show all headers | View raw

On 1/31/2026 11:49 AM, olcott wrote:
> 
> int DD()
> {
>    int Halt_Status = HHH(DD);
>    if (Halt_Status)
>      HERE: goto HERE;
>    return Halt_Status;
> }
> 

*I am stipulating that*
*I am stipulating that*
*I am stipulating that*
*I am stipulating that*

> 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.
> 


-- 
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

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