On 4/9/26 5:43 PM, Ross Finlayson wrote:
On 04/09/2026 12:55 PM, Chris M. Thomasson wrote:
On 4/9/2026 10:14 AM, Ross Finlayson wrote:
On 04/09/2026 05:46 AM, Alan Mackenzie wrote:
In sci.math Chris M. Thomasson <chris.m.thomasson.1@gmail.com> wrote: >>>>>> On 4/7/2026 12:46 PM, Alan Mackenzie wrote:
In comp.theory Chris M. Thomasson <chris.m.thomasson.1@gmail.com> >>>>>>> wrote:
[ .... ]
Why are seemingly trying to justify pedo's?
You're the sort of person who, 90 years ago in Europe, would be >>>>>>> asking
"why are you trying to justify Jews?".
Strange! pedo vs a person who is jewish?
I just don't believe you're dumb enough not to see the analogy. We're >>>>> talking about two groups of people who aren't popular in popular
culture
(of whatever time), and bullies like you think that justifies them in >>>>> harrassing members of those groups with degrading epithets.
You used the term "low-life pedo" in this thread, implying that the
target of your nastiness was less than human. I suggest you
reconsider
all the implications, and then apologise publicly to Peter Olcott in >>>>> this thread.
Besides everything else, individuals' sexual psychology is not on
topic
in the newsgroups this thread is posted to.
"Otherism" as a usual account is sometimes demonizing specters and then >>>> threatening sympathy with association, and furthermore threatening the >>>> rejection of otherism as association with the demonized, besides the
wider accounts of "otherism" and "we-think" and "in-group" types of
pecking and the like, then furthermore is the association with "thought >>>> police" and the like, here vis-a-vis "thought crimes" and "real
crimes".
So, besides "un-popular", it's a gross bludgeon.
Let us recall the stories we'd tell youth, or give youth to discover,
the fable.
https://en.wikipedia.org/wiki/Fable
https://en.wikipedia.org/wiki/Aesop%27s_Fables#Select_fables
Now, plenty of these fables have consequences,
and some invoke a specter like "the boogey-man"
as variously threatens irresponsibility or the unwary,
or, punishes misbehavior, and even, when that
invoking the specter, invokes the specter.
https://en.wikipedia.org/wiki/The_Boy_Who_Cried_Wolf
The psycho-sexual in the psycho-logical, is an aspect
of thinking and feeling beings, largely biological.
Anyways children should be more concerned with if anybody
in their class likes them, not whether the world is full
of monsters, after them. (Nor that they'll become one.)
There is not a monster under the bed,
there is not a monster in the closet,
there is not a monster in the basement,
there is not a monster in the yard.
"The only thing to fear is fear itself."
"So, first of all, let me assert my firm belief that the only thing we >>>> have to fear is fear itself — nameless, unreasoning, unjustified terror >>>> which paralyzes needed efforts to convert retreat into advance." -- FDR >>>>
There is not a monster in your mind.
Then, basically it's insulting to make "ad hominem" fallacy.
I read a good book a few years ago about identity and including
a chapter on otherism, and how easy it is to see through it,
I'm thinking it was an "Ian B." or so, if I don't recall,
something about "politics of identity" or "psychology of identity"
or along these lines, in the philosophy section though as about
psychology. If I recall it I'll note it here.
Anyways, we still need a word for "loves children".
Thanks for writing.
A parent loves their children, indeed. Or at least they should? Olcott,
might love them too much? Oh shit, there I go again.
Try minding your own business and the old "innocent until proven
guilty", and not be sham "operant-conditioning" that is still
back on pigeons and dogs.
If your actual interests are "protecting the children", and everybody
else, from dangers real or imagined, how about investigating "ad-tech"
for billions of counts and counting of "luring", "corruption of a
minor", "child endangerment", and not even getting into slander and
libel, "identity theft", "computer crimes", and so on. The "ad-tech"
is not "social media", it's got no "safe harbor", and having
algorithm'ed itself it's poisoned itself and pierced its own veil.
Then, about what used to be "special services", these days with
the "surveillance tech" making it more like "secret stasis",
then that's also for busting surveillance tech. That and
busting all the "seals" covering all kinds of "mistakes".
Yes, let's protect the children by busting ad-tech and surveillance
tech. For example, they're liable for anything they know.
Sometimes: ignorance _is_ a defense.
idk if u've used the rest of the internet in the last decade or so,
but pedos are basically the ultimately boogieman that somehow sit below literal serial killers and mass murders on the social media hierarchy,
usenet (which i only joined last year) is the only place i've ever seen
any amount of nuance applied to subject, probably because censorship
doesn't really exist here, and therefore the discussion cannot be shaped
by the fear of people in charge
imo this is likely a reflection of an incredibly amount of systemic
sexual trauma we've received by how modern society represses sexuality during childhood, which i think is an appendage of how religion used to repress it, that somehow snuck it's way into secular society...
my wife just gave birth to a boy 6 hours ago, and i'm unsure of how to protect him from that during his childhood 😕
On 4/9/2026 11:01 PM, dart200 wrote:
Why are seemingly trying to justify pedo's?
my wife just gave birth to a boy 6 hours ago, and i'm unsure of how to
protect him from that during his childhood 😕
Don't ever let him onto the internet. It's addictive. Case in point.
On 4/10/2026 4:24 PM, Dude wrote:
On 4/9/2026 11:01 PM, dart200 wrote:
Why are seemingly trying to justify pedo's?
;Don't ever let him onto the internet. It's addictive. Case in point.
my wife just gave birth to a boy 6 hours ago, and i'm unsure of how
to > protect him from that during his childhood 😕
;
Scary. He has to be able to use the internet, but its the wild west
filled with predators. Sigh.
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
On 02/04/2026 21:58, olcott wrote:
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Won't the intuitive meaning of the phrase require just a non-strict description of all the tails of all the derivations of a statement? Is
that it? A trivial notion of a search space that is defined inductively
from the goal statement if one has eliminated the potential for a graph
to occur using a unique resolution of cycles to either one choice or
none (which I expect you will pick "none") ?
On 02/04/2026 21:58, olcott wrote:
To be able to properly ground this in existing foundational
peer reviewed papers will take some time.
Won't the intuitive meaning of the phrase require just a non-strict description of all the tails of all the derivations of a statement? Is
that it? A trivial notion of a search space that is defined inductively
from the goal statement if one has eliminated the potential for a graph
to occur using a unique resolution of cycles to either one choice or
none (which I expect you will pick "none") ?
On 23/04/2026 16:32, olcott wrote:
On 4/23/2026 1:35 AM, Mikko wrote:
On 22/04/2026 10:45, olcott wrote:
On 4/22/2026 2:03 AM, Mikko wrote:
On 21/04/2026 16:22, olcott wrote:
On 4/21/2026 1:30 AM, Mikko wrote:
On 20/04/2026 16:31, olcott wrote:
On 4/20/2026 3:49 AM, Mikko wrote:
On 19/04/2026 20:21, olcott wrote:
On 4/19/2026 3:59 AM, Mikko wrote:
On 18/04/2026 15:58, olcott wrote:
Unknown truths are not elements of the body of
knowledge is a semantic tautology. Did you think
that things that are unknown are known?
No, but that measn that for some sentences X True(X) is >>>>>>>>>>> unknown and there
is no method to find out.
I don't know about philosophers but mathematicians and
logicians don't
find it interesting if all you can say that all knowledge is >>>>>>>>>>> knowable
and everything else is not.
Ross Finlayson, seemed to endlessly hedge on whether
or not the truth value of the Goldbach conjecture was
known. He seemed to think that there are alternative
analytical frameworks that make the question of whether
or not its truth value is known an ambiguous question.
I needed to refer to unknown truth values specifically
because all "undecidability" when construed correctly
falls into one of two categories.
(a) Semantic incoherence
(b) Unknown truth values.
A centence can be said to be undecidable when it is known that >>>>>>>>> neither
the sentence nor its negation is a theorem.
When we skip model theory and and define True and False
as the existence of a back chained sequence of inference
steps of expressions x or ~x reaching axioms
It is not useful to define new terms for comcepts that already have >>>>>>> good terms.
The result of undecidability proves that the current
foundations are incoherent in the same way that
Russell's paradox proved that naive set theory had
a glitch.
Hardly the same way as Russell's paradox proves that there is no
undecidability in the naive set theory.
If the sequence of inference steps is restricted to
valid inferences the term "True" as defined above then "sentence is >>>>>>> true" is just another way to say "sentence is a theorem".
then it is a yes or no question that has no correct yes
or no answer within the formal system.
Even if a question has no answer within a formal theory of natural >>>>>>> numbers it may have an answer in the natural numbers themselves. >>>>>>>
My system is based on simple type theory and formalized
natural language.
This makes it a yes or no question that has no
correct yes or no answer at all anywhere, thus
an incorrect polar question.
How does your system handle questions that are not known to have a >>>>>>> yes or no answer but k´nor known to lack such answer, either,
e.g. Goldbach's conjecture ?
out-of-scope of the body of knowledge.
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
So the question whether something is in the scope of your system
is not in the scope of your system? OK, but shoudn't such questions
be answerable anyway?
The truth value of the Goldbach conjecture might
be unknowable if it is true and the only way to
prove it is true is an infinite number of steps.
Peano arithmetic is unsolvable, i.e., there is no method to find
out whether a particular sentence (for exmaple Goldbach conjecture)
is provable or not. If you find a proof then you know it but it is
possible that you never find, no matter how much you search.
Goldbach is unknowable if it is true because
verifying that it is true requires an infinite
number of steps.
That is not known. Perhaps there is an unknown proof that proves it.
This just means that the truth> value of Goldbach is outside of thebody of
knowledge thus outside of the scope of my project.While the truth value is not in the body of knowledge someone may
some day find a way to infer it from what is known.
On 4/24/2026 1:08 AM, Mikko wrote:
On 23/04/2026 16:32, olcott wrote:
On 4/23/2026 1:35 AM, Mikko wrote:
On 22/04/2026 10:45, olcott wrote:
On 4/22/2026 2:03 AM, Mikko wrote:
On 21/04/2026 16:22, olcott wrote:
On 4/21/2026 1:30 AM, Mikko wrote:
On 20/04/2026 16:31, olcott wrote:
On 4/20/2026 3:49 AM, Mikko wrote:
On 19/04/2026 20:21, olcott wrote:
On 4/19/2026 3:59 AM, Mikko wrote:
On 18/04/2026 15:58, olcott wrote:
Unknown truths are not elements of the body of
knowledge is a semantic tautology. Did you think
that things that are unknown are known?
No, but that measn that for some sentences X True(X) is >>>>>>>>>>>> unknown and there
is no method to find out.
I don't know about philosophers but mathematicians and >>>>>>>>>>>> logicians don't
find it interesting if all you can say that all knowledge is >>>>>>>>>>>> knowable
and everything else is not.
Ross Finlayson, seemed to endlessly hedge on whether
or not the truth value of the Goldbach conjecture was
known. He seemed to think that there are alternative
analytical frameworks that make the question of whether
or not its truth value is known an ambiguous question.
I needed to refer to unknown truth values specifically
because all "undecidability" when construed correctly
falls into one of two categories.
(a) Semantic incoherence
(b) Unknown truth values.
A centence can be said to be undecidable when it is known that >>>>>>>>>> neither
the sentence nor its negation is a theorem.
When we skip model theory and and define True and False
as the existence of a back chained sequence of inference
steps of expressions x or ~x reaching axioms
It is not useful to define new terms for comcepts that already have >>>>>>>> good terms.
The result of undecidability proves that the current
foundations are incoherent in the same way that
Russell's paradox proved that naive set theory had
a glitch.
Hardly the same way as Russell's paradox proves that there is no
undecidability in the naive set theory.
If the sequence of inference steps is restricted to
valid inferences the term "True" as defined above then "sentence is >>>>>>>> true" is just another way to say "sentence is a theorem".
then it is a yes or no question that has no correct yes
or no answer within the formal system.
Even if a question has no answer within a formal theory of natural >>>>>>>> numbers it may have an answer in the natural numbers themselves. >>>>>>>>
My system is based on simple type theory and formalized
natural language.
This makes it a yes or no question that has no
correct yes or no answer at all anywhere, thus
an incorrect polar question.
How does your system handle questions that are not known to have a >>>>>>>> yes or no answer but k´nor known to lack such answer, either, >>>>>>>> e.g. Goldbach's conjecture ?
out-of-scope of the body of knowledge.
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
So the question whether something is in the scope of your system
is not in the scope of your system? OK, but shoudn't such questions >>>>>> be answerable anyway?
The truth value of the Goldbach conjecture might
be unknowable if it is true and the only way to
prove it is true is an infinite number of steps.
Peano arithmetic is unsolvable, i.e., there is no method to find
out whether a particular sentence (for exmaple Goldbach conjecture)
is provable or not. If you find a proof then you know it but it is
possible that you never find, no matter how much you search.
Goldbach is unknowable if it is true because
verifying that it is true requires an infinite
number of steps.
That is not known. Perhaps there is an unknown proof that proves it.
This just means that the truth> value of Goldbach is outside of thebody of
knowledge thus outside of the scope of my project.While the truth value is not in the body of knowledge someone may
some day find a way to infer it from what is known.
A proposition P (or its negation) ¬P has a well-founded
justification tree if there is a sequence of back-chained
inference steps from P or ¬P to the axioms of the formal
system. Otherwise P is ungrounded.
On 24/04/2026 19:24, olcott wrote:
On 4/24/2026 1:08 AM, Mikko wrote:
On 23/04/2026 16:32, olcott wrote:
On 4/23/2026 1:35 AM, Mikko wrote:
On 22/04/2026 10:45, olcott wrote:
On 4/22/2026 2:03 AM, Mikko wrote:
On 21/04/2026 16:22, olcott wrote:
On 4/21/2026 1:30 AM, Mikko wrote:
On 20/04/2026 16:31, olcott wrote:
On 4/20/2026 3:49 AM, Mikko wrote:
On 19/04/2026 20:21, olcott wrote:
On 4/19/2026 3:59 AM, Mikko wrote:
On 18/04/2026 15:58, olcott wrote:
Unknown truths are not elements of the body of
knowledge is a semantic tautology. Did you think
that things that are unknown are known?
No, but that measn that for some sentences X True(X) is >>>>>>>>>>>>> unknown and there
is no method to find out.
I don't know about philosophers but mathematicians and >>>>>>>>>>>>> logicians don't
find it interesting if all you can say that all knowledge >>>>>>>>>>>>> is knowable
and everything else is not.
Ross Finlayson, seemed to endlessly hedge on whether
or not the truth value of the Goldbach conjecture was
known. He seemed to think that there are alternative
analytical frameworks that make the question of whether >>>>>>>>>>>> or not its truth value is known an ambiguous question. >>>>>>>>>>>>
I needed to refer to unknown truth values specifically >>>>>>>>>>>> because all "undecidability" when construed correctly
falls into one of two categories.
(a) Semantic incoherence
(b) Unknown truth values.
A centence can be said to be undecidable when it is known >>>>>>>>>>> that neither
the sentence nor its negation is a theorem.
When we skip model theory and and define True and False
as the existence of a back chained sequence of inference
steps of expressions x or ~x reaching axioms
It is not useful to define new terms for comcepts that already >>>>>>>>> have
good terms.
The result of undecidability proves that the current
foundations are incoherent in the same way that
Russell's paradox proved that naive set theory had
a glitch.
Hardly the same way as Russell's paradox proves that there is no >>>>>>> undecidability in the naive set theory.
If the sequence of inference steps is restricted to
valid inferences the term "True" as defined above then
"sentence is
true" is just another way to say "sentence is a theorem".
then it is a yes or no question that has no correct yes
or no answer within the formal system.
Even if a question has no answer within a formal theory of natural >>>>>>>>> numbers it may have an answer in the natural numbers themselves. >>>>>>>>>
My system is based on simple type theory and formalized
natural language.
This makes it a yes or no question that has no
correct yes or no answer at all anywhere, thus
an incorrect polar question.
How does your system handle questions that are not known to have a >>>>>>>>> yes or no answer but k´nor known to lack such answer, either, >>>>>>>>> e.g. Goldbach's conjecture ?
out-of-scope of the body of knowledge.
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
So the question whether something is in the scope of your system >>>>>>> is not in the scope of your system? OK, but shoudn't such questions >>>>>>> be answerable anyway?
The truth value of the Goldbach conjecture might
be unknowable if it is true and the only way to
prove it is true is an infinite number of steps.
Peano arithmetic is unsolvable, i.e., there is no method to find
out whether a particular sentence (for exmaple Goldbach conjecture)
is provable or not. If you find a proof then you know it but it is
possible that you never find, no matter how much you search.
Goldbach is unknowable if it is true because
verifying that it is true requires an infinite
number of steps.
That is not known. Perhaps there is an unknown proof that proves it.
This just means that the truth> value of Goldbach is outside ofthe body of
knowledge thus outside of the scope of my project.While the truth value is not in the body of knowledge someone may
some day find a way to infer it from what is known.
A proposition P (or its negation) ¬P has a well-founded
justification tree if there is a sequence of back-chained
inference steps from P or ¬P to the axioms of the formal
system. Otherwise P is ungrounded.
That does not help if it is not known whether such sequence of
inference steps exists.
On 4/25/2026 3:20 AM, Mikko wrote:
On 24/04/2026 19:24, olcott wrote:
On 4/24/2026 1:08 AM, Mikko wrote:
On 23/04/2026 16:32, olcott wrote:
On 4/23/2026 1:35 AM, Mikko wrote:
On 22/04/2026 10:45, olcott wrote:
On 4/22/2026 2:03 AM, Mikko wrote:
On 21/04/2026 16:22, olcott wrote:
On 4/21/2026 1:30 AM, Mikko wrote:
On 20/04/2026 16:31, olcott wrote:
On 4/20/2026 3:49 AM, Mikko wrote:
On 19/04/2026 20:21, olcott wrote:
On 4/19/2026 3:59 AM, Mikko wrote:
On 18/04/2026 15:58, olcott wrote:
Unknown truths are not elements of the body of
knowledge is a semantic tautology. Did you think >>>>>>>>>>>>>>> that things that are unknown are known?
No, but that measn that for some sentences X True(X) is >>>>>>>>>>>>>> unknown and there
is no method to find out.
I don't know about philosophers but mathematicians and >>>>>>>>>>>>>> logicians don't
find it interesting if all you can say that all knowledge >>>>>>>>>>>>>> is knowable
and everything else is not.
Ross Finlayson, seemed to endlessly hedge on whether >>>>>>>>>>>>> or not the truth value of the Goldbach conjecture was >>>>>>>>>>>>> known. He seemed to think that there are alternative >>>>>>>>>>>>> analytical frameworks that make the question of whether >>>>>>>>>>>>> or not its truth value is known an ambiguous question. >>>>>>>>>>>>>
I needed to refer to unknown truth values specifically >>>>>>>>>>>>> because all "undecidability" when construed correctly >>>>>>>>>>>>> falls into one of two categories.
(a) Semantic incoherence
(b) Unknown truth values.
A centence can be said to be undecidable when it is known >>>>>>>>>>>> that neither
the sentence nor its negation is a theorem.
When we skip model theory and and define True and False
as the existence of a back chained sequence of inference >>>>>>>>>>> steps of expressions x or ~x reaching axioms
It is not useful to define new terms for comcepts that already >>>>>>>>>> have
good terms.
The result of undecidability proves that the current
foundations are incoherent in the same way that
Russell's paradox proved that naive set theory had
a glitch.
Hardly the same way as Russell's paradox proves that there is no >>>>>>>> undecidability in the naive set theory.
If the sequence of inference steps is restricted to
valid inferences the term "True" as defined above then
"sentence is
true" is just another way to say "sentence is a theorem".
then it is a yes or no question that has no correct yes
or no answer within the formal system.
Even if a question has no answer within a formal theory of >>>>>>>>>> natural
numbers it may have an answer in the natural numbers themselves. >>>>>>>>>>
My system is based on simple type theory and formalized
natural language.
This makes it a yes or no question that has no
correct yes or no answer at all anywhere, thus
an incorrect polar question.
How does your system handle questions that are not known to >>>>>>>>>> have a
yes or no answer but k´nor known to lack such answer, either, >>>>>>>>>> e.g. Goldbach's conjecture ?
out-of-scope of the body of knowledge.
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
So the question whether something is in the scope of your system >>>>>>>> is not in the scope of your system? OK, but shoudn't such questions >>>>>>>> be answerable anyway?
The truth value of the Goldbach conjecture might
be unknowable if it is true and the only way to
prove it is true is an infinite number of steps.
Peano arithmetic is unsolvable, i.e., there is no method to find
out whether a particular sentence (for exmaple Goldbach conjecture) >>>>>> is provable or not. If you find a proof then you know it but it is >>>>>> possible that you never find, no matter how much you search.
Goldbach is unknowable if it is true because
verifying that it is true requires an infinite
number of steps.
That is not known. Perhaps there is an unknown proof that proves it.
This just means that the truth> value of Goldbach is outside ofthe body of
knowledge thus outside of the scope of my project.While the truth value is not in the body of knowledge someone may
some day find a way to infer it from what is known.
A proposition P (or its negation) ¬P has a well-founded
justification tree if there is a sequence of back-chained
inference steps from P or ¬P to the axioms of the formal
system. Otherwise P is ungrounded.
That does not help if it is not known whether such sequence of
inference steps exists.
It does help for the halting problem counter-example input
and it does help for the 1931 Incompleteness Theorem. Both
of these are ruled ungrounded rather than undecidable.
On 25/04/2026 15:25, olcott wrote:
On 4/25/2026 3:20 AM, Mikko wrote:
inference steps exists.That does not help if it is not known whether such sequence of
It does help for the halting problem counter-example input
and it does help for the 1931 Incompleteness Theorem. Both
of these are ruled ungrounded rather than undecidable.
The halting problem counter-example is grounded. One of the following statements is true per the definition of "halting decider":
- The proposed decider accepts the counter-example.
- The proposed decider rejects the counter-example.
- The proposed decider is not a halting decider.
It is not necessary to know which one is true. Each one is sufficient
to infer that the propsed decider is not a halting decider.
Whether a halting oracle is possible is another problem. Accordint to
the CHurch-Turing thesis it isn't but there is no known proof.
On 4/26/2026 3:09 AM, Mikko wrote:
On 25/04/2026 15:25, olcott wrote:
On 4/25/2026 3:20 AM, Mikko wrote:
inference steps exists.That does not help if it is not known whether such sequence of
It does help for the halting problem counter-example input
and it does help for the 1931 Incompleteness Theorem. Both
of these are ruled ungrounded rather than undecidable.
The halting problem counter-example is grounded. One of the following
statements is true per the definition of "halting decider":
- The proposed decider accepts the counter-example.
- The proposed decider rejects the counter-example.
- The proposed decider is not a halting decider.
It is not necessary to know which one is true. Each one is sufficient
to infer that the propsed decider is not a halting decider.
Whether a halting oracle is possible is another problem. Accordint to
the CHurch-Turing thesis it isn't but there is no known proof.
typedef int (*ptr)();
int HHH(ptr P);
int DD()
{
int Halt_Status = HHH(DD);
if (Halt_Status)
HERE: goto HERE;
return Halt_Status;
}
int main()
{
HHH(DD);
}
Proof theoretic halt prover HHH is fully operational
code since 2022 can correctly rejects its input DD
as lacking a well-founded justification tree.
HHH is on line 1081
https://github.com/plolcott/x86utm/blob/master/Halt7.c
HHH is a proof-theoretic-semantics halt prover:
it accepts exactly those programs whose simulation
admits a finite, well-founded justification tree,
and rejects those whose simulation is non-well-founded.
Under the operational semantics of C as implemented
by HHH, the simulation of DD induces a recursive
self-reference cycle; therefore, no finite, well-founded
justification tree exists for DD under HHH.
On 4/26/2026 3:09 AM, Mikko wrote:
On 25/04/2026 15:25, olcott wrote:
On 4/25/2026 3:20 AM, Mikko wrote:
inference steps exists.That does not help if it is not known whether such sequence of
It does help for the halting problem counter-example input
and it does help for the 1931 Incompleteness Theorem. Both
of these are ruled ungrounded rather than undecidable.
The halting problem counter-example is grounded. One of the following
statements is true per the definition of "halting decider":
- The proposed decider accepts the counter-example.
- The proposed decider rejects the counter-example.
- The proposed decider is not a halting decider.
It is not necessary to know which one is true. Each one is sufficient
to infer that the propsed decider is not a halting decider.
Whether a halting oracle is possible is another problem. Accordint to
the CHurch-Turing thesis it isn't but there is no known proof.
typedef int (*ptr)();
int HHH(ptr P);
int DD()
{
int Halt_Status = HHH(DD);
if (Halt_Status)
HERE: goto HERE;
return Halt_Status;
}
int main()
{
HHH(DD);
}
Proof theoretic halt prover HHH is fully operational
code since 2022 can correctly rejects its input DD
as lacking a well-founded justification tree.
HHH is on line 1081
https://github.com/plolcott/x86utm/blob/master/Halt7.c
HHH is a proof-theoretic-semantics halt prover:
it accepts exactly those programs whose simulation
admits a finite, well-founded justification tree,
and rejects those whose simulation is non-well-founded.
Under the operational semantics of C as implemented--
by HHH, the simulation of DD induces a recursive
self-reference cycle; therefore, no finite, well-founded
justification tree exists for DD under HHH.
On 26/04/2026 16:22, olcott wrote:
On 4/26/2026 3:09 AM, Mikko wrote:
On 25/04/2026 15:25, olcott wrote:
On 4/25/2026 3:20 AM, Mikko wrote:
That does not help if it is not known whether such sequence of >>>>> inference steps exists.
It does help for the halting problem counter-example input
and it does help for the 1931 Incompleteness Theorem. Both
of these are ruled ungrounded rather than undecidable.
The halting problem counter-example is grounded. One of the following
statements is true per the definition of "halting decider":
- The proposed decider accepts the counter-example.
- The proposed decider rejects the counter-example.
- The proposed decider is not a halting decider.
It is not necessary to know which one is true. Each one is sufficient
to infer that the propsed decider is not a halting decider.
Whether a halting oracle is possible is another problem. Accordint to
the CHurch-Turing thesis it isn't but there is no known proof.
typedef int (*ptr)();
int HHH(ptr P);
int DD()
{
int Halt_Status = HHH(DD);
if (Halt_Status)
HERE: goto HERE;
return Halt_Status;
}
int main()
{
HHH(DD);
}
Proof theoretic halt prover HHH is fully operational
code since 2022 can correctly rejects its input DD
as lacking a well-founded justification tree.
Which is not quite correct. The input should be rejected as incomplete (unless the exact meaning of HHH is a part of the input language).
It does not make sense to say that the input has or lacks a
justification tree
(just like it does not make sense that the
input "25 + 79" to an addition program has or lacks a justification
tree). There is nothing in the input that requires a justification
tree. The output must have a justification tree, though usually a
decider is not required to show it. Also the justification tree
(or some other form of proof) of the correctness is often required.
HHH is on line 1081
https://github.com/plolcott/x86utm/blob/master/Halt7.c
If HHH in DD is interpreted to mean that routime then the question
whether a call to DD ever returns (instead of looping forever or
aborting for stack or heap overflow or some other reason) is valid.
HHH is a proof-theoretic-semantics halt prover:
it accepts exactly those programs whose simulation
admits a finite, well-founded justification tree,
and rejects those whose simulation is non-well-founded.
It does not count as a prover as it does not output a proof.
For a halting computation the excution trace is almost all
of a proof but for a non-halting computation it isn't.
--Under the operational semantics of C as implemented
by HHH, the simulation of DD induces a recursive
self-reference cycle; therefore, no finite, well-founded
justification tree exists for DD under HHH.
On 4/27/2026 4:22 AM, Mikko wrote:
On 26/04/2026 16:22, olcott wrote:
On 4/26/2026 3:09 AM, Mikko wrote:
On 25/04/2026 15:25, olcott wrote:
On 4/25/2026 3:20 AM, Mikko wrote:
That does not help if it is not known whether such sequence of >>>>>> inference steps exists.
It does help for the halting problem counter-example input
and it does help for the 1931 Incompleteness Theorem. Both
of these are ruled ungrounded rather than undecidable.
The halting problem counter-example is grounded. One of the following
statements is true per the definition of "halting decider":
- The proposed decider accepts the counter-example.
- The proposed decider rejects the counter-example.
- The proposed decider is not a halting decider.
It is not necessary to know which one is true. Each one is sufficient
to infer that the propsed decider is not a halting decider.
Whether a halting oracle is possible is another problem. Accordint to
the CHurch-Turing thesis it isn't but there is no known proof.
typedef int (*ptr)();
int HHH(ptr P);
int DD()
{
int Halt_Status = HHH(DD);
if (Halt_Status)
HERE: goto HERE;
return Halt_Status;
}
int main()
{
HHH(DD);
}
Proof theoretic halt prover HHH is fully operational
code since 2022 can correctly rejects its input DD
as lacking a well-founded justification tree.
Which is not quite correct. The input should be rejected as incomplete
(unless the exact meaning of HHH is a part of the input language).
Until you become a PTS expert your critique of
my work is like a carpenter trying to provide
medical advice on the basis of carpentry skills.
On 27/04/2026 17:47, olcott wrote:
On 4/27/2026 4:22 AM, Mikko wrote:
On 26/04/2026 16:22, olcott wrote:
On 4/26/2026 3:09 AM, Mikko wrote:
On 25/04/2026 15:25, olcott wrote:
On 4/25/2026 3:20 AM, Mikko wrote:
That does not help if it is not known whether such sequence of >>>>>>> inference steps exists.
It does help for the halting problem counter-example input
and it does help for the 1931 Incompleteness Theorem. Both
of these are ruled ungrounded rather than undecidable.
The halting problem counter-example is grounded. One of the following >>>>> statements is true per the definition of "halting decider":
- The proposed decider accepts the counter-example.
- The proposed decider rejects the counter-example.
- The proposed decider is not a halting decider.
It is not necessary to know which one is true. Each one is sufficient >>>>> to infer that the propsed decider is not a halting decider.
Whether a halting oracle is possible is another problem. Accordint to >>>>> the CHurch-Turing thesis it isn't but there is no known proof.
typedef int (*ptr)();
int HHH(ptr P);
int DD()
{
int Halt_Status = HHH(DD);
if (Halt_Status)
HERE: goto HERE;
return Halt_Status;
}
int main()
{
HHH(DD);
}
Proof theoretic halt prover HHH is fully operational
code since 2022 can correctly rejects its input DD
as lacking a well-founded justification tree.
Which is not quite correct. The input should be rejected as incomplete
(unless the exact meaning of HHH is a part of the input language).
Until you become a PTS expert your critique of
my work is like a carpenter trying to provide
medical advice on the basis of carpentry skills.
If your best argument is an ad-hominem fallacy you have nothing
worth of notice to say about the halting problem.
On 4/28/2026 2:55 AM, Mikko wrote:
On 27/04/2026 17:47, olcott wrote:
On 4/27/2026 4:22 AM, Mikko wrote:
On 26/04/2026 16:22, olcott wrote:
On 4/26/2026 3:09 AM, Mikko wrote:
On 25/04/2026 15:25, olcott wrote:
On 4/25/2026 3:20 AM, Mikko wrote:
That does not help if it is not known whether such sequence of >>>>>>>> inference steps exists.
It does help for the halting problem counter-example input
and it does help for the 1931 Incompleteness Theorem. Both
of these are ruled ungrounded rather than undecidable.
The halting problem counter-example is grounded. One of the following >>>>>> statements is true per the definition of "halting decider":
- The proposed decider accepts the counter-example.
- The proposed decider rejects the counter-example.
- The proposed decider is not a halting decider.
It is not necessary to know which one is true. Each one is sufficient >>>>>> to infer that the propsed decider is not a halting decider.
Whether a halting oracle is possible is another problem. Accordint to >>>>>> the CHurch-Turing thesis it isn't but there is no known proof.
typedef int (*ptr)();
int HHH(ptr P);
int DD()
{
int Halt_Status = HHH(DD);
if (Halt_Status)
HERE: goto HERE;
return Halt_Status;
}
int main()
{
HHH(DD);
}
Proof theoretic halt prover HHH is fully operational
code since 2022 can correctly rejects its input DD
as lacking a well-founded justification tree.
Which is not quite correct. The input should be rejected as incomplete >>>> (unless the exact meaning of HHH is a part of the input language).
Until you become a PTS expert your critique of
my work is like a carpenter trying to provide
medical advice on the basis of carpentry skills.
If your best argument is an ad-hominem fallacy you have nothing
worth of notice to say about the halting problem.
I am pointing out a specific mandatory prerequisite
that you lack.
It is incorrect to dismiss a view
that you do not understand on the basis of your
own lack of understanding.
On 4/24/2026 1:08 AM, Mikko wrote:
On 23/04/2026 16:32, olcott wrote:
On 4/23/2026 1:35 AM, Mikko wrote:
On 22/04/2026 10:45, olcott wrote:
On 4/22/2026 2:03 AM, Mikko wrote:
On 21/04/2026 16:22, olcott wrote:
On 4/21/2026 1:30 AM, Mikko wrote:
On 20/04/2026 16:31, olcott wrote:
On 4/20/2026 3:49 AM, Mikko wrote:
On 19/04/2026 20:21, olcott wrote:
On 4/19/2026 3:59 AM, Mikko wrote:
On 18/04/2026 15:58, olcott wrote:
Unknown truths are not elements of the body of
knowledge is a semantic tautology. Did you think
that things that are unknown are known?
No, but that measn that for some sentences X True(X) is >>>>>>>>>>>> unknown and there
is no method to find out.
I don't know about philosophers but mathematicians and >>>>>>>>>>>> logicians don't
find it interesting if all you can say that all knowledge is >>>>>>>>>>>> knowable
and everything else is not.
Ross Finlayson, seemed to endlessly hedge on whether
or not the truth value of the Goldbach conjecture was
known. He seemed to think that there are alternative
analytical frameworks that make the question of whether
or not its truth value is known an ambiguous question.
I needed to refer to unknown truth values specifically
because all "undecidability" when construed correctly
falls into one of two categories.
(a) Semantic incoherence
(b) Unknown truth values.
A centence can be said to be undecidable when it is known that >>>>>>>>>> neither
the sentence nor its negation is a theorem.
When we skip model theory and and define True and False
as the existence of a back chained sequence of inference
steps of expressions x or ~x reaching axioms
It is not useful to define new terms for comcepts that already have >>>>>>>> good terms.
The result of undecidability proves that the current
foundations are incoherent in the same way that
Russell's paradox proved that naive set theory had
a glitch.
Hardly the same way as Russell's paradox proves that there is no
undecidability in the naive set theory.
If the sequence of inference steps is restricted to
valid inferences the term "True" as defined above then "sentence is >>>>>>>> true" is just another way to say "sentence is a theorem".
then it is a yes or no question that has no correct yes
or no answer within the formal system.
Even if a question has no answer within a formal theory of natural >>>>>>>> numbers it may have an answer in the natural numbers themselves. >>>>>>>>
My system is based on simple type theory and formalized
natural language.
This makes it a yes or no question that has no
correct yes or no answer at all anywhere, thus
an incorrect polar question.
How does your system handle questions that are not known to have a >>>>>>>> yes or no answer but k´nor known to lack such answer, either, >>>>>>>> e.g. Goldbach's conjecture ?
out-of-scope of the body of knowledge.
"true on the basis of meaning expressed in language"
reliably computable for the entire body of knowledge.
So the question whether something is in the scope of your system
is not in the scope of your system? OK, but shoudn't such questions >>>>>> be answerable anyway?
The truth value of the Goldbach conjecture might
be unknowable if it is true and the only way to
prove it is true is an infinite number of steps.
Peano arithmetic is unsolvable, i.e., there is no method to find
out whether a particular sentence (for exmaple Goldbach conjecture)
is provable or not. If you find a proof then you know it but it is
possible that you never find, no matter how much you search.
Goldbach is unknowable if it is true because
verifying that it is true requires an infinite
number of steps.
That is not known. Perhaps there is an unknown proof that proves it.
This just means that the truth> value of Goldbach is outside of thebody of
knowledge thus outside of the scope of my project.While the truth value is not in the body of knowledge someone may
some day find a way to infer it from what is known.
A proposition P (or its negation) ¬P has a well-founded
justification tree if there is a sequence of back-chained
inference steps from P or ¬P to the axioms of the formal
system. Otherwise P is ungrounded.
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,116 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 85:27:51 |
| Calls: | 14,305 |
| Files: | 186,338 |
| D/L today: |
650 files (185M bytes) |
| Messages: | 2,525,478 |