From Newsgroup: comp.theory


A halt prover attempts to prove halting and when it
detects that the proof of its input does not form

*a well-founded justification tree within Proof*
*theoretic semantics*

Then it is correct to reject this input as bad data.

*Halting Problem and Proof Theoretic Semantics* https://www.researchgate.net/publication/400341134_Halting_Problem_and_Proof_Theoretic_Semantics


This change makes
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
--
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>

--- Synchronet 3.21b-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 2/4/26 11:47 AM, olcott wrote:

A halt prover attempts to prove halting and when it
detects that the proof of its input does not form

*a well-founded justification tree within Proof*
*theoretic semantics*

But Programs are not based on a "justification tree", so your definition
is just meaningles.

Then it is correct to reject this input as bad data.

No, it it correct to reject you concept as just a category error

*Halting Problem and Proof Theoretic Semantics*
https://www.researchgate.net/ publication/400341134_Halting_Problem_and_Proof_Theoretic_Semantics

This change makes
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.

Since your input just isn't a valid program. as it is incomplete, all
you are doing is proving your own stupidity.

It seems you just fundamentally don't understand that yoy neec to know
what you are talking about and use language properly.

This is what has made you just an ignorant pathological liar.
--- Synchronet 3.21b-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 04/02/2026 18:47, olcott wrote:

A halt prover attempts to prove halting

To prove that a computation halts is simple. Just show the execution
trace from the start to the halting. The hard problem is to prove
that an execution does not halt.

and when it detects that the proof of its input does not form

*a well-founded justification tree within Proof*
*theoretic semantics*

Then it is correct to reject this input as bad data.

No, that does not follow. That only means that it is correct to reject
the proof. The conclusion of the proof may still be correct.
--
Mikko
--- Synchronet 3.21b-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 2/5/2026 4:45 AM, Mikko wrote:

On 04/02/2026 18:47, olcott wrote:

A halt prover attempts to prove halting

To prove that a computation halts is simple. Just show the execution
trace from the start to the halting. The hard problem is to prove
that an execution does not halt.

and when it detects that the proof of its input does not form

*a well-founded justification tree within Proof*
*theoretic semantics*

Then it is correct to reject this input as bad data.

No, that does not follow. That only means that it is correct to reject
the proof. The conclusion of the proof may still be correct.

This same system makes
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
Proving that it was the right way to do this all along.
--
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>
--- Synchronet 3.21b-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 2/5/26 5:59 AM, olcott wrote:

On 2/5/2026 4:45 AM, Mikko wrote:

On 04/02/2026 18:47, olcott wrote:

A halt prover attempts to prove halting

To prove that a computation halts is simple. Just show the execution
trace from the start to the halting. The hard problem is to prove
that an execution does not halt.

and when it detects that the proof of its input does not form

*a well-founded justification tree within Proof*
*theoretic semantics*

Then it is correct to reject this input as bad data.

No, that does not follow. That only means that it is correct to reject
the proof. The conclusion of the proof may still be correct.

This same system makes
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
Proving that it was the right way to do this all along.

No it doesn't, as your "logic" tries to establish that words can have
their meaning changed, and thus "meaning" is no longer a term with meaning.

Sorry, you are just proving how stupid you are.
--- Synchronet 3.21b-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 2/5/26 6:28 AM, olcott wrote:

On 2/5/2026 4:45 AM, Mikko wrote:

On 04/02/2026 18:47, olcott wrote:

A halt prover attempts to prove halting

To prove that a computation halts is simple. Just show the execution
trace from the start to the halting. The hard problem is to prove
that an execution does not halt.

and when it detects that the proof of its input does not form

*a well-founded justification tree within Proof*
*theoretic semantics*

Then it is correct to reject this input as bad data.

No, that does not follow. That only means that it is correct to reject
the proof. The conclusion of the proof may still be correct.

The way that proofs work in proof theoretic
semantics is that they reject inputs not having
well-founded justification trees as bad data.

Is is the same as a truth predicate rejecting
True("What time is it?") as not truth-apt.

No, they don't.

The system just doesn't assign truth values to statements which can't be proven.

But then, not assigning truth values has impact on the semantics, and it
means that it can't actually talk about statements which you don't know
if they have truth values or not.

