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) -4P has a well-founded
justification tree if there is a sequence of back-chained
inference steps from P or -4P 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) -4P has a well-founded
justification tree if there is a sequence of back-chained
inference steps from P or -4P 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) -4P has a well-founded
justification tree if there is a sequence of back-chained
inference steps from P or -4P 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()
{
-a int Halt_Status = HHH(DD);
-a if (Halt_Status)
-a-a-a HERE: goto HERE;
-a return Halt_Status;
}
int main()
{
-a 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()
{
-a int Halt_Status = HHH(DD);
-a if (Halt_Status)
-a-a-a HERE: goto HERE;
-a return Halt_Status;
}
int main()
{
-a 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()
{
-a-a int Halt_Status = HHH(DD);
-a-a if (Halt_Status)
-a-a-a-a HERE: goto HERE;
-a-a return Halt_Status;
}
int main()
{
-a-a 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()
{
-a-a int Halt_Status = HHH(DD);
-a-a if (Halt_Status)
-a-a-a-a HERE: goto HERE;
-a-a return Halt_Status;
}
int main()
{
-a-a 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()
{
-a-a int Halt_Status = HHH(DD);
-a-a if (Halt_Status)
-a-a-a-a HERE: goto HERE;
-a-a return Halt_Status;
}
int main()
{
-a-a 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()
{
-a-a int Halt_Status = HHH(DD);
-a-a if (Halt_Status)
-a-a-a-a HERE: goto HERE;
-a-a return Halt_Status;
}
int main()
{
-a-a 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) -4P has a well-founded
justification tree if there is a sequence of back-chained
inference steps from P or -4P to the axioms of the formal
system. Otherwise P is ungrounded.
| Sysop: | Amessyroom |
|---|---|
| Location: | Fayetteville, NC |
| Users: | 65 |
| Nodes: | 6 (1 / 5) |
| Uptime: | 01:02:19 |
| Calls: | 862 |
| Files: | 1,311 |
| D/L today: |
10 files (20,373K bytes) |
| Messages: | 264,187 |