On 13/01/2026 16:17, olcott wrote:
On 1/13/2026 2:46 AM, Mikko wrote:
On 12/01/2026 16:43, olcott wrote:
On 1/12/2026 4:51 AM, Mikko wrote:
On 11/01/2026 16:23, olcott wrote:
On 1/11/2026 4:22 AM, Mikko wrote:
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:It is a perfectly valid question to ask whther a particular
On 09/01/2026 17:52, olcott wrote:
On 1/9/2026 3:59 AM, Mikko wrote:
On 08/01/2026 16:22, olcott wrote:
On 1/8/2026 4:22 AM, Mikko wrote:The misconception is yours. No expression in the language of >>>>>>>>>>> the first
On 07/01/2026 13:54, olcott wrote:
On 1/7/2026 5:49 AM, Mikko wrote:Depends on whether the word "truth" is interpeted in the >>>>>>>>>>>>> standard
On 07/01/2026 06:44, olcott wrote:*if undecidability is correct then truth itself is broken* >>>>>>>>>>>>>
All deciders essentially: Transform finite string >>>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>>> {Accept, Reject} values.
The counter-example input to requires more than >>>>>>>>>>>>>>>> can be derived from finite string transformation >>>>>>>>>>>>>>>> rules applied to this specific input thus the
Halting Problem requires too much.
In a sense the halting problem asks too much: the problem >>>>>>>>>>>>>>> is proven to
be unsolvable. In another sense it asks too little: >>>>>>>>>>>>>>> usually we want to
know whether a method halts on every input, not just one. >>>>>>>>>>>>>>>
Although the halting problem is unsolvable, there are >>>>>>>>>>>>>>> partial solutions
to the halting problem. In particular, every counter- >>>>>>>>>>>>>>> example to the
full solution is correctly solved by some partial deciders. >>>>>>>>>>>>>>
sense or in Olcott's sense.
Undecidability is misconception. Self-contradictory
expressions are correctly rejected as semantically
incoherent thus form no undecidability or incompleteness. >>>>>>>>>>>
order group theory is self-contradictory. But the first order >>>>>>>>>>> goupr
theory is incomplete: it is impossible to prove that AB = BA >>>>>>>>>>> is true
for every A and every B but it is also impossible to prove >>>>>>>>>>> that AB = BA
is false for some A and some B.
All deciders essentially: Transform finite string
inputs by finite string transformation rules into
{Accept, Reject} values.
When a required result cannot be derived by applying
finite string transformation rules to actual finite
string inputs, then the required result exceeds the
scope of computation and must be rejected as an
incorrect requirement.
No, that does not follow. If a required result cannot be
derived by
appying a finite string transformation then the it it is
uncomputable.
Right. Outside the scope of computation. Requiring anything
outside the scope of computation is an incorrect requirement.
Of course, it one can prove that the required result is not >>>>>>>>> computable
then that helps to avoid wasting effort to try the impossible. The >>>>>>>>> situation is worse if it is not known that the required result >>>>>>>>> is not
computable.
That something is not computable does not mean that there is >>>>>>>>> anyting
"incorrect" in the requirement.
Yes it certainly does. Requiring the impossible is always an error. >>>>>>>
reuqirement
is satisfiable.
Any yes/no question lacking a correct yes/no answer
is an incorrect question that must be rejected on
that basis.
Irrelevant. The question whether a particular requirement is
satisfiable
does have an answer that is either "yes" or "no". In some ases it is >>>>> not known whether it is "yes" or "no" and there may be no known way to >>>>> find out be even then either "yes" or "no" is the correct answer.
Now that I finally have the standard terminology:
Proof-theoretic semantics has always been the correct
formal system to handle decision problems.
When it is asked a yes/no question lacking a correct
yes/no answer it correctly determines non-well-founded.
I have been correct all along and merely lacked the
standard terminology.
Irrelevant, as already noted above.
It is not irrelevant at all. Most all of undecidability
cease to exist in this system:
It does not help if the system is not sound. Or if the particuar undecidability that one happens to care about does not cease to
exist.
On 1/14/2026 3:04 AM, Mikko wrote:
On 13/01/2026 16:17, olcott wrote:
On 1/13/2026 2:46 AM, Mikko wrote:
On 12/01/2026 16:43, olcott wrote:
On 1/12/2026 4:51 AM, Mikko wrote:
On 11/01/2026 16:23, olcott wrote:
On 1/11/2026 4:22 AM, Mikko wrote:
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:
On 09/01/2026 17:52, olcott wrote:
On 1/9/2026 3:59 AM, Mikko wrote:
On 08/01/2026 16:22, olcott wrote:
On 1/8/2026 4:22 AM, Mikko wrote:The misconception is yours. No expression in the language of >>>>>>>>>>>> the first
On 07/01/2026 13:54, olcott wrote:
On 1/7/2026 5:49 AM, Mikko wrote:Depends on whether the word "truth" is interpeted in the >>>>>>>>>>>>>> standard
On 07/01/2026 06:44, olcott wrote:*if undecidability is correct then truth itself is broken* >>>>>>>>>>>>>>
All deciders essentially: Transform finite string >>>>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>>>> {Accept, Reject} values.
The counter-example input to requires more than >>>>>>>>>>>>>>>>> can be derived from finite string transformation >>>>>>>>>>>>>>>>> rules applied to this specific input thus the >>>>>>>>>>>>>>>>> Halting Problem requires too much.
In a sense the halting problem asks too much: the >>>>>>>>>>>>>>>> problem is proven to
be unsolvable. In another sense it asks too little: >>>>>>>>>>>>>>>> usually we want to
know whether a method halts on every input, not just one. >>>>>>>>>>>>>>>>
Although the halting problem is unsolvable, there are >>>>>>>>>>>>>>>> partial solutions
to the halting problem. In particular, every counter- >>>>>>>>>>>>>>>> example to the
full solution is correctly solved by some partial deciders. >>>>>>>>>>>>>>>
sense or in Olcott's sense.
Undecidability is misconception. Self-contradictory
expressions are correctly rejected as semantically
incoherent thus form no undecidability or incompleteness. >>>>>>>>>>>>
order group theory is self-contradictory. But the first >>>>>>>>>>>> order goupr
theory is incomplete: it is impossible to prove that AB = BA >>>>>>>>>>>> is true
for every A and every B but it is also impossible to prove >>>>>>>>>>>> that AB = BA
is false for some A and some B.
All deciders essentially: Transform finite string
inputs by finite string transformation rules into
{Accept, Reject} values.
When a required result cannot be derived by applying
finite string transformation rules to actual finite
string inputs, then the required result exceeds the
scope of computation and must be rejected as an
incorrect requirement.
No, that does not follow. If a required result cannot be
derived by
appying a finite string transformation then the it it is
uncomputable.
Right. Outside the scope of computation. Requiring anything
outside the scope of computation is an incorrect requirement. >>>>>>>>>
Of course, it one can prove that the required result is not >>>>>>>>>> computable
then that helps to avoid wasting effort to try the impossible. >>>>>>>>>> The
situation is worse if it is not known that the required result >>>>>>>>>> is not
computable.
That something is not computable does not mean that there is >>>>>>>>>> anyting
"incorrect" in the requirement.
Yes it certainly does. Requiring the impossible is always an >>>>>>>>> error.
It is a perfectly valid question to ask whther a particular
reuqirement
is satisfiable.
Any yes/no question lacking a correct yes/no answer
is an incorrect question that must be rejected on
that basis.
Irrelevant. The question whether a particular requirement is
satisfiable
does have an answer that is either "yes" or "no". In some ases it is >>>>>> not known whether it is "yes" or "no" and there may be no known
way to
find out be even then either "yes" or "no" is the correct answer.
Now that I finally have the standard terminology:
Proof-theoretic semantics has always been the correct
formal system to handle decision problems.
When it is asked a yes/no question lacking a correct
yes/no answer it correctly determines non-well-founded.
I have been correct all along and merely lacked the
standard terminology.
Irrelevant, as already noted above.
It is not irrelevant at all. Most all of undecidability
cease to exist in this system:
It does not help if the system is not sound. Or if the particuar
undecidability that one happens to care about does not cease to
exist.
Soundness is exactly why proofrCatheoretic semantics matters here.
When meaning is grounded in inferential structure and truth is anchored
in an axiomatic base, only wellrCafounded expressions are admissible.
On 14/01/2026 21:32, olcott wrote:
On 1/14/2026 3:01 AM, Mikko wrote:
On 13/01/2026 16:31, olcott wrote:
On 1/13/2026 3:13 AM, Mikko wrote:
On 12/01/2026 16:32, olcott wrote:
On 1/12/2026 4:47 AM, Mikko wrote:
On 11/01/2026 16:24, Tristan Wibberley wrote:
On 11/01/2026 10:13, Mikko wrote:For pracitcal programming it is useful to know what is known to be >>>>>>> uncomputable in order to avoid wasting time in attemlpts to do the >>>>>>> impossible.
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:
You can't determine whether the required result is computable >>>>>>>>> beforeNo, that does not follow. If a required result cannot be >>>>>>>>>>> derived by
appying a finite string transformation then the it it is >>>>>>>>>>> uncomputable.
Right. Outside the scope of computation. Requiring anything >>>>>>>>>> outside the scope of computation is an incorrect requirement. >>>>>>>>>
you have the requirement.
Right, it is /in/ scope for computer science... for the /ology/. >>>>>>>> Olcott
here uses "computation" to refer to the practice. You give the >>>>>>>> requirement to the /ologist/ who correctly decides that it is >>>>>>>> not for
computation because it is not computable.
You two so often violently agree; I find it warming to the heart. >>>>>>>
It f-cking nuts that after more than 2000 years
people still don't understand that self-contradictory
expressions: "This sentence is not true" have no
truth value. A smart high school student should have
figured this out 2000 years ago.
Irrelevant. For practical programming that question needn't be
answered.
The halting problem counter-example input is anchored
in the Liar Paradox. Proof Theoretic Semantics rejects
those two and G||del's incompleteness and a bunch more
as merely non-well-founded inputs.
For every Turing machine the halting problem counter-example provably
exists.
Not when using Proof Theoretic Semantics grounded
in the specification language. In this case the
pathological input is simply rejected as ungrounded.
Then your "Proof Theoretic Semantics" is not useful for discussion of
Turing machines. For every Turing machine a counter example exists.
And so exists a Turing machine that writes the counter example when
given a Turing machine as input.
On 14/01/2026 19:28, olcott wrote:
On 1/14/2026 1:40 AM, Mikko wrote:
On 13/01/2026 16:27, olcott wrote:
On 1/13/2026 3:11 AM, Mikko wrote:
On 12/01/2026 16:29, olcott wrote:
On 1/12/2026 4:44 AM, Mikko wrote:
On 11/01/2026 16:18, olcott wrote:
On 1/11/2026 4:13 AM, Mikko wrote:
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:You can't determine whether the required result is computable >>>>>>>>> before
On 09/01/2026 17:52, olcott wrote:
On 1/9/2026 3:59 AM, Mikko wrote:
On 08/01/2026 16:22, olcott wrote:
On 1/8/2026 4:22 AM, Mikko wrote:The misconception is yours. No expression in the language >>>>>>>>>>>>> of the first
On 07/01/2026 13:54, olcott wrote:
On 1/7/2026 5:49 AM, Mikko wrote:Depends on whether the word "truth" is interpeted in the >>>>>>>>>>>>>>> standard
On 07/01/2026 06:44, olcott wrote:
All deciders essentially: Transform finite string >>>>>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>>>>> {Accept, Reject} values.
The counter-example input to requires more than >>>>>>>>>>>>>>>>>> can be derived from finite string transformation >>>>>>>>>>>>>>>>>> rules applied to this specific input thus the >>>>>>>>>>>>>>>>>> Halting Problem requires too much.
In a sense the halting problem asks too much: the >>>>>>>>>>>>>>>>> problem is proven to
be unsolvable. In another sense it asks too little: >>>>>>>>>>>>>>>>> usually we want to
know whether a method halts on every input, not just one. >>>>>>>>>>>>>>>>>
Although the halting problem is unsolvable, there are >>>>>>>>>>>>>>>>> partial solutions
to the halting problem. In particular, every counter- >>>>>>>>>>>>>>>>> example to the
full solution is correctly solved by some partial >>>>>>>>>>>>>>>>> deciders.
*if undecidability is correct then truth itself is broken* >>>>>>>>>>>>>>>
sense or in Olcott's sense.
Undecidability is misconception. Self-contradictory >>>>>>>>>>>>>> expressions are correctly rejected as semantically >>>>>>>>>>>>>> incoherent thus form no undecidability or incompleteness. >>>>>>>>>>>>>
order group theory is self-contradictory. But the first >>>>>>>>>>>>> order goupr
theory is incomplete: it is impossible to prove that AB = >>>>>>>>>>>>> BA is true
for every A and every B but it is also impossible to prove >>>>>>>>>>>>> that AB = BA
is false for some A and some B.
All deciders essentially: Transform finite string
inputs by finite string transformation rules into
{Accept, Reject} values.
When a required result cannot be derived by applying
finite string transformation rules to actual finite
string inputs, then the required result exceeds the
scope of computation and must be rejected as an
incorrect requirement.
No, that does not follow. If a required result cannot be >>>>>>>>>>> derived by
appying a finite string transformation then the it it is >>>>>>>>>>> uncomputable.
Right. Outside the scope of computation. Requiring anything >>>>>>>>>> outside the scope of computation is an incorrect requirement. >>>>>>>>>
you have the requirement.
*Computation and Undecidability*
https://philpapers.org/go.pl?aid=OLCCAU
We know that there does not exist any finite
string transformations that H can apply to its
input P to derive the halt status of any P
that does the opposite of whatever H returns.
Which only nmakes sense when the requirement that H must determine >>>>>>> whether the computation presented by its input halts has already >>>>>>> been presented.
*ChatGPT explains how and why I am correct*
-a-a *Reinterpretation of undecidability*
-a-a The example of P and H demonstrates that what is
-a-a often called rCLundecidablerCY is better understood as
-a-a ill-posed with respect to computable semantics.
-a-a When the specification is constrained to properties
-a-a detectable via finite simulation and finite pattern
-a-a recognition, computation proceeds normally and
-a-a correctly. Undecidability only appears when the
-a-a specification overreaches that boundary.
It tries to explain but it does not prove.
Its the same thing that I have been saying for years.
It is not that a universal halt decider cannot exist.
It is proven that an universal halt decider does not exist.
rCLThe system adopts Proof-Theoretic Semantics: meaning is determined >>>> by inferential role, and truth is internal to the theory. A theory T
is defined by a finite set of stipulated atomic statements together
with all expressions derivable from them under the inference rules.
The statements belonging to T constitute its theorems, and these are
exactly the statements that are true-in-T.rCY
Under a system like the above rough draft all inputs
having pathological self reference such as the halting
problem counter-example input are simply rejected as
non-well-founded. Tarski Undefinability, G||del's
incompleteness and the halting problem cease to exist.
A Turing
machine cannot determine the halting of all Turing machines and is
therefore not an universla halt decider.
This is not true in Proof Theoretic Semantics. I
still have to refine my words. I may not have said
that exactly correctly. The result is that in Proof
Theoretic Semantics the counter-example is rejected
as non-well-founded.
That no Turing machine is a halt decider is a proven theorem and a
truth about Turing machines. If your "Proof Thoeretic Semnatics"
does not regard it as true then your "Proof Theoretic Semantics"
is incomplete.
My longrCaterm goal is to make rCytrue on the basis of meaningrCO computable.
As meaning is not computable, how can "true on the balsis of meaning"
be commputable?
On 1/15/2026 3:48 AM, Mikko wrote:
On 14/01/2026 19:28, olcott wrote:
On 1/14/2026 1:40 AM, Mikko wrote:
On 13/01/2026 16:27, olcott wrote:
On 1/13/2026 3:11 AM, Mikko wrote:
On 12/01/2026 16:29, olcott wrote:
On 1/12/2026 4:44 AM, Mikko wrote:
On 11/01/2026 16:18, olcott wrote:
On 1/11/2026 4:13 AM, Mikko wrote:
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:You can't determine whether the required result is computable >>>>>>>>>> before
On 09/01/2026 17:52, olcott wrote:
On 1/9/2026 3:59 AM, Mikko wrote:
On 08/01/2026 16:22, olcott wrote:
On 1/8/2026 4:22 AM, Mikko wrote:The misconception is yours. No expression in the language >>>>>>>>>>>>>> of the first
On 07/01/2026 13:54, olcott wrote:
On 1/7/2026 5:49 AM, Mikko wrote:Depends on whether the word "truth" is interpeted in the >>>>>>>>>>>>>>>> standard
On 07/01/2026 06:44, olcott wrote:
All deciders essentially: Transform finite string >>>>>>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>>>>>> {Accept, Reject} values.
The counter-example input to requires more than >>>>>>>>>>>>>>>>>>> can be derived from finite string transformation >>>>>>>>>>>>>>>>>>> rules applied to this specific input thus the >>>>>>>>>>>>>>>>>>> Halting Problem requires too much.
In a sense the halting problem asks too much: the >>>>>>>>>>>>>>>>>> problem is proven to
be unsolvable. In another sense it asks too little: >>>>>>>>>>>>>>>>>> usually we want to
know whether a method halts on every input, not just one. >>>>>>>>>>>>>>>>>>
Although the halting problem is unsolvable, there are >>>>>>>>>>>>>>>>>> partial solutions
to the halting problem. In particular, every counter- >>>>>>>>>>>>>>>>>> example to the
full solution is correctly solved by some partial >>>>>>>>>>>>>>>>>> deciders.
*if undecidability is correct then truth itself is broken* >>>>>>>>>>>>>>>>
sense or in Olcott's sense.
Undecidability is misconception. Self-contradictory >>>>>>>>>>>>>>> expressions are correctly rejected as semantically >>>>>>>>>>>>>>> incoherent thus form no undecidability or incompleteness. >>>>>>>>>>>>>>
order group theory is self-contradictory. But the first >>>>>>>>>>>>>> order goupr
theory is incomplete: it is impossible to prove that AB = >>>>>>>>>>>>>> BA is true
for every A and every B but it is also impossible to prove >>>>>>>>>>>>>> that AB = BA
is false for some A and some B.
All deciders essentially: Transform finite string
inputs by finite string transformation rules into
{Accept, Reject} values.
When a required result cannot be derived by applying >>>>>>>>>>>>> finite string transformation rules to actual finite
string inputs, then the required result exceeds the
scope of computation and must be rejected as an
incorrect requirement.
No, that does not follow. If a required result cannot be >>>>>>>>>>>> derived by
appying a finite string transformation then the it it is >>>>>>>>>>>> uncomputable.
Right. Outside the scope of computation. Requiring anything >>>>>>>>>>> outside the scope of computation is an incorrect requirement. >>>>>>>>>>
you have the requirement.
*Computation and Undecidability*
https://philpapers.org/go.pl?aid=OLCCAU
We know that there does not exist any finite
string transformations that H can apply to its
input P to derive the halt status of any P
that does the opposite of whatever H returns.
Which only nmakes sense when the requirement that H must determine >>>>>>>> whether the computation presented by its input halts has already >>>>>>>> been presented.
*ChatGPT explains how and why I am correct*
-a-a *Reinterpretation of undecidability*
-a-a The example of P and H demonstrates that what is
-a-a often called rCLundecidablerCY is better understood as
-a-a ill-posed with respect to computable semantics.
-a-a When the specification is constrained to properties
-a-a detectable via finite simulation and finite pattern
-a-a recognition, computation proceeds normally and
-a-a correctly. Undecidability only appears when the
-a-a specification overreaches that boundary.
It tries to explain but it does not prove.
Its the same thing that I have been saying for years.
It is not that a universal halt decider cannot exist.
It is proven that an universal halt decider does not exist.
rCLThe system adopts Proof-Theoretic Semantics: meaning is determined >>>>> by inferential role, and truth is internal to the theory. A theory
T is defined by a finite set of stipulated atomic statements
together with all expressions derivable from them under the
inference rules. The statements belonging to T constitute its
theorems, and these are exactly the statements that are true-in-T.rCY >>>>>
Under a system like the above rough draft all inputs
having pathological self reference such as the halting
problem counter-example input are simply rejected as
non-well-founded. Tarski Undefinability, G||del's
incompleteness and the halting problem cease to exist.
A Turing
machine cannot determine the halting of all Turing machines and is >>>>>> therefore not an universla halt decider.
This is not true in Proof Theoretic Semantics. I
still have to refine my words. I may not have said
that exactly correctly. The result is that in Proof
Theoretic Semantics the counter-example is rejected
as non-well-founded.
That no Turing machine is a halt decider is a proven theorem and a
truth about Turing machines. If your "Proof Thoeretic Semnatics"
does not regard it as true then your "Proof Theoretic Semantics"
is incomplete.
My longrCaterm goal is to make rCytrue on the basis of meaningrCO computable.
As meaning is not computable, how can "true on the balsis of meaning"
be commputable?
Under *proofrCatheoretic semantics*
"true on the basis of meaning expressed in language"
has always been entirely computable.
On 1/15/2026 3:34 AM, Mikko wrote:
On 14/01/2026 21:32, olcott wrote:
On 1/14/2026 3:01 AM, Mikko wrote:
On 13/01/2026 16:31, olcott wrote:
On 1/13/2026 3:13 AM, Mikko wrote:
On 12/01/2026 16:32, olcott wrote:
On 1/12/2026 4:47 AM, Mikko wrote:
On 11/01/2026 16:24, Tristan Wibberley wrote:
On 11/01/2026 10:13, Mikko wrote:For pracitcal programming it is useful to know what is known to be >>>>>>>> uncomputable in order to avoid wasting time in attemlpts to do the >>>>>>>> impossible.
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:
You can't determine whether the required result is computable >>>>>>>>>> beforeNo, that does not follow. If a required result cannot be >>>>>>>>>>>> derived by
appying a finite string transformation then the it it is >>>>>>>>>>>> uncomputable.
Right. Outside the scope of computation. Requiring anything >>>>>>>>>>> outside the scope of computation is an incorrect requirement. >>>>>>>>>>
you have the requirement.
Right, it is /in/ scope for computer science... for the /
ology/. Olcott
here uses "computation" to refer to the practice. You give the >>>>>>>>> requirement to the /ologist/ who correctly decides that it is >>>>>>>>> not for
computation because it is not computable.
You two so often violently agree; I find it warming to the heart. >>>>>>>>
It f-cking nuts that after more than 2000 years
people still don't understand that self-contradictory
expressions: "This sentence is not true" have no
truth value. A smart high school student should have
figured this out 2000 years ago.
Irrelevant. For practical programming that question needn't be
answered.
The halting problem counter-example input is anchored
in the Liar Paradox. Proof Theoretic Semantics rejects
those two and G||del's incompleteness and a bunch more
as merely non-well-founded inputs.
For every Turing machine the halting problem counter-example provably
exists.
Not when using Proof Theoretic Semantics grounded
in the specification language. In this case the
pathological input is simply rejected as ungrounded.
Then your "Proof Theoretic Semantics" is not useful for discussion of
Turing machines. For every Turing machine a counter example exists.
And so exists a Turing machine that writes the counter example when
given a Turing machine as input.
It is "not useful" in the same way that ZFC was
"not useful" for addressing Russell's Paradox.
On 16/01/2026 01:38, olcott wrote:
On 1/15/2026 3:48 AM, Mikko wrote:
On 14/01/2026 19:28, olcott wrote:
On 1/14/2026 1:40 AM, Mikko wrote:
On 13/01/2026 16:27, olcott wrote:
On 1/13/2026 3:11 AM, Mikko wrote:
On 12/01/2026 16:29, olcott wrote:
On 1/12/2026 4:44 AM, Mikko wrote:
On 11/01/2026 16:18, olcott wrote:
On 1/11/2026 4:13 AM, Mikko wrote:
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:You can't determine whether the required result is computable >>>>>>>>>>> before
On 09/01/2026 17:52, olcott wrote:
On 1/9/2026 3:59 AM, Mikko wrote:
On 08/01/2026 16:22, olcott wrote:
On 1/8/2026 4:22 AM, Mikko wrote:The misconception is yours. No expression in the language >>>>>>>>>>>>>>> of the first
On 07/01/2026 13:54, olcott wrote:
On 1/7/2026 5:49 AM, Mikko wrote:
On 07/01/2026 06:44, olcott wrote:
All deciders essentially: Transform finite string >>>>>>>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>>>>>>> {Accept, Reject} values.
The counter-example input to requires more than >>>>>>>>>>>>>>>>>>>> can be derived from finite string transformation >>>>>>>>>>>>>>>>>>>> rules applied to this specific input thus the >>>>>>>>>>>>>>>>>>>> Halting Problem requires too much.
In a sense the halting problem asks too much: the >>>>>>>>>>>>>>>>>>> problem is proven to
be unsolvable. In another sense it asks too little: >>>>>>>>>>>>>>>>>>> usually we want to
know whether a method halts on every input, not just >>>>>>>>>>>>>>>>>>> one.
Although the halting problem is unsolvable, there are >>>>>>>>>>>>>>>>>>> partial solutions
to the halting problem. In particular, every counter- >>>>>>>>>>>>>>>>>>> example to the
full solution is correctly solved by some partial >>>>>>>>>>>>>>>>>>> deciders.
*if undecidability is correct then truth itself is >>>>>>>>>>>>>>>>>> broken*
Depends on whether the word "truth" is interpeted in >>>>>>>>>>>>>>>>> the standard
sense or in Olcott's sense.
Undecidability is misconception. Self-contradictory >>>>>>>>>>>>>>>> expressions are correctly rejected as semantically >>>>>>>>>>>>>>>> incoherent thus form no undecidability or incompleteness. >>>>>>>>>>>>>>>
order group theory is self-contradictory. But the first >>>>>>>>>>>>>>> order goupr
theory is incomplete: it is impossible to prove that AB = >>>>>>>>>>>>>>> BA is true
for every A and every B but it is also impossible to >>>>>>>>>>>>>>> prove that AB = BA
is false for some A and some B.
All deciders essentially: Transform finite string
inputs by finite string transformation rules into
{Accept, Reject} values.
When a required result cannot be derived by applying >>>>>>>>>>>>>> finite string transformation rules to actual finite >>>>>>>>>>>>>> string inputs, then the required result exceeds the >>>>>>>>>>>>>> scope of computation and must be rejected as an
incorrect requirement.
No, that does not follow. If a required result cannot be >>>>>>>>>>>>> derived by
appying a finite string transformation then the it it is >>>>>>>>>>>>> uncomputable.
Right. Outside the scope of computation. Requiring anything >>>>>>>>>>>> outside the scope of computation is an incorrect requirement. >>>>>>>>>>>
you have the requirement.
*Computation and Undecidability*
https://philpapers.org/go.pl?aid=OLCCAU
We know that there does not exist any finite
string transformations that H can apply to its
input P to derive the halt status of any P
that does the opposite of whatever H returns.
Which only nmakes sense when the requirement that H must determine >>>>>>>>> whether the computation presented by its input halts has already >>>>>>>>> been presented.
*ChatGPT explains how and why I am correct*
-a-a *Reinterpretation of undecidability*
-a-a The example of P and H demonstrates that what is
-a-a often called rCLundecidablerCY is better understood as >>>>>>>>>> -a-a ill-posed with respect to computable semantics.
-a-a When the specification is constrained to properties
-a-a detectable via finite simulation and finite pattern
-a-a recognition, computation proceeds normally and
-a-a correctly. Undecidability only appears when the
-a-a specification overreaches that boundary.
It tries to explain but it does not prove.
Its the same thing that I have been saying for years.
It is not that a universal halt decider cannot exist.
It is proven that an universal halt decider does not exist.
rCLThe system adopts Proof-Theoretic Semantics: meaning is
determined by inferential role, and truth is internal to the
theory. A theory T is defined by a finite set of stipulated atomic >>>>>> statements together with all expressions derivable from them under >>>>>> the inference rules. The statements belonging to T constitute its >>>>>> theorems, and these are exactly the statements that are true-in-T.rCY >>>>>>
Under a system like the above rough draft all inputs
having pathological self reference such as the halting
problem counter-example input are simply rejected as
non-well-founded. Tarski Undefinability, G||del's
incompleteness and the halting problem cease to exist.
A Turing
machine cannot determine the halting of all Turing machines and is >>>>>>> therefore not an universla halt decider.
This is not true in Proof Theoretic Semantics. I
still have to refine my words. I may not have said
that exactly correctly. The result is that in Proof
Theoretic Semantics the counter-example is rejected
as non-well-founded.
That no Turing machine is a halt decider is a proven theorem and a
truth about Turing machines. If your "Proof Thoeretic Semnatics"
does not regard it as true then your "Proof Theoretic Semantics"
is incomplete.
My longrCaterm goal is to make rCytrue on the basis of meaningrCO computable.
As meaning is not computable, how can "true on the balsis of meaning"
be commputable?
Under *proofrCatheoretic semantics*
"true on the basis of meaning expressed in language"
has always been entirely computable.
Have you already put the algorithm to some web page?
On 16/01/2026 01:38, olcott wrote:
On 1/15/2026 3:48 AM, Mikko wrote:
On 14/01/2026 19:28, olcott wrote:
On 1/14/2026 1:40 AM, Mikko wrote:
On 13/01/2026 16:27, olcott wrote:
On 1/13/2026 3:11 AM, Mikko wrote:
On 12/01/2026 16:29, olcott wrote:
On 1/12/2026 4:44 AM, Mikko wrote:
On 11/01/2026 16:18, olcott wrote:
On 1/11/2026 4:13 AM, Mikko wrote:
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:You can't determine whether the required result is computable >>>>>>>>>>> before
On 09/01/2026 17:52, olcott wrote:
On 1/9/2026 3:59 AM, Mikko wrote:
On 08/01/2026 16:22, olcott wrote:
On 1/8/2026 4:22 AM, Mikko wrote:The misconception is yours. No expression in the language >>>>>>>>>>>>>>> of the first
On 07/01/2026 13:54, olcott wrote:
On 1/7/2026 5:49 AM, Mikko wrote:
On 07/01/2026 06:44, olcott wrote:
All deciders essentially: Transform finite string >>>>>>>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>>>>>>> {Accept, Reject} values.
The counter-example input to requires more than >>>>>>>>>>>>>>>>>>>> can be derived from finite string transformation >>>>>>>>>>>>>>>>>>>> rules applied to this specific input thus the >>>>>>>>>>>>>>>>>>>> Halting Problem requires too much.
In a sense the halting problem asks too much: the >>>>>>>>>>>>>>>>>>> problem is proven to
be unsolvable. In another sense it asks too little: >>>>>>>>>>>>>>>>>>> usually we want to
know whether a method halts on every input, not just >>>>>>>>>>>>>>>>>>> one.
Although the halting problem is unsolvable, there are >>>>>>>>>>>>>>>>>>> partial solutions
to the halting problem. In particular, every counter- >>>>>>>>>>>>>>>>>>> example to the
full solution is correctly solved by some partial >>>>>>>>>>>>>>>>>>> deciders.
*if undecidability is correct then truth itself is >>>>>>>>>>>>>>>>>> broken*
Depends on whether the word "truth" is interpeted in >>>>>>>>>>>>>>>>> the standard
sense or in Olcott's sense.
Undecidability is misconception. Self-contradictory >>>>>>>>>>>>>>>> expressions are correctly rejected as semantically >>>>>>>>>>>>>>>> incoherent thus form no undecidability or incompleteness. >>>>>>>>>>>>>>>
order group theory is self-contradictory. But the first >>>>>>>>>>>>>>> order goupr
theory is incomplete: it is impossible to prove that AB = >>>>>>>>>>>>>>> BA is true
for every A and every B but it is also impossible to >>>>>>>>>>>>>>> prove that AB = BA
is false for some A and some B.
All deciders essentially: Transform finite string
inputs by finite string transformation rules into
{Accept, Reject} values.
When a required result cannot be derived by applying >>>>>>>>>>>>>> finite string transformation rules to actual finite >>>>>>>>>>>>>> string inputs, then the required result exceeds the >>>>>>>>>>>>>> scope of computation and must be rejected as an
incorrect requirement.
No, that does not follow. If a required result cannot be >>>>>>>>>>>>> derived by
appying a finite string transformation then the it it is >>>>>>>>>>>>> uncomputable.
Right. Outside the scope of computation. Requiring anything >>>>>>>>>>>> outside the scope of computation is an incorrect requirement. >>>>>>>>>>>
you have the requirement.
*Computation and Undecidability*
https://philpapers.org/go.pl?aid=OLCCAU
We know that there does not exist any finite
string transformations that H can apply to its
input P to derive the halt status of any P
that does the opposite of whatever H returns.
Which only nmakes sense when the requirement that H must determine >>>>>>>>> whether the computation presented by its input halts has already >>>>>>>>> been presented.
*ChatGPT explains how and why I am correct*
-a-a *Reinterpretation of undecidability*
-a-a The example of P and H demonstrates that what is
-a-a often called rCLundecidablerCY is better understood as >>>>>>>>>> -a-a ill-posed with respect to computable semantics.
-a-a When the specification is constrained to properties
-a-a detectable via finite simulation and finite pattern
-a-a recognition, computation proceeds normally and
-a-a correctly. Undecidability only appears when the
-a-a specification overreaches that boundary.
It tries to explain but it does not prove.
Its the same thing that I have been saying for years.
It is not that a universal halt decider cannot exist.
It is proven that an universal halt decider does not exist.
rCLThe system adopts Proof-Theoretic Semantics: meaning is
determined by inferential role, and truth is internal to the
theory. A theory T is defined by a finite set of stipulated atomic >>>>>> statements together with all expressions derivable from them under >>>>>> the inference rules. The statements belonging to T constitute its >>>>>> theorems, and these are exactly the statements that are true-in-T.rCY >>>>>>
Under a system like the above rough draft all inputs
having pathological self reference such as the halting
problem counter-example input are simply rejected as
non-well-founded. Tarski Undefinability, G||del's
incompleteness and the halting problem cease to exist.
A Turing
machine cannot determine the halting of all Turing machines and is >>>>>>> therefore not an universla halt decider.
This is not true in Proof Theoretic Semantics. I
still have to refine my words. I may not have said
that exactly correctly. The result is that in Proof
Theoretic Semantics the counter-example is rejected
as non-well-founded.
That no Turing machine is a halt decider is a proven theorem and a
truth about Turing machines. If your "Proof Thoeretic Semnatics"
does not regard it as true then your "Proof Theoretic Semantics"
is incomplete.
My longrCaterm goal is to make rCytrue on the basis of meaningrCO computable.
As meaning is not computable, how can "true on the balsis of meaning"
be commputable?
Under *proofrCatheoretic semantics*
"true on the basis of meaning expressed in language"
has always been entirely computable.
Have you already put the algorithm to some web page?
On 1/16/2026 3:17 AM, Mikko wrote:
On 16/01/2026 01:38, olcott wrote:
On 1/15/2026 3:48 AM, Mikko wrote:
On 14/01/2026 19:28, olcott wrote:
On 1/14/2026 1:40 AM, Mikko wrote:
On 13/01/2026 16:27, olcott wrote:
On 1/13/2026 3:11 AM, Mikko wrote:
On 12/01/2026 16:29, olcott wrote:
On 1/12/2026 4:44 AM, Mikko wrote:
On 11/01/2026 16:18, olcott wrote:
On 1/11/2026 4:13 AM, Mikko wrote:
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:You can't determine whether the required result is
On 09/01/2026 17:52, olcott wrote:
On 1/9/2026 3:59 AM, Mikko wrote:
On 08/01/2026 16:22, olcott wrote:
On 1/8/2026 4:22 AM, Mikko wrote:The misconception is yours. No expression in the >>>>>>>>>>>>>>>> language of the first
On 07/01/2026 13:54, olcott wrote:
On 1/7/2026 5:49 AM, Mikko wrote:
On 07/01/2026 06:44, olcott wrote:
All deciders essentially: Transform finite string >>>>>>>>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>>>>>>>> {Accept, Reject} values.
The counter-example input to requires more than >>>>>>>>>>>>>>>>>>>>> can be derived from finite string transformation >>>>>>>>>>>>>>>>>>>>> rules applied to this specific input thus the >>>>>>>>>>>>>>>>>>>>> Halting Problem requires too much.
In a sense the halting problem asks too much: the >>>>>>>>>>>>>>>>>>>> problem is proven to
be unsolvable. In another sense it asks too little: >>>>>>>>>>>>>>>>>>>> usually we want to
know whether a method halts on every input, not just >>>>>>>>>>>>>>>>>>>> one.
Although the halting problem is unsolvable, there >>>>>>>>>>>>>>>>>>>> are partial solutions
to the halting problem. In particular, every >>>>>>>>>>>>>>>>>>>> counter- example to the
full solution is correctly solved by some partial >>>>>>>>>>>>>>>>>>>> deciders.
*if undecidability is correct then truth itself is >>>>>>>>>>>>>>>>>>> broken*
Depends on whether the word "truth" is interpeted in >>>>>>>>>>>>>>>>>> the standard
sense or in Olcott's sense.
Undecidability is misconception. Self-contradictory >>>>>>>>>>>>>>>>> expressions are correctly rejected as semantically >>>>>>>>>>>>>>>>> incoherent thus form no undecidability or incompleteness. >>>>>>>>>>>>>>>>
order group theory is self-contradictory. But the first >>>>>>>>>>>>>>>> order goupr
theory is incomplete: it is impossible to prove that AB >>>>>>>>>>>>>>>> = BA is true
for every A and every B but it is also impossible to >>>>>>>>>>>>>>>> prove that AB = BA
is false for some A and some B.
All deciders essentially: Transform finite string >>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>> {Accept, Reject} values.
When a required result cannot be derived by applying >>>>>>>>>>>>>>> finite string transformation rules to actual finite >>>>>>>>>>>>>>> string inputs, then the required result exceeds the >>>>>>>>>>>>>>> scope of computation and must be rejected as an
incorrect requirement.
No, that does not follow. If a required result cannot be >>>>>>>>>>>>>> derived by
appying a finite string transformation then the it it is >>>>>>>>>>>>>> uncomputable.
Right. Outside the scope of computation. Requiring anything >>>>>>>>>>>>> outside the scope of computation is an incorrect requirement. >>>>>>>>>>>>
computable before
you have the requirement.
*Computation and Undecidability*
https://philpapers.org/go.pl?aid=OLCCAU
We know that there does not exist any finite
string transformations that H can apply to its
input P to derive the halt status of any P
that does the opposite of whatever H returns.
Which only nmakes sense when the requirement that H must
determine
whether the computation presented by its input halts has already >>>>>>>>>> been presented.
*ChatGPT explains how and why I am correct*
-a-a *Reinterpretation of undecidability*
-a-a The example of P and H demonstrates that what is
-a-a often called rCLundecidablerCY is better understood as >>>>>>>>>>> -a-a ill-posed with respect to computable semantics.
-a-a When the specification is constrained to properties >>>>>>>>>>> -a-a detectable via finite simulation and finite pattern >>>>>>>>>>> -a-a recognition, computation proceeds normally and
-a-a correctly. Undecidability only appears when the
-a-a specification overreaches that boundary.
It tries to explain but it does not prove.
Its the same thing that I have been saying for years.
It is not that a universal halt decider cannot exist.
It is proven that an universal halt decider does not exist.
rCLThe system adopts Proof-Theoretic Semantics: meaning is
determined by inferential role, and truth is internal to the
theory. A theory T is defined by a finite set of stipulated
atomic statements together with all expressions derivable from
them under the inference rules. The statements belonging to T
constitute its theorems, and these are exactly the statements
that are true-in-T.rCY
Under a system like the above rough draft all inputs
having pathological self reference such as the halting
problem counter-example input are simply rejected as
non-well-founded. Tarski Undefinability, G||del's
incompleteness and the halting problem cease to exist.
A Turing
machine cannot determine the halting of all Turing machines and is >>>>>>>> therefore not an universla halt decider.
This is not true in Proof Theoretic Semantics. I
still have to refine my words. I may not have said
that exactly correctly. The result is that in Proof
Theoretic Semantics the counter-example is rejected
as non-well-founded.
That no Turing machine is a halt decider is a proven theorem and a >>>>>> truth about Turing machines. If your "Proof Thoeretic Semnatics"
does not regard it as true then your "Proof Theoretic Semantics"
is incomplete.
My longrCaterm goal is to make rCytrue on the basis of meaningrCO
computable.
As meaning is not computable, how can "true on the balsis of meaning"
be commputable?
Under *proofrCatheoretic semantics*
"true on the basis of meaning expressed in language"
has always been entirely computable.
Have you already put the algorithm to some web page?
I am still working on refining the presentation.
On 1/16/2026 3:17 AM, Mikko wrote:
On 16/01/2026 01:38, olcott wrote:
On 1/15/2026 3:48 AM, Mikko wrote:
On 14/01/2026 19:28, olcott wrote:
On 1/14/2026 1:40 AM, Mikko wrote:
On 13/01/2026 16:27, olcott wrote:
On 1/13/2026 3:11 AM, Mikko wrote:
On 12/01/2026 16:29, olcott wrote:
On 1/12/2026 4:44 AM, Mikko wrote:
On 11/01/2026 16:18, olcott wrote:
On 1/11/2026 4:13 AM, Mikko wrote:
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:You can't determine whether the required result is
On 09/01/2026 17:52, olcott wrote:
On 1/9/2026 3:59 AM, Mikko wrote:
On 08/01/2026 16:22, olcott wrote:
On 1/8/2026 4:22 AM, Mikko wrote:The misconception is yours. No expression in the >>>>>>>>>>>>>>>> language of the first
On 07/01/2026 13:54, olcott wrote:
On 1/7/2026 5:49 AM, Mikko wrote:
On 07/01/2026 06:44, olcott wrote:
All deciders essentially: Transform finite string >>>>>>>>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>>>>>>>> {Accept, Reject} values.
The counter-example input to requires more than >>>>>>>>>>>>>>>>>>>>> can be derived from finite string transformation >>>>>>>>>>>>>>>>>>>>> rules applied to this specific input thus the >>>>>>>>>>>>>>>>>>>>> Halting Problem requires too much.
In a sense the halting problem asks too much: the >>>>>>>>>>>>>>>>>>>> problem is proven to
be unsolvable. In another sense it asks too little: >>>>>>>>>>>>>>>>>>>> usually we want to
know whether a method halts on every input, not just >>>>>>>>>>>>>>>>>>>> one.
Although the halting problem is unsolvable, there >>>>>>>>>>>>>>>>>>>> are partial solutions
to the halting problem. In particular, every >>>>>>>>>>>>>>>>>>>> counter- example to the
full solution is correctly solved by some partial >>>>>>>>>>>>>>>>>>>> deciders.
*if undecidability is correct then truth itself is >>>>>>>>>>>>>>>>>>> broken*
Depends on whether the word "truth" is interpeted in >>>>>>>>>>>>>>>>>> the standard
sense or in Olcott's sense.
Undecidability is misconception. Self-contradictory >>>>>>>>>>>>>>>>> expressions are correctly rejected as semantically >>>>>>>>>>>>>>>>> incoherent thus form no undecidability or incompleteness. >>>>>>>>>>>>>>>>
order group theory is self-contradictory. But the first >>>>>>>>>>>>>>>> order goupr
theory is incomplete: it is impossible to prove that AB >>>>>>>>>>>>>>>> = BA is true
for every A and every B but it is also impossible to >>>>>>>>>>>>>>>> prove that AB = BA
is false for some A and some B.
All deciders essentially: Transform finite string >>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>> {Accept, Reject} values.
When a required result cannot be derived by applying >>>>>>>>>>>>>>> finite string transformation rules to actual finite >>>>>>>>>>>>>>> string inputs, then the required result exceeds the >>>>>>>>>>>>>>> scope of computation and must be rejected as an
incorrect requirement.
No, that does not follow. If a required result cannot be >>>>>>>>>>>>>> derived by
appying a finite string transformation then the it it is >>>>>>>>>>>>>> uncomputable.
Right. Outside the scope of computation. Requiring anything >>>>>>>>>>>>> outside the scope of computation is an incorrect requirement. >>>>>>>>>>>>
computable before
you have the requirement.
*Computation and Undecidability*
https://philpapers.org/go.pl?aid=OLCCAU
We know that there does not exist any finite
string transformations that H can apply to its
input P to derive the halt status of any P
that does the opposite of whatever H returns.
Which only nmakes sense when the requirement that H must
determine
whether the computation presented by its input halts has already >>>>>>>>>> been presented.
*ChatGPT explains how and why I am correct*
-a-a *Reinterpretation of undecidability*
-a-a The example of P and H demonstrates that what is
-a-a often called rCLundecidablerCY is better understood as >>>>>>>>>>> -a-a ill-posed with respect to computable semantics.
-a-a When the specification is constrained to properties >>>>>>>>>>> -a-a detectable via finite simulation and finite pattern >>>>>>>>>>> -a-a recognition, computation proceeds normally and
-a-a correctly. Undecidability only appears when the
-a-a specification overreaches that boundary.
It tries to explain but it does not prove.
Its the same thing that I have been saying for years.
It is not that a universal halt decider cannot exist.
It is proven that an universal halt decider does not exist.
rCLThe system adopts Proof-Theoretic Semantics: meaning is
determined by inferential role, and truth is internal to the
theory. A theory T is defined by a finite set of stipulated
atomic statements together with all expressions derivable from
them under the inference rules. The statements belonging to T
constitute its theorems, and these are exactly the statements
that are true-in-T.rCY
Under a system like the above rough draft all inputs
having pathological self reference such as the halting
problem counter-example input are simply rejected as
non-well-founded. Tarski Undefinability, G||del's
incompleteness and the halting problem cease to exist.
A Turing
machine cannot determine the halting of all Turing machines and is >>>>>>>> therefore not an universla halt decider.
This is not true in Proof Theoretic Semantics. I
still have to refine my words. I may not have said
that exactly correctly. The result is that in Proof
Theoretic Semantics the counter-example is rejected
as non-well-founded.
That no Turing machine is a halt decider is a proven theorem and a >>>>>> truth about Turing machines. If your "Proof Thoeretic Semnatics"
does not regard it as true then your "Proof Theoretic Semantics"
is incomplete.
My longrCaterm goal is to make rCytrue on the basis of meaningrCO
computable.
As meaning is not computable, how can "true on the balsis of meaning"
be commputable?
Under *proofrCatheoretic semantics*
"true on the basis of meaning expressed in language"
has always been entirely computable.
Have you already put the algorithm to some web page?
Proof Theoretic Semantics Blocks Pathological Self-Reference https://philpapers.org/rec/OLCPTS
On 1/16/2026 3:17 AM, Mikko wrote:
On 16/01/2026 01:38, olcott wrote:
On 1/15/2026 3:48 AM, Mikko wrote:
On 14/01/2026 19:28, olcott wrote:
On 1/14/2026 1:40 AM, Mikko wrote:
On 13/01/2026 16:27, olcott wrote:
On 1/13/2026 3:11 AM, Mikko wrote:
On 12/01/2026 16:29, olcott wrote:
On 1/12/2026 4:44 AM, Mikko wrote:
On 11/01/2026 16:18, olcott wrote:
On 1/11/2026 4:13 AM, Mikko wrote:
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:You can't determine whether the required result is
On 09/01/2026 17:52, olcott wrote:
On 1/9/2026 3:59 AM, Mikko wrote:
On 08/01/2026 16:22, olcott wrote:
On 1/8/2026 4:22 AM, Mikko wrote:The misconception is yours. No expression in the >>>>>>>>>>>>>>>> language of the first
On 07/01/2026 13:54, olcott wrote:
On 1/7/2026 5:49 AM, Mikko wrote:
On 07/01/2026 06:44, olcott wrote:
All deciders essentially: Transform finite string >>>>>>>>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>>>>>>>> {Accept, Reject} values.
The counter-example input to requires more than >>>>>>>>>>>>>>>>>>>>> can be derived from finite string transformation >>>>>>>>>>>>>>>>>>>>> rules applied to this specific input thus the >>>>>>>>>>>>>>>>>>>>> Halting Problem requires too much.
In a sense the halting problem asks too much: the >>>>>>>>>>>>>>>>>>>> problem is proven to
be unsolvable. In another sense it asks too little: >>>>>>>>>>>>>>>>>>>> usually we want to
know whether a method halts on every input, not just >>>>>>>>>>>>>>>>>>>> one.
Although the halting problem is unsolvable, there >>>>>>>>>>>>>>>>>>>> are partial solutions
to the halting problem. In particular, every >>>>>>>>>>>>>>>>>>>> counter- example to the
full solution is correctly solved by some partial >>>>>>>>>>>>>>>>>>>> deciders.
*if undecidability is correct then truth itself is >>>>>>>>>>>>>>>>>>> broken*
Depends on whether the word "truth" is interpeted in >>>>>>>>>>>>>>>>>> the standard
sense or in Olcott's sense.
Undecidability is misconception. Self-contradictory >>>>>>>>>>>>>>>>> expressions are correctly rejected as semantically >>>>>>>>>>>>>>>>> incoherent thus form no undecidability or incompleteness. >>>>>>>>>>>>>>>>
order group theory is self-contradictory. But the first >>>>>>>>>>>>>>>> order goupr
theory is incomplete: it is impossible to prove that AB >>>>>>>>>>>>>>>> = BA is true
for every A and every B but it is also impossible to >>>>>>>>>>>>>>>> prove that AB = BA
is false for some A and some B.
All deciders essentially: Transform finite string >>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>> {Accept, Reject} values.
When a required result cannot be derived by applying >>>>>>>>>>>>>>> finite string transformation rules to actual finite >>>>>>>>>>>>>>> string inputs, then the required result exceeds the >>>>>>>>>>>>>>> scope of computation and must be rejected as an
incorrect requirement.
No, that does not follow. If a required result cannot be >>>>>>>>>>>>>> derived by
appying a finite string transformation then the it it is >>>>>>>>>>>>>> uncomputable.
Right. Outside the scope of computation. Requiring anything >>>>>>>>>>>>> outside the scope of computation is an incorrect requirement. >>>>>>>>>>>>
computable before
you have the requirement.
*Computation and Undecidability*
https://philpapers.org/go.pl?aid=OLCCAU
We know that there does not exist any finite
string transformations that H can apply to its
input P to derive the halt status of any P
that does the opposite of whatever H returns.
Which only nmakes sense when the requirement that H must
determine
whether the computation presented by its input halts has already >>>>>>>>>> been presented.
*ChatGPT explains how and why I am correct*
-a-a *Reinterpretation of undecidability*
-a-a The example of P and H demonstrates that what is
-a-a often called rCLundecidablerCY is better understood as >>>>>>>>>>> -a-a ill-posed with respect to computable semantics.
-a-a When the specification is constrained to properties >>>>>>>>>>> -a-a detectable via finite simulation and finite pattern >>>>>>>>>>> -a-a recognition, computation proceeds normally and
-a-a correctly. Undecidability only appears when the
-a-a specification overreaches that boundary.
It tries to explain but it does not prove.
Its the same thing that I have been saying for years.
It is not that a universal halt decider cannot exist.
It is proven that an universal halt decider does not exist.
rCLThe system adopts Proof-Theoretic Semantics: meaning is
determined by inferential role, and truth is internal to the
theory. A theory T is defined by a finite set of stipulated
atomic statements together with all expressions derivable from
them under the inference rules. The statements belonging to T
constitute its theorems, and these are exactly the statements
that are true-in-T.rCY
Under a system like the above rough draft all inputs
having pathological self reference such as the halting
problem counter-example input are simply rejected as
non-well-founded. Tarski Undefinability, G||del's
incompleteness and the halting problem cease to exist.
A Turing
machine cannot determine the halting of all Turing machines and is >>>>>>>> therefore not an universla halt decider.
This is not true in Proof Theoretic Semantics. I
still have to refine my words. I may not have said
that exactly correctly. The result is that in Proof
Theoretic Semantics the counter-example is rejected
as non-well-founded.
That no Turing machine is a halt decider is a proven theorem and a >>>>>> truth about Turing machines. If your "Proof Thoeretic Semnatics"
does not regard it as true then your "Proof Theoretic Semantics"
is incomplete.
My longrCaterm goal is to make rCytrue on the basis of meaningrCO
computable.
As meaning is not computable, how can "true on the balsis of meaning"
be commputable?
Under *proofrCatheoretic semantics*
"true on the basis of meaning expressed in language"
has always been entirely computable.
Have you already put the algorithm to some web page?
Proof Theoretic Semantics Blocks Pathological Self-Reference https://philpapers.org/rec/OLCPTS
On 1/16/2026 3:17 AM, Mikko wrote:
On 16/01/2026 01:38, olcott wrote:
On 1/15/2026 3:48 AM, Mikko wrote:
On 14/01/2026 19:28, olcott wrote:
On 1/14/2026 1:40 AM, Mikko wrote:
On 13/01/2026 16:27, olcott wrote:
On 1/13/2026 3:11 AM, Mikko wrote:
On 12/01/2026 16:29, olcott wrote:
On 1/12/2026 4:44 AM, Mikko wrote:
On 11/01/2026 16:18, olcott wrote:
On 1/11/2026 4:13 AM, Mikko wrote:
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:You can't determine whether the required result is
On 09/01/2026 17:52, olcott wrote:
On 1/9/2026 3:59 AM, Mikko wrote:
On 08/01/2026 16:22, olcott wrote:
On 1/8/2026 4:22 AM, Mikko wrote:The misconception is yours. No expression in the >>>>>>>>>>>>>>>> language of the first
On 07/01/2026 13:54, olcott wrote:
On 1/7/2026 5:49 AM, Mikko wrote:
On 07/01/2026 06:44, olcott wrote:
All deciders essentially: Transform finite string >>>>>>>>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>>>>>>>> {Accept, Reject} values.
The counter-example input to requires more than >>>>>>>>>>>>>>>>>>>>> can be derived from finite string transformation >>>>>>>>>>>>>>>>>>>>> rules applied to this specific input thus the >>>>>>>>>>>>>>>>>>>>> Halting Problem requires too much.
In a sense the halting problem asks too much: the >>>>>>>>>>>>>>>>>>>> problem is proven to
be unsolvable. In another sense it asks too little: >>>>>>>>>>>>>>>>>>>> usually we want to
know whether a method halts on every input, not just >>>>>>>>>>>>>>>>>>>> one.
Although the halting problem is unsolvable, there >>>>>>>>>>>>>>>>>>>> are partial solutions
to the halting problem. In particular, every >>>>>>>>>>>>>>>>>>>> counter- example to the
full solution is correctly solved by some partial >>>>>>>>>>>>>>>>>>>> deciders.
*if undecidability is correct then truth itself is >>>>>>>>>>>>>>>>>>> broken*
Depends on whether the word "truth" is interpeted in >>>>>>>>>>>>>>>>>> the standard
sense or in Olcott's sense.
Undecidability is misconception. Self-contradictory >>>>>>>>>>>>>>>>> expressions are correctly rejected as semantically >>>>>>>>>>>>>>>>> incoherent thus form no undecidability or incompleteness. >>>>>>>>>>>>>>>>
order group theory is self-contradictory. But the first >>>>>>>>>>>>>>>> order goupr
theory is incomplete: it is impossible to prove that AB >>>>>>>>>>>>>>>> = BA is true
for every A and every B but it is also impossible to >>>>>>>>>>>>>>>> prove that AB = BA
is false for some A and some B.
All deciders essentially: Transform finite string >>>>>>>>>>>>>>> inputs by finite string transformation rules into >>>>>>>>>>>>>>> {Accept, Reject} values.
When a required result cannot be derived by applying >>>>>>>>>>>>>>> finite string transformation rules to actual finite >>>>>>>>>>>>>>> string inputs, then the required result exceeds the >>>>>>>>>>>>>>> scope of computation and must be rejected as an
incorrect requirement.
No, that does not follow. If a required result cannot be >>>>>>>>>>>>>> derived by
appying a finite string transformation then the it it is >>>>>>>>>>>>>> uncomputable.
Right. Outside the scope of computation. Requiring anything >>>>>>>>>>>>> outside the scope of computation is an incorrect requirement. >>>>>>>>>>>>
computable before
you have the requirement.
*Computation and Undecidability*
https://philpapers.org/go.pl?aid=OLCCAU
We know that there does not exist any finite
string transformations that H can apply to its
input P to derive the halt status of any P
that does the opposite of whatever H returns.
Which only nmakes sense when the requirement that H must
determine
whether the computation presented by its input halts has already >>>>>>>>>> been presented.
*ChatGPT explains how and why I am correct*
-a-a *Reinterpretation of undecidability*
-a-a The example of P and H demonstrates that what is
-a-a often called rCLundecidablerCY is better understood as >>>>>>>>>>> -a-a ill-posed with respect to computable semantics.
-a-a When the specification is constrained to properties >>>>>>>>>>> -a-a detectable via finite simulation and finite pattern >>>>>>>>>>> -a-a recognition, computation proceeds normally and
-a-a correctly. Undecidability only appears when the
-a-a specification overreaches that boundary.
It tries to explain but it does not prove.
Its the same thing that I have been saying for years.
It is not that a universal halt decider cannot exist.
It is proven that an universal halt decider does not exist.
rCLThe system adopts Proof-Theoretic Semantics: meaning is
determined by inferential role, and truth is internal to the
theory. A theory T is defined by a finite set of stipulated
atomic statements together with all expressions derivable from
them under the inference rules. The statements belonging to T
constitute its theorems, and these are exactly the statements
that are true-in-T.rCY
Under a system like the above rough draft all inputs
having pathological self reference such as the halting
problem counter-example input are simply rejected as
non-well-founded. Tarski Undefinability, G||del's
incompleteness and the halting problem cease to exist.
A Turing
machine cannot determine the halting of all Turing machines and is >>>>>>>> therefore not an universla halt decider.
This is not true in Proof Theoretic Semantics. I
still have to refine my words. I may not have said
that exactly correctly. The result is that in Proof
Theoretic Semantics the counter-example is rejected
as non-well-founded.
That no Turing machine is a halt decider is a proven theorem and a >>>>>> truth about Turing machines. If your "Proof Thoeretic Semnatics"
does not regard it as true then your "Proof Theoretic Semantics"
is incomplete.
My longrCaterm goal is to make rCytrue on the basis of meaningrCO
computable.
As meaning is not computable, how can "true on the balsis of meaning"
be commputable?
Under *proofrCatheoretic semantics*
"true on the basis of meaning expressed in language"
has always been entirely computable.
Have you already put the algorithm to some web page?
Proof Theoretic Semantics Blocks Pathological Self-Reference https://philpapers.org/rec/OLCPTS
On 16/01/2026 17:38, olcott wrote:
On 1/16/2026 3:32 AM, Mikko wrote:
On 15/01/2026 22:30, olcott wrote:
On 1/15/2026 3:34 AM, Mikko wrote:
On 14/01/2026 21:32, olcott wrote:
On 1/14/2026 3:01 AM, Mikko wrote:
On 13/01/2026 16:31, olcott wrote:
On 1/13/2026 3:13 AM, Mikko wrote:
On 12/01/2026 16:32, olcott wrote:
On 1/12/2026 4:47 AM, Mikko wrote:
On 11/01/2026 16:24, Tristan Wibberley wrote:
On 11/01/2026 10:13, Mikko wrote:
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:
You can't determine whether the required result isNo, that does not follow. If a required result cannot be >>>>>>>>>>>>>>> derived by
appying a finite string transformation then the it it is >>>>>>>>>>>>>>> uncomputable.
Right. Outside the scope of computation. Requiring anything >>>>>>>>>>>>>> outside the scope of computation is an incorrect requirement. >>>>>>>>>>>>>
computable before
you have the requirement.
Right, it is /in/ scope for computer science... for the / >>>>>>>>>>>> ology/. Olcott
here uses "computation" to refer to the practice. You give the >>>>>>>>>>>> requirement to the /ologist/ who correctly decides that it >>>>>>>>>>>> is not for
computation because it is not computable.
You two so often violently agree; I find it warming to the >>>>>>>>>>>> heart.
For pracitcal programming it is useful to know what is known >>>>>>>>>>> to be
uncomputable in order to avoid wasting time in attemlpts to >>>>>>>>>>> do the
impossible.
It f-cking nuts that after more than 2000 years
people still don't understand that self-contradictory
expressions: "This sentence is not true" have no
truth value. A smart high school student should have
figured this out 2000 years ago.
Irrelevant. For practical programming that question needn't be >>>>>>>>> answered.
The halting problem counter-example input is anchored
in the Liar Paradox. Proof Theoretic Semantics rejects
those two and G||del's incompleteness and a bunch more
as merely non-well-founded inputs.
For every Turing machine the halting problem counter-example
provably
exists.
Not when using Proof Theoretic Semantics grounded
in the specification language. In this case the
pathological input is simply rejected as ungrounded.
Then your "Proof Theoretic Semantics" is not useful for discussion of >>>>> Turing machines. For every Turing machine a counter example exists.
And so exists a Turing machine that writes the counter example when
given a Turing machine as input.
It is "not useful" in the same way that ZFC was
"not useful" for addressing Russell's Paradox.
ZF or ZFC is to some extent useful for addressing Russell's paradox.
It is an example of a set theory where Russell's paradox is avoided.
If your "Proof Theretic Semantics" cannot handle the existence of
a counter example for every Turing decider then it is not usefule
for those who work on practical problems of program correctness.
Proof theoretic semantics addresses G||del Incompleteness
for PA in a way similar to the way that ZFC addresses
Russell's Paradox in set theory.
Not really the same way. Your "Proof theoretic semantics" redefines
truth and replaces the logic. ZFC is another theory using ordinary
logic. The problem with the naive set theory is that it is not
sound for any semantics.
On 1/17/2026 3:53 AM, Mikko wrote:
On 16/01/2026 17:38, olcott wrote:
On 1/16/2026 3:32 AM, Mikko wrote:
On 15/01/2026 22:30, olcott wrote:
On 1/15/2026 3:34 AM, Mikko wrote:
On 14/01/2026 21:32, olcott wrote:
On 1/14/2026 3:01 AM, Mikko wrote:
On 13/01/2026 16:31, olcott wrote:
On 1/13/2026 3:13 AM, Mikko wrote:
On 12/01/2026 16:32, olcott wrote:
On 1/12/2026 4:47 AM, Mikko wrote:
On 11/01/2026 16:24, Tristan Wibberley wrote:
On 11/01/2026 10:13, Mikko wrote:
On 10/01/2026 17:47, olcott wrote:
On 1/10/2026 2:23 AM, Mikko wrote:
No, that does not follow. If a required result cannot be >>>>>>>>>>>>>>>> derived by
appying a finite string transformation then the it it is >>>>>>>>>>>>>>>> uncomputable.
Right. Outside the scope of computation. Requiring anything >>>>>>>>>>>>>>> outside the scope of computation is an incorrect >>>>>>>>>>>>>>> requirement.
You can't determine whether the required result is >>>>>>>>>>>>>> computable before
you have the requirement.
Right, it is /in/ scope for computer science... for the / >>>>>>>>>>>>> ology/. Olcott
here uses "computation" to refer to the practice. You give the >>>>>>>>>>>>> requirement to the /ologist/ who correctly decides that it >>>>>>>>>>>>> is not for
computation because it is not computable.
You two so often violently agree; I find it warming to the >>>>>>>>>>>>> heart.
For pracitcal programming it is useful to know what is known >>>>>>>>>>>> to be
uncomputable in order to avoid wasting time in attemlpts to >>>>>>>>>>>> do the
impossible.
It f-cking nuts that after more than 2000 years
people still don't understand that self-contradictory
expressions: "This sentence is not true" have no
truth value. A smart high school student should have
figured this out 2000 years ago.
Irrelevant. For practical programming that question needn't be >>>>>>>>>> answered.
The halting problem counter-example input is anchored
in the Liar Paradox. Proof Theoretic Semantics rejects
those two and G||del's incompleteness and a bunch more
as merely non-well-founded inputs.
For every Turing machine the halting problem counter-example
provably
exists.
Not when using Proof Theoretic Semantics grounded
in the specification language. In this case the
pathological input is simply rejected as ungrounded.
Then your "Proof Theoretic Semantics" is not useful for discussion of >>>>>> Turing machines. For every Turing machine a counter example exists. >>>>>> And so exists a Turing machine that writes the counter example when >>>>>> given a Turing machine as input.
It is "not useful" in the same way that ZFC was
"not useful" for addressing Russell's Paradox.
ZF or ZFC is to some extent useful for addressing Russell's paradox.
It is an example of a set theory where Russell's paradox is avoided.
If your "Proof Theretic Semantics" cannot handle the existence of
a counter example for every Turing decider then it is not usefule
for those who work on practical problems of program correctness.
Proof theoretic semantics addresses G||del Incompleteness
for PA in a way similar to the way that ZFC addresses
Russell's Paradox in set theory.
Not really the same way. Your "Proof theoretic semantics" redefines
truth and replaces the logic. ZFC is another theory using ordinary
logic. The problem with the naive set theory is that it is not
sound for any semantics.
ZFC redefines set theory such that Russell's Paradox cannot arise.
Proof theoretic semantics redefines formal systems such that
Incompleteness cannot arise. G||del did not do this himself because
Proof theoretic semantics did not exist at the time.
| Sysop: | Amessyroom |
|---|---|
| Location: | Fayetteville, NC |
| Users: | 74 |
| Nodes: | 6 (0 / 6) |
| Uptime: | 01:01:18 |
| Calls: | 1,102 |
| Calls today: | 2 |
| Files: | 1,339 |
| Messages: | 276,780 |