You are just proving that you don't understand what you are talking
about, but look at the world through your fantasy glasses that let you
only see what you want, even if that is nothing.
--- Synchronet 3.21b-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 05/02/2026 13:28, olcott wrote:

On 2/5/2026 4:45 AM, Mikko wrote:

On 04/02/2026 18:47, olcott wrote:

A halt prover attempts to prove halting

To prove that a computation halts is simple. Just show the execution
trace from the start to the halting. The hard problem is to prove
that an execution does not halt.

and when it detects that the proof of its input does not form

*a well-founded justification tree within Proof*
*theoretic semantics*

Then it is correct to reject this input as bad data.

No, that does not follow. That only means that it is correct to reject
the proof. The conclusion of the proof may still be correct.

The way that proofs work in proof theoretic
semantics is that they reject inputs not having
well-founded justification trees as bad data.

An example of a valid input is "42". That input has no justification, well-founded or otherwise. But there is no proof that would reject
"42" as bad data.
--
Mikko
--- Synchronet 3.21b-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 2/7/2026 4:15 AM, Mikko wrote:

On 06/02/2026 17:32, olcott wrote:

On 2/6/2026 3:15 AM, Mikko wrote:

On 05/02/2026 13:28, olcott wrote:

On 2/5/2026 4:45 AM, Mikko wrote:

On 04/02/2026 18:47, olcott wrote:

A halt prover attempts to prove halting

To prove that a computation halts is simple. Just show the execution >>>>> trace from the start to the halting. The hard problem is to prove
that an execution does not halt.

and when it detects that the proof of its input does not form

*a well-founded justification tree within Proof*
*theoretic semantics*

Then it is correct to reject this input as bad data.

No, that does not follow. That only means that it is correct to reject >>>>> the proof. The conclusion of the proof may still be correct.

The way that proofs work in proof theoretic
semantics is that they reject inputs not having
well-founded justification trees as bad data.

An example of a valid input is "42". That input has no justification,
well-founded or otherwise. But there is no proof that would reject
"42" as bad data.

It is an element of the set of natural numbers.

True, but non necessarily relevant to tthe proof. But the current
question is whether the proof rejects the input "42" as bad data.

Is the integer 42 a machine description that halts?
Reject.
--
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>
--- Synchronet 3.21b-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 2/7/26 8:08 AM, olcott wrote:

On 2/7/2026 4:15 AM, Mikko wrote:

On 06/02/2026 17:32, olcott wrote:

On 2/6/2026 3:15 AM, Mikko wrote:

On 05/02/2026 13:28, olcott wrote:

On 2/5/2026 4:45 AM, Mikko wrote:

On 04/02/2026 18:47, olcott wrote:

A halt prover attempts to prove halting

To prove that a computation halts is simple. Just show the execution >>>>>> trace from the start to the halting. The hard problem is to prove
that an execution does not halt.

and when it detects that the proof of its input does not form

*a well-founded justification tree within Proof*
*theoretic semantics*

Then it is correct to reject this input as bad data.

No, that does not follow. That only means that it is correct to
reject
the proof. The conclusion of the proof may still be correct.

The way that proofs work in proof theoretic
semantics is that they reject inputs not having
well-founded justification trees as bad data.

An example of a valid input is "42". That input has no justification,
well-founded or otherwise. But there is no proof that would reject
"42" as bad data.

It is an element of the set of natural numbers.

True, but non necessarily relevant to tthe proof. But the current
question is whether the proof rejects the input "42" as bad data.

Is the integer 42 a machine description that halts?
Reject.

But 42 might well be a machine description that halts, it depend on how
you have defined your encoding of a machine.
--- Synchronet 3.21b-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 2/7/2026 8:44 AM, Richard Damon wrote:

On 2/7/26 8:08 AM, olcott wrote:

On 2/7/2026 4:15 AM, Mikko wrote:

On 06/02/2026 17:32, olcott wrote:

On 2/6/2026 3:15 AM, Mikko wrote:

On 05/02/2026 13:28, olcott wrote:

On 2/5/2026 4:45 AM, Mikko wrote:

On 04/02/2026 18:47, olcott wrote:

A halt prover attempts to prove halting

To prove that a computation halts is simple. Just show the execution >>>>>>> trace from the start to the halting. The hard problem is to prove >>>>>>> that an execution does not halt.

and when it detects that the proof of its input does not form

*a well-founded justification tree within Proof*
*theoretic semantics*

Then it is correct to reject this input as bad data.

No, that does not follow. That only means that it is correct to >>>>>>> reject
the proof. The conclusion of the proof may still be correct.

The way that proofs work in proof theoretic
semantics is that they reject inputs not having
well-founded justification trees as bad data.

An example of a valid input is "42". That input has no justification, >>>>> well-founded or otherwise. But there is no proof that would reject
"42" as bad data.

It is an element of the set of natural numbers.

True, but non necessarily relevant to tthe proof. But the current
question is whether the proof rejects the input "42" as bad data.

Is the integer 42 a machine description that halts?
Reject.

But 42 might well be a machine description that halts, it depend on how
you have defined your encoding of a machine.

Can't be the shortest one is a single quintuple.
--
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>
--- Synchronet 3.21b-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 2/7/26 10:08 AM, olcott wrote:

On 2/7/2026 8:44 AM, Richard Damon wrote:

On 2/7/26 8:08 AM, olcott wrote:

On 2/7/2026 4:15 AM, Mikko wrote:

On 06/02/2026 17:32, olcott wrote:

On 2/6/2026 3:15 AM, Mikko wrote:

On 05/02/2026 13:28, olcott wrote:

On 2/5/2026 4:45 AM, Mikko wrote:

On 04/02/2026 18:47, olcott wrote:

A halt prover attempts to prove halting

To prove that a computation halts is simple. Just show the
execution
trace from the start to the halting. The hard problem is to prove >>>>>>>> that an execution does not halt.

and when it detects that the proof of its input does not form >>>>>>>>>
*a well-founded justification tree within Proof*
*theoretic semantics*

Then it is correct to reject this input as bad data.

No, that does not follow. That only means that it is correct to >>>>>>>> reject
the proof. The conclusion of the proof may still be correct.

The way that proofs work in proof theoretic
semantics is that they reject inputs not having
well-founded justification trees as bad data.

An example of a valid input is "42". That input has no justification, >>>>>> well-founded or otherwise. But there is no proof that would reject >>>>>> "42" as bad data.

It is an element of the set of natural numbers.

True, but non necessarily relevant to tthe proof. But the current
question is whether the proof rejects the input "42" as bad data.

Is the integer 42 a machine description that halts?
Reject.

But 42 might well be a machine description that halts, it depend on
how you have defined your encoding of a machine.

Can't be the shortest one is a single quintuple.

Which can be encoded into a single number.

I guess you don't understand how to encode things.
--- Synchronet 3.21b-Linux NewsLink 1.2

From Newsgroup: comp.theory

On 07/02/2026 15:08, olcott wrote:

On 2/7/2026 4:15 AM, Mikko wrote:

On 06/02/2026 17:32, olcott wrote:

On 2/6/2026 3:15 AM, Mikko wrote:

On 05/02/2026 13:28, olcott wrote:

On 2/5/2026 4:45 AM, Mikko wrote:

On 04/02/2026 18:47, olcott wrote:

A halt prover attempts to prove halting

To prove that a computation halts is simple. Just show the execution >>>>>> trace from the start to the halting. The hard problem is to prove
that an execution does not halt.

and when it detects that the proof of its input does not form

*a well-founded justification tree within Proof*
*theoretic semantics*

Then it is correct to reject this input as bad data.

No, that does not follow. That only means that it is correct to
reject
the proof. The conclusion of the proof may still be correct.

The way that proofs work in proof theoretic
semantics is that they reject inputs not having
well-founded justification trees as bad data.

An example of a valid input is "42". That input has no justification,
well-founded or otherwise. But there is no proof that would reject
"42" as bad data.

It is an element of the set of natural numbers.

True, but non necessarily relevant to tthe proof. But the current
question is whether the proof rejects the input "42" as bad data.

Is the integer 42 a machine description that halts?
Reject.

The question is already answered above: "42" is an input not having
a well-founded justification tree, or at least none that I know.
--
Mikko
--- Synchronet 3.21b-Linux NewsLink 1.2