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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection feeds back
into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of the
fact of infinite recursion gets invalidate by actions taken after the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the machine with
an external detector isn't the same as just running the machine...
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection feeds back
into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of the
fact of infinite recursion gets invalidate by actions taken after the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the machine with
an external detector isn't the same as just running the machine...
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection feeds back
into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of the
fact of infinite recursion gets invalidate by actions taken after the
measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the machine
with an external detector isn't the same as just running the machine...
Your problem is that with "machines" you can't make a decider that can't
be incorporated into a valid input.
There is a fundamental limitation of computation once this "recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would need to be
able to be given a level-H Oracle input, which we can show it can't handle.
A level-N Oracle machine can only handle inputs based on at most
level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't handle a full maximal power computation input, and thus can't decide for *ALL* machine inputs.
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection feeds
back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of the
fact of infinite recursion gets invalidate by actions taken after the
measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the machine
with an external detector isn't the same as just running the machine...
Your problem is that with "machines" you can't make a decider that
can't be incorporated into a valid input.
There is a fundamental limitation of computation once this "recursion"
becomes possible.
Even with Oracle machines, as a level-N Oracle machine would need to
be able to be given a level-H Oracle input, which we can show it can't
handle.
A level-N Oracle machine can only handle inputs based on at most
level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't handle
a full maximal power computation input, and thus can't decide for
*ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to express
this computation?
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
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);
}
When DD is simulated by proof theoretic halt prover HHH the recursive simulation that HHH detects allows DD to be rejected as not having a well-founded justification tree. The only inputs left out are
semantically unsound.
On 2026-04-10 17:03, olcott wrote:
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
"proof theoretic halting prover" is a term used only by you and one
which you have never defined, let alone coherently defined.
André
On 4/10/2026 5:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection feeds
back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of the
fact of infinite recursion gets invalidate by actions taken after
the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the machine
with an external detector isn't the same as just running the machine... >>>>
Your problem is that with "machines" you can't make a decider that
can't be incorporated into a valid input.
There is a fundamental limitation of computation once this
"recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would need to
be able to be given a level-H Oracle input, which we can show it
can't handle.
A level-N Oracle machine can only handle inputs based on at most
level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't
handle a full maximal power computation input, and thus can't decide
for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to express
this computation?
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
The only other category of what is mistakenly called undecidable
input are things that are outside of the body of knowledge such
as the truth value of the Goldbach conjecture.
All of every kind of "paradox" has always only been only
been undiscovered incoherence.
On 4/10/26 4:03 PM, olcott wrote:That you just ignored proof theoretic semantics and
On 4/10/2026 5:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection feeds
back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of
the fact of infinite recursion gets invalidate by actions taken
after the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the machine
with an external detector isn't the same as just running the
machine...
Your problem is that with "machines" you can't make a decider that
can't be incorporated into a valid input.
There is a fundamental limitation of computation once this
"recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would need to
be able to be given a level-H Oracle input, which we can show it
can't handle.
A level-N Oracle machine can only handle inputs based on at most
level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't
handle a full maximal power computation input, and thus can't decide
for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to express
this computation?
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
the problem is if u run the DD()
On 4/10/2026 10:05 PM, dart200 wrote:
On 4/10/26 4:03 PM, olcott wrote:That you just ignored proof theoretic semantics and
On 4/10/2026 5:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection feeds >>>>>> back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of
the fact of infinite recursion gets invalidate by actions taken
after the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the machine >>>>>> with an external detector isn't the same as just running the
machine...
Your problem is that with "machines" you can't make a decider that
can't be incorporated into a valid input.
There is a fundamental limitation of computation once this
"recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would need
to be able to be given a level-H Oracle input, which we can show it >>>>> can't handle.
A level-N Oracle machine can only handle inputs based on at most
level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't
handle a full maximal power computation input, and thus can't
decide for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to express
this computation?
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
the problem is if u run the DD()
cannot possibly grasp what I said correctly.
As a proof theoretic halt prover DD is absolutely
and positively rejected. You cannot see this until
you first totally understand all of proof theoretic
semantics.
It like like I say "to bake a cake..." and you say
that I used the hammer and screw driver incorrectly
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
On 4/10/26 8:19 PM, olcott wrote:
On 4/10/2026 10:05 PM, dart200 wrote:
On 4/10/26 4:03 PM, olcott wrote:That you just ignored proof theoretic semantics and
On 4/10/2026 5:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection feeds >>>>>>> back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of >>>>>>> the fact of infinite recursion gets invalidate by actions taken >>>>>>> after the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the
machine with an external detector isn't the same as just running >>>>>>> the machine...
Your problem is that with "machines" you can't make a decider that >>>>>> can't be incorporated into a valid input.
There is a fundamental limitation of computation once this
"recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would need >>>>>> to be able to be given a level-H Oracle input, which we can show
it can't handle.
A level-N Oracle machine can only handle inputs based on at most
level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't
handle a full maximal power computation input, and thus can't
decide for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to
express this computation?
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
the problem is if u run the DD()
cannot possibly grasp what I said correctly.
As a proof theoretic halt prover DD is absolutely
and positively rejected. You cannot see this until
you first totally understand all of proof theoretic
semantics.
It like like I say "to bake a cake..." and you say
that I used the hammer and screw driver incorrectly
is DD() executable or not???
On 08/04/2026 21:33, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic Semantics as it
is anyway. If a computation halts it can be proven to halt, although
the proof may be unknown. If a computation can be proven to halt it
halts even when the proof is unknown.
The problem is that there is no complete method to find out whether
the proof exists. Using Proof Theoretic Semantics does not help.
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic Semantics as it
*Become a PTS expert before you dare say these things*
All of the meaning of DD to proof theoretic semantics
halt prover HHH is derived entirely by its inference
steps and the loop in these steps always means bad input.
is anyway. If a computation halts it can be proven to halt, although
the proof may be unknown. If a computation can be proven to halt it
halts even when the proof is unknown.
An input that does the opposite of whatever its
proof theoretic halt prover reports has always been
semantically incoherent. Every "paradox" that ever
was has only ever been undiscovered semantically
incoherence.
The problem is that there is no complete method to find out whether
the proof exists. Using Proof Theoretic Semantics does not help.
On 04/11/2026 07:03 AM, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic Semantics as it
*Become a PTS expert before you dare say these things*
All of the meaning of DD to proof theoretic semantics
halt prover HHH is derived entirely by its inference
steps and the loop in these steps always means bad input.
is anyway. If a computation halts it can be proven to halt, although
the proof may be unknown. If a computation can be proven to halt it
halts even when the proof is unknown.
An input that does the opposite of whatever its
proof theoretic halt prover reports has always been
semantically incoherent. Every "paradox" that ever
was has only ever been undiscovered semantically
incoherence.
The problem is that there is no complete method to find out whether
the proof exists. Using Proof Theoretic Semantics does not help.
Mathematical "independence" isn't "incoherence", rather,
false closures or false completions or false axioms
result, "incoherence".
Thusly, if you're finding incoherence, you're missing
something, or, as like the albatross, have some
unwanted baggage.
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection feeds
back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of the
fact of infinite recursion gets invalidate by actions taken after the
measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the machine
with an external detector isn't the same as just running the machine...
Your problem is that with "machines" you can't make a decider that
can't be incorporated into a valid input.
There is a fundamental limitation of computation once this "recursion"
becomes possible.
Even with Oracle machines, as a level-N Oracle machine would need to
be able to be given a level-H Oracle input, which we can show it can't
handle.
A level-N Oracle machine can only handle inputs based on at most
level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't handle
a full maximal power computation input, and thus can't decide for
*ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to express
this computation?
On 4/10/2026 5:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection feeds
back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of the
fact of infinite recursion gets invalidate by actions taken after
the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the machine
with an external detector isn't the same as just running the machine... >>>>
Your problem is that with "machines" you can't make a decider that
can't be incorporated into a valid input.
There is a fundamental limitation of computation once this
"recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would need to
be able to be given a level-H Oracle input, which we can show it
can't handle.
A level-N Oracle machine can only handle inputs based on at most
level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't
handle a full maximal power computation input, and thus can't decide
for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to express
this computation?
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
The only other category of what is mistakenly called undecidable
input are things that are outside of the body of knowledge such
as the truth value of the Goldbach conjecture.
All of every kind of "paradox" has always only been only
been undiscovered incoherence.
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
On 4/8/2026 1:33 PM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
This cannot possibly be sufficiently understood until
one first becomes a truth theoretic semantics expert.
On 4/11/2026 12:07 AM, dart200 wrote:
On 4/10/26 8:19 PM, olcott wrote:
On 4/10/2026 10:05 PM, dart200 wrote:
On 4/10/26 4:03 PM, olcott wrote:That you just ignored proof theoretic semantics and
On 4/10/2026 5:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>> tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection
feeds back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of >>>>>>>> the fact of infinite recursion gets invalidate by actions taken >>>>>>>> after the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the
machine with an external detector isn't the same as just running >>>>>>>> the machine...
Your problem is that with "machines" you can't make a decider
that can't be incorporated into a valid input.
There is a fundamental limitation of computation once this
"recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would need >>>>>>> to be able to be given a level-H Oracle input, which we can show >>>>>>> it can't handle.
A level-N Oracle machine can only handle inputs based on at most >>>>>>> level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't >>>>>>> handle a full maximal power computation input, and thus can't
decide for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to
express this computation?
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
the problem is if u run the DD()
cannot possibly grasp what I said correctly.
As a proof theoretic halt prover DD is absolutely
and positively rejected. You cannot see this until
you first totally understand all of proof theoretic
semantics.
It like like I say "to bake a cake..." and you say
that I used the hammer and screw driver incorrectly
is DD() executable or not???
As far as a proof theoretic halt prover goes
that question is the same as asking do you
need a screwdriver or a hammer to bake an
angel food cake. HHH just correctly rejects
DD as bad input. That's all there is to it in
proof theoretic semantics.
In PTS it is the inference steps themselves
that derive ALL of the semantic meaning of DD.
On 4/11/26 6:54 AM, olcott wrote:
On 4/11/2026 12:07 AM, dart200 wrote:
On 4/10/26 8:19 PM, olcott wrote:
On 4/10/2026 10:05 PM, dart200 wrote:
On 4/10/26 4:03 PM, olcott wrote:That you just ignored proof theoretic semantics and
On 4/10/2026 5:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>>> tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection >>>>>>>>> feeds back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement >>>>>>>>> of the fact of infinite recursion gets invalidate by actions >>>>>>>>> taken after the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the
machine with an external detector isn't the same as just
running the machine...
Your problem is that with "machines" you can't make a decider >>>>>>>> that can't be incorporated into a valid input.
There is a fundamental limitation of computation once this
"recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would
need to be able to be given a level-H Oracle input, which we can >>>>>>>> show it can't handle.
A level-N Oracle machine can only handle inputs based on at most >>>>>>>> level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't >>>>>>>> handle a full maximal power computation input, and thus can't >>>>>>>> decide for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to
express this computation?
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
the problem is if u run the DD()
cannot possibly grasp what I said correctly.
As a proof theoretic halt prover DD is absolutely
and positively rejected. You cannot see this until
you first totally understand all of proof theoretic
semantics.
It like like I say "to bake a cake..." and you say
that I used the hammer and screw driver incorrectly
is DD() executable or not???
As far as a proof theoretic halt prover goes
that question is the same as asking do you
need a screwdriver or a hammer to bake an
angel food cake. HHH just correctly rejects
DD as bad input. That's all there is to it in
proof theoretic semantics.
In PTS it is the inference steps themselves
that derive ALL of the semantic meaning of DD.
"is DD() a valid executable machine or not" is a true/false question,
and your response did not answer that question polcott
On 4/11/2026 5:31 PM, dart200 wrote:
On 4/11/26 6:54 AM, olcott wrote:
On 4/11/2026 12:07 AM, dart200 wrote:
On 4/10/26 8:19 PM, olcott wrote:
On 4/10/2026 10:05 PM, dart200 wrote:
On 4/10/26 4:03 PM, olcott wrote:That you just ignored proof theoretic semantics and
On 4/10/2026 5:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>>>> tree. The only inputs left out are semantically unsound. >>>>>>>>>>>
yeah i ran into the same problem,
simulating the recursion with an action after the detection >>>>>>>>>> feeds back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement >>>>>>>>>> of the fact of infinite recursion gets invalidate by actions >>>>>>>>>> taken after the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the >>>>>>>>>> machine with an external detector isn't the same as just
running the machine...
Your problem is that with "machines" you can't make a decider >>>>>>>>> that can't be incorporated into a valid input.
There is a fundamental limitation of computation once this
"recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would >>>>>>>>> need to be able to be given a level-H Oracle input, which we >>>>>>>>> can show it can't handle.
A level-N Oracle machine can only handle inputs based on at most >>>>>>>>> level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't >>>>>>>>> handle a full maximal power computation input, and thus can't >>>>>>>>> decide for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to
express this computation?
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
the problem is if u run the DD()
cannot possibly grasp what I said correctly.
As a proof theoretic halt prover DD is absolutely
and positively rejected. You cannot see this until
you first totally understand all of proof theoretic
semantics.
It like like I say "to bake a cake..." and you say
that I used the hammer and screw driver incorrectly
is DD() executable or not???
As far as a proof theoretic halt prover goes
that question is the same as asking do you
need a screwdriver or a hammer to bake an
angel food cake. HHH just correctly rejects
DD as bad input. That's all there is to it in
proof theoretic semantics.
In PTS it is the inference steps themselves
that derive ALL of the semantic meaning of DD.
"is DD() a valid executable machine or not" is a true/false question,
and your response did not answer that question polcott
As far as a proof theoretic halt prover goes that
question is as relevant to HHH/DD as asking should
HHH have mustard on its pizza?
On 4/10/26 6:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection feeds
back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of the
fact of infinite recursion gets invalidate by actions taken after
the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the machine
with an external detector isn't the same as just running the machine... >>>>
Your problem is that with "machines" you can't make a decider that
can't be incorporated into a valid input.
There is a fundamental limitation of computation once this
"recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would need to
be able to be given a level-H Oracle input, which we can show it
can't handle.
A level-N Oracle machine can only handle inputs based on at most
level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't
handle a full maximal power computation input, and thus can't decide
for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to express
this computation?
Because it has been logically proven.
Unless you want to presume that logic is inherently flawed, as we can
not trust any proof, the assumption of things proven impossible just
isn't allowed.
Your world seems to be based on the assumption that magical unicorns
exist that can allow you to do what has been proven to be impossible,
and thus you live in a fantasy world.
On 4/11/2026 5:31 PM, dart200 wrote:
On 4/11/26 6:54 AM, olcott wrote:
On 4/11/2026 12:07 AM, dart200 wrote:
On 4/10/26 8:19 PM, olcott wrote:
On 4/10/2026 10:05 PM, dart200 wrote:
On 4/10/26 4:03 PM, olcott wrote:That you just ignored proof theoretic semantics and
On 4/10/2026 5:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>>>> tree. The only inputs left out are semantically unsound. >>>>>>>>>>>
yeah i ran into the same problem,
simulating the recursion with an action after the detection >>>>>>>>>> feeds back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement >>>>>>>>>> of the fact of infinite recursion gets invalidate by actions >>>>>>>>>> taken after the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the >>>>>>>>>> machine with an external detector isn't the same as just
running the machine...
Your problem is that with "machines" you can't make a decider >>>>>>>>> that can't be incorporated into a valid input.
There is a fundamental limitation of computation once this
"recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would >>>>>>>>> need to be able to be given a level-H Oracle input, which we >>>>>>>>> can show it can't handle.
A level-N Oracle machine can only handle inputs based on at most >>>>>>>>> level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't >>>>>>>>> handle a full maximal power computation input, and thus can't >>>>>>>>> decide for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to
express this computation?
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
the problem is if u run the DD()
cannot possibly grasp what I said correctly.
As a proof theoretic halt prover DD is absolutely
and positively rejected. You cannot see this until
you first totally understand all of proof theoretic
semantics.
It like like I say "to bake a cake..." and you say
that I used the hammer and screw driver incorrectly
is DD() executable or not???
As far as a proof theoretic halt prover goes
that question is the same as asking do you
need a screwdriver or a hammer to bake an
angel food cake. HHH just correctly rejects
DD as bad input. That's all there is to it in
proof theoretic semantics.
In PTS it is the inference steps themselves
that derive ALL of the semantic meaning of DD.
"is DD() a valid executable machine or not" is a true/false question,
and your response did not answer that question polcott
As far as a proof theoretic halt prover goes that
question is as relevant to HHH/DD as asking should
HHH have mustard on its pizza?
On 4/11/26 3:43 PM, olcott wrote:
On 4/11/2026 5:31 PM, dart200 wrote:
On 4/11/26 6:54 AM, olcott wrote:
On 4/11/2026 12:07 AM, dart200 wrote:
On 4/10/26 8:19 PM, olcott wrote:
On 4/10/2026 10:05 PM, dart200 wrote:
On 4/10/26 4:03 PM, olcott wrote:That you just ignored proof theoretic semantics and
On 4/10/2026 5:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>>>>> tree. The only inputs left out are semantically unsound. >>>>>>>>>>>>
yeah i ran into the same problem,
simulating the recursion with an action after the detection >>>>>>>>>>> feeds back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement >>>>>>>>>>> of the fact of infinite recursion gets invalidate by actions >>>>>>>>>>> taken after the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the >>>>>>>>>>> machine with an external detector isn't the same as just >>>>>>>>>>> running the machine...
Your problem is that with "machines" you can't make a decider >>>>>>>>>> that can't be incorporated into a valid input.
There is a fundamental limitation of computation once this >>>>>>>>>> "recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would >>>>>>>>>> need to be able to be given a level-H Oracle input, which we >>>>>>>>>> can show it can't handle.
A level-N Oracle machine can only handle inputs based on at most >>>>>>>>>> level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) >>>>>>>>>> can't handle a full maximal power computation input, and thus >>>>>>>>>> can't decide for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to >>>>>>>>> express this computation?
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
the problem is if u run the DD()
cannot possibly grasp what I said correctly.
As a proof theoretic halt prover DD is absolutely
and positively rejected. You cannot see this until
you first totally understand all of proof theoretic
semantics.
It like like I say "to bake a cake..." and you say
that I used the hammer and screw driver incorrectly
is DD() executable or not???
As far as a proof theoretic halt prover goes
that question is the same as asking do you
need a screwdriver or a hammer to bake an
angel food cake. HHH just correctly rejects
DD as bad input. That's all there is to it in
proof theoretic semantics.
In PTS it is the inference steps themselves
that derive ALL of the semantic meaning of DD.
"is DD() a valid executable machine or not" is a true/false question,
and your response did not answer that question polcott
As far as a proof theoretic halt prover goes that
question is as relevant to HHH/DD as asking should
HHH have mustard on its pizza?
regardless of whether it's relevant, ur not answering the question:
"is DD() a valid executable machine or not?" is a true/false question,
what is the answer polcott???
On 4/11/2026 11:41 PM, dart200 wrote:
On 4/11/26 3:43 PM, olcott wrote:
On 4/11/2026 5:31 PM, dart200 wrote:
On 4/11/26 6:54 AM, olcott wrote:
On 4/11/2026 12:07 AM, dart200 wrote:
On 4/10/26 8:19 PM, olcott wrote:
On 4/10/2026 10:05 PM, dart200 wrote:
On 4/10/26 4:03 PM, olcott wrote:That you just ignored proof theoretic semantics and
On 4/10/2026 5:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows >>>>>>>>>>>>> DD to be rejected as not having a well-founded justification >>>>>>>>>>>>> tree. The only inputs left out are semantically unsound. >>>>>>>>>>>>>
yeah i ran into the same problem,
simulating the recursion with an action after the detection >>>>>>>>>>>> feeds back into making the detection invalid...
it's a rather weird measurement paradox, like the
measurement of the fact of infinite recursion gets
invalidate by actions taken after the measurement itself >>>>>>>>>>>> happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the >>>>>>>>>>>> machine with an external detector isn't the same as just >>>>>>>>>>>> running the machine...
Your problem is that with "machines" you can't make a decider >>>>>>>>>>> that can't be incorporated into a valid input.
There is a fundamental limitation of computation once this >>>>>>>>>>> "recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would >>>>>>>>>>> need to be able to be given a level-H Oracle input, which we >>>>>>>>>>> can show it can't handle.
A level-N Oracle machine can only handle inputs based on at most >>>>>>>>>>> level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) >>>>>>>>>>> can't handle a full maximal power computation input, and thus >>>>>>>>>>> can't decide for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to >>>>>>>>>> express this computation?
The moment that one switches from the notion of a halt
decider to the fully coherent notion of a proof theoretic
halting prover the halting problem counter-example input
is rejected as not specifying a well-founded justification
tree, thus a semantically incoherent input.
the problem is if u run the DD()
cannot possibly grasp what I said correctly.
As a proof theoretic halt prover DD is absolutely
and positively rejected. You cannot see this until
you first totally understand all of proof theoretic
semantics.
It like like I say "to bake a cake..." and you say
that I used the hammer and screw driver incorrectly
is DD() executable or not???
As far as a proof theoretic halt prover goes
that question is the same as asking do you
need a screwdriver or a hammer to bake an
angel food cake. HHH just correctly rejects
DD as bad input. That's all there is to it in
proof theoretic semantics.
In PTS it is the inference steps themselves
that derive ALL of the semantic meaning of DD.
"is DD() a valid executable machine or not" is a true/false
question, and your response did not answer that question polcott
As far as a proof theoretic halt prover goes that
question is as relevant to HHH/DD as asking should
HHH have mustard on its pizza?
regardless of whether it's relevant, ur not answering the question:
The question proves that your understanding is
incorrect. Being incorrectly understood is the
opposite of my goal.
"is DD() a valid executable machine or not?" is a true/false question,
what is the answer polcott???
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic Semantics as it
*Become a PTS expert before you dare say these things*
On 4/11/26 9:39 AM, Richard Damon wrote:
On 4/10/26 6:47 PM, dart200 wrote:
On 4/10/26 7:14 AM, Richard Damon wrote:
On 4/8/26 4:09 PM, dart200 wrote:
On 4/8/26 11:33 AM, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
yeah i ran into the same problem,
simulating the recursion with an action after the detection feeds
back into making the detection invalid...
it's a rather weird measurement paradox, like the measurement of
the fact of infinite recursion gets invalidate by actions taken
after the measurement itself happened
how do we frame this as a certain contradiction?
rick tried to dismiss it with the claim the simulating the machine
with an external detector isn't the same as just running the
machine...
Your problem is that with "machines" you can't make a decider that
can't be incorporated into a valid input.
There is a fundamental limitation of computation once this
"recursion" becomes possible.
Even with Oracle machines, as a level-N Oracle machine would need to
be able to be given a level-H Oracle input, which we can show it
can't handle.
A level-N Oracle machine can only handle inputs based on at most
level-N-1 Oracle machines.
By this, A Maximal Power Computation (the Level-0 Oracle) can't
handle a full maximal power computation input, and thus can't decide
for *ALL* machine inputs.
how do u know this isn't a fault of the theory in failing to express
this computation?
Because it has been logically proven.
Unless you want to presume that logic is inherently flawed, as we can
not trust any proof, the assumption of things proven impossible just
isn't allowed.
Your world seems to be based on the assumption that magical unicorns
exist that can allow you to do what has been proven to be impossible,
and thus you live in a fantasy world.
for any given partial halting recognizer one can demonstrate an machine
that with semantics that ought to result in a true return, but that the recognizer cannot answer truthfully true to...
but for every one of those machines we've proven what the machine does,
and that the partial halting recognizer must response false because it cannot answer truthfully true...
which is fine as such a response within it's specification, but the
failure to answer truthful true is _not_ because the machine's semantics
is fundamentally undecidable, it's only "undecidable" from the
perspective of that specific partial recognizer...
the question i'm left with is what algo did we use to compute that if
it's truly uncomputable?
you might say we did an analysis that transcends any kind of single
algo, but i kinda doubt that???
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding of what
you are proposing, as my intuition dictates ... which is really the only
way i know how to learn things like this. i'm sorry.
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding of what
you are proposing, as my intuition dictates ... which is really the
only way i know how to learn things like this. i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding of what
you are proposing, as my intuition dictates ... which is really the
only way i know how to learn things like this. i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding of what
you are proposing, as my intuition dictates ... which is really the
only way i know how to learn things like this. i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
is DD() a valid executable machine?
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding of
what you are proposing, as my intuition dictates ... which is really
the only way i know how to learn things like this. i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
is DD() a valid executable machine?
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding of
what you are proposing, as my intuition dictates ... which is really
the only way i know how to learn things like this. i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
is DD() a valid executable machine?
On 4/12/26 3:20 PM, olcott wrote:
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding of
what you are proposing, as my intuition dictates ... which is
really the only way i know how to learn things like this. i'm sorry. >>>>>
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
what am i incorrect about???
all i did was ask a question:
is DD() a valid executable machine?
On 4/12/2026 5:35 PM, dart200 wrote:
On 4/12/26 3:20 PM, olcott wrote:
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding of
what you are proposing, as my intuition dictates ... which is
really the only way i know how to learn things like this. i'm sorry. >>>>>>
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
what am i incorrect about???
Unless you becomes an expert at proof theoretic semantics
you cannot possibly ever know. Until then it is like
trying to explain modern virology to someone convinced
that disease is caused by evil spirits and have made up
their mind on this and closed it.
all i did was ask a question:
is DD() a valid executable machine?
On 4/12/26 6:13 PM, olcott wrote:
On 4/12/2026 5:35 PM, dart200 wrote:
On 4/12/26 3:20 PM, olcott wrote:
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding of >>>>>>> what you are proposing, as my intuition dictates ... which is
really the only way i know how to learn things like this. i'm sorry. >>>>>>>
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
what am i incorrect about???
Unless you becomes an expert at proof theoretic semantics
you cannot possibly ever know. Until then it is like
trying to explain modern virology to someone convinced
that disease is caused by evil spirits and have made up
their mind on this and closed it.
i'm sorry asking whether DD is a valid executable machine is akin to ascribing disease to spirits???
bro it's a true/false question in regards to the objective nature of DD.
either it is a valid executable machine or it's not a valid executable machine ... regardless of whether it's valid input to HHH or not ...
are you going to answer the question???
all i did was ask a question:
is DD() a valid executable machine?
On 4/12/2026 10:19 PM, dart200 wrote:
On 4/12/26 6:13 PM, olcott wrote:
On 4/12/2026 5:35 PM, dart200 wrote:
On 4/12/26 3:20 PM, olcott wrote:
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding of >>>>>>>> what you are proposing, as my intuition dictates ... which is >>>>>>>> really the only way i know how to learn things like this. i'm >>>>>>>> sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
what am i incorrect about???
Unless you becomes an expert at proof theoretic semantics
you cannot possibly ever know. Until then it is like
trying to explain modern virology to someone convinced
that disease is caused by evil spirits and have made up
their mind on this and closed it.
i'm sorry asking whether DD is a valid executable machine is akin to
ascribing disease to spirits???
bro it's a true/false question in regards to the objective nature of DD.
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
It is like I ask you to read the exact words
that text says and you take that to mean to say
what you want the words to mean that has nothing
to do with exactly what they actually say.
either it is a valid executable machine or it's not a valid executable
machine ... regardless of whether it's valid input to HHH or not ...
are you going to answer the question???
all i did was ask a question:
is DD() a valid executable machine?
On 4/12/26 9:12 PM, olcott wrote:That is why you must become an expert in proof theoretic
On 4/12/2026 10:19 PM, dart200 wrote:
On 4/12/26 6:13 PM, olcott wrote:*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
On 4/12/2026 5:35 PM, dart200 wrote:
On 4/12/26 3:20 PM, olcott wrote:
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding >>>>>>>>> of what you are proposing, as my intuition dictates ... which >>>>>>>>> is really the only way i know how to learn things like this. >>>>>>>>> i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
what am i incorrect about???
Unless you becomes an expert at proof theoretic semantics
you cannot possibly ever know. Until then it is like
trying to explain modern virology to someone convinced
that disease is caused by evil spirits and have made up
their mind on this and closed it.
i'm sorry asking whether DD is a valid executable machine is akin to
ascribing disease to spirits???
bro it's a true/false question in regards to the objective nature of DD. >>
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
It is like I ask you to read the exact words
that text says and you take that to mean to say
what you want the words to mean that has nothing
to do with exactly what they actually say.
regurgitating words isn't the same thing as understanding polcott.
On 4/12/2026 11:50 PM, dart200 wrote:
On 4/12/26 9:12 PM, olcott wrote:That is why you must become an expert in proof theoretic
On 4/12/2026 10:19 PM, dart200 wrote:
On 4/12/26 6:13 PM, olcott wrote:
On 4/12/2026 5:35 PM, dart200 wrote:
On 4/12/26 3:20 PM, olcott wrote:
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding >>>>>>>>>> of what you are proposing, as my intuition dictates ... which >>>>>>>>>> is really the only way i know how to learn things like this. >>>>>>>>>> i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
what am i incorrect about???
Unless you becomes an expert at proof theoretic semantics
you cannot possibly ever know. Until then it is like
trying to explain modern virology to someone convinced
that disease is caused by evil spirits and have made up
their mind on this and closed it.
i'm sorry asking whether DD is a valid executable machine is akin to
ascribing disease to spirits???
bro it's a true/false question in regards to the objective nature of
DD.
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
It is like I ask you to read the exact words
that text says and you take that to mean to say
what you want the words to mean that has nothing
to do with exactly what they actually say.
regurgitating words isn't the same thing as understanding polcott.
semantics before you will understand me. Changing the
subject REALLY WILL NOT HELP !!!
On 4/12/26 10:21 PM, olcott wrote:
On 4/12/2026 11:50 PM, dart200 wrote:
On 4/12/26 9:12 PM, olcott wrote:That is why you must become an expert in proof theoretic
On 4/12/2026 10:19 PM, dart200 wrote:
On 4/12/26 6:13 PM, olcott wrote:
On 4/12/2026 5:35 PM, dart200 wrote:
On 4/12/26 3:20 PM, olcott wrote:
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my understanding >>>>>>>>>>> of what you are proposing, as my intuition dictates ... which >>>>>>>>>>> is really the only way i know how to learn things like this. >>>>>>>>>>> i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
what am i incorrect about???
Unless you becomes an expert at proof theoretic semantics
you cannot possibly ever know. Until then it is like
trying to explain modern virology to someone convinced
that disease is caused by evil spirits and have made up
their mind on this and closed it.
i'm sorry asking whether DD is a valid executable machine is akin
to ascribing disease to spirits???
bro it's a true/false question in regards to the objective nature
of DD.
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
It is like I ask you to read the exact words
that text says and you take that to mean to say
what you want the words to mean that has nothing
to do with exactly what they actually say.
regurgitating words isn't the same thing as understanding polcott.
semantics before you will understand me. Changing the
subject REALLY WILL NOT HELP !!!
how is asking about the executable nature of DD changing the subject?
On 4/13/2026 1:00 AM, dart200 wrote:
On 4/12/26 10:21 PM, olcott wrote:
On 4/12/2026 11:50 PM, dart200 wrote:
On 4/12/26 9:12 PM, olcott wrote:That is why you must become an expert in proof theoretic
On 4/12/2026 10:19 PM, dart200 wrote:
On 4/12/26 6:13 PM, olcott wrote:
On 4/12/2026 5:35 PM, dart200 wrote:
On 4/12/26 3:20 PM, olcott wrote:
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my
understanding of what you are proposing, as my intuition >>>>>>>>>>>> dictates ... which is really the only way i know how to >>>>>>>>>>>> learn things like this. i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
what am i incorrect about???
Unless you becomes an expert at proof theoretic semantics
you cannot possibly ever know. Until then it is like
trying to explain modern virology to someone convinced
that disease is caused by evil spirits and have made up
their mind on this and closed it.
i'm sorry asking whether DD is a valid executable machine is akin >>>>>> to ascribing disease to spirits???
bro it's a true/false question in regards to the objective nature >>>>>> of DD.
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
It is like I ask you to read the exact words
that text says and you take that to mean to say
what you want the words to mean that has nothing
to do with exactly what they actually say.
regurgitating words isn't the same thing as understanding polcott.
semantics before you will understand me. Changing the
subject REALLY WILL NOT HELP !!!
how is asking about the executable nature of DD changing the subject?
A proof theoretic ANYTHING prover does not give a
rat's ass about anything else in the universe besides
its own sequence of inference steps.
On 12/04/2026 16:27, olcott wrote:
On 4/12/2026 4:38 AM, Mikko wrote:
On 11/04/2026 17:03, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:*Become a PTS expert before you dare say these things*
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic Semantics as it >>>>
You needn't to know anything about PTS in order to know everythihg that
can be known about the halting problem.
You must become a PTS expert to know anything about
a proof theoretic halt prover.
Not quite. There is one thing I can know anyway: it does not solve
the halting problem.
I havn't seen any proof that PTS is interesting.
On 4/13/2026 2:09 AM, Mikko wrote:
On 12/04/2026 16:27, olcott wrote:
On 4/12/2026 4:38 AM, Mikko wrote:
On 11/04/2026 17:03, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic Semantics
as it
*Become a PTS expert before you dare say these things*
You needn't to know anything about PTS in order to know everythihg that >>>> can be known about the halting problem.
You must become a PTS expert to know anything about
a proof theoretic halt prover.
Not quite. There is one thing I can know anyway: it does not solve
the halting problem.
Tarski Undefinability, Gödel 1931 Incompleteness and
the Halting problem proof have never been anything
more than undiscovered semantic incoherence.
When we replace the analytical foundation of Logic,
Math and computation with proof theoretic semantics
then we see that Tarski, Gödel, and the HP proof have
always only been anchored in an incoherent foundation.
undecidability has always never been more
that incoherent inputs.
I havn't seen any proof that PTS is interesting.
On 4/13/2026 1:00 AM, dart200 wrote:
On 4/12/26 10:21 PM, olcott wrote:
On 4/12/2026 11:50 PM, dart200 wrote:
On 4/12/26 9:12 PM, olcott wrote:That is why you must become an expert in proof theoretic
On 4/12/2026 10:19 PM, dart200 wrote:
On 4/12/26 6:13 PM, olcott wrote:
On 4/12/2026 5:35 PM, dart200 wrote:
On 4/12/26 3:20 PM, olcott wrote:
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my
understanding of what you are proposing, as my intuition >>>>>>>>>>>> dictates ... which is really the only way i know how to >>>>>>>>>>>> learn things like this. i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
what am i incorrect about???
Unless you becomes an expert at proof theoretic semantics
you cannot possibly ever know. Until then it is like
trying to explain modern virology to someone convinced
that disease is caused by evil spirits and have made up
their mind on this and closed it.
i'm sorry asking whether DD is a valid executable machine is akin >>>>>> to ascribing disease to spirits???
bro it's a true/false question in regards to the objective nature >>>>>> of DD.
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
It is like I ask you to read the exact words
that text says and you take that to mean to say
what you want the words to mean that has nothing
to do with exactly what they actually say.
regurgitating words isn't the same thing as understanding polcott.
semantics before you will understand me. Changing the
subject REALLY WILL NOT HELP !!!
how is asking about the executable nature of DD changing the subject?
A proof theoretic ANYTHING prover does not give a
rat's ass about anything else in the universe besides
its own sequence of inference steps.
On 4/13/2026 2:09 AM, Mikko wrote:
On 12/04/2026 16:27, olcott wrote:
On 4/12/2026 4:38 AM, Mikko wrote:
On 11/04/2026 17:03, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic Semantics
as it
*Become a PTS expert before you dare say these things*
You needn't to know anything about PTS in order to know everythihg that >>>> can be known about the halting problem.
You must become a PTS expert to know anything about
a proof theoretic halt prover.
Not quite. There is one thing I can know anyway: it does not solve
the halting problem.
Tarski Undefinability, Gödel 1931 Incompleteness and
the Halting problem proof have never been anything
more than undiscovered semantic incoherence.
On 4/13/26 2:27 AM, olcott wrote:
On 4/13/2026 1:00 AM, dart200 wrote:
On 4/12/26 10:21 PM, olcott wrote:
On 4/12/2026 11:50 PM, dart200 wrote:
On 4/12/26 9:12 PM, olcott wrote:That is why you must become an expert in proof theoretic
On 4/12/2026 10:19 PM, dart200 wrote:
On 4/12/26 6:13 PM, olcott wrote:
On 4/12/2026 5:35 PM, dart200 wrote:
On 4/12/26 3:20 PM, olcott wrote:
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my
understanding of what you are proposing, as my intuition >>>>>>>>>>>>> dictates ... which is really the only way i know how to >>>>>>>>>>>>> learn things like this. i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded
justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
what am i incorrect about???
Unless you becomes an expert at proof theoretic semantics
you cannot possibly ever know. Until then it is like
trying to explain modern virology to someone convinced
that disease is caused by evil spirits and have made up
their mind on this and closed it.
i'm sorry asking whether DD is a valid executable machine is akin >>>>>>> to ascribing disease to spirits???
bro it's a true/false question in regards to the objective nature >>>>>>> of DD.
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
It is like I ask you to read the exact words
that text says and you take that to mean to say
what you want the words to mean that has nothing
to do with exactly what they actually say.
regurgitating words isn't the same thing as understanding polcott.
semantics before you will understand me. Changing the
subject REALLY WILL NOT HELP !!!
how is asking about the executable nature of DD changing the subject?
A proof theoretic ANYTHING prover does not give a
rat's ass about anything else in the universe besides
its own sequence of inference steps.
look i'll so beating around the bush:
DD is a valid executable machine. when run DD halts, and that is fact.
do u not agree???
when ur proof theoretic whatever prover analyzes DD it concludes the
input is invalid, and that is always a fact. i can agree with this.
this facts aren't incongruent with each other, both facts can be true.
DD can be a halting machine that is also invalid input in regards to
your proof theoretic whatever prover.
do u not agree???
On 13/04/2026 18:01, olcott wrote:
On 4/13/2026 2:09 AM, Mikko wrote:
On 12/04/2026 16:27, olcott wrote:
On 4/12/2026 4:38 AM, Mikko wrote:
On 11/04/2026 17:03, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification
tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic Semantics >>>>>>> as it
*Become a PTS expert before you dare say these things*
You needn't to know anything about PTS in order to know everythihg
that
can be known about the halting problem.
You must become a PTS expert to know anything about
a proof theoretic halt prover.
Not quite. There is one thing I can know anyway: it does not solve
the halting problem.
Tarski Undefinability, Gödel 1931 Incompleteness and
the Halting problem proof have never been anything
more than undiscovered semantic incoherence.
Everything derived from axioms and postulates with truth preserving inferences is true in every interpretation where the axioms are true.
Both Tarski's and Gödel's theorems are rooted in the axioms of logic
and arithmetic so they are true whenever the axioms or logic and
arithmetic are.
On 4/14/2026 12:14 AM, dart200 wrote:
On 4/13/26 2:27 AM, olcott wrote:
On 4/13/2026 1:00 AM, dart200 wrote:
On 4/12/26 10:21 PM, olcott wrote:
On 4/12/2026 11:50 PM, dart200 wrote:
On 4/12/26 9:12 PM, olcott wrote:That is why you must become an expert in proof theoretic
On 4/12/2026 10:19 PM, dart200 wrote:
On 4/12/26 6:13 PM, olcott wrote:
On 4/12/2026 5:35 PM, dart200 wrote:
On 4/12/26 3:20 PM, olcott wrote:
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my
understanding of what you are proposing, as my intuition >>>>>>>>>>>>>> dictates ... which is really the only way i know how to >>>>>>>>>>>>>> learn things like this. i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded >>>>>>>>>>>>> justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
what am i incorrect about???
Unless you becomes an expert at proof theoretic semantics
you cannot possibly ever know. Until then it is like
trying to explain modern virology to someone convinced
that disease is caused by evil spirits and have made up
their mind on this and closed it.
i'm sorry asking whether DD is a valid executable machine is
akin to ascribing disease to spirits???
bro it's a true/false question in regards to the objective
nature of DD.
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
It is like I ask you to read the exact words
that text says and you take that to mean to say
what you want the words to mean that has nothing
to do with exactly what they actually say.
regurgitating words isn't the same thing as understanding polcott.
semantics before you will understand me. Changing the
subject REALLY WILL NOT HELP !!!
how is asking about the executable nature of DD changing the subject?
A proof theoretic ANYTHING prover does not give a
rat's ass about anything else in the universe besides
its own sequence of inference steps.
look i'll so beating around the bush:
DD is a valid executable machine. when run DD halts, and that is fact.
do u not agree???
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/ #InfeIntuAntiReal
when ur proof theoretic whatever prover analyzes DD it concludes the
input is invalid, and that is always a fact. i can agree with this.
this facts aren't incongruent with each other, both facts can be true.
DD can be a halting machine that is also invalid input in regards to
your proof theoretic whatever prover.
do u not agree???
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
so ur saying nothing can prove this correct???
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
so ur saying nothing can prove this correct???
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
unless u disagree that DD halts???
so ur saying nothing can prove this correct???
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
unless u disagree that DD halts???
so ur saying nothing can prove this correct???
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/ >>>>>>>> #InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the total
possible ways a machine can be constructed,
specifically because the possibility for machines referencing themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind of
circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/ >>>>>>>>> #InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the total
possible ways a machine can be constructed,
specifically because the possibility for machines referencing
themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind of
circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
On 4/14/2026 12:14 AM, dart200 wrote:
On 4/13/26 2:27 AM, olcott wrote:
On 4/13/2026 1:00 AM, dart200 wrote:
On 4/12/26 10:21 PM, olcott wrote:
On 4/12/2026 11:50 PM, dart200 wrote:
On 4/12/26 9:12 PM, olcott wrote:That is why you must become an expert in proof theoretic
On 4/12/2026 10:19 PM, dart200 wrote:
On 4/12/26 6:13 PM, olcott wrote:
On 4/12/2026 5:35 PM, dart200 wrote:
On 4/12/26 3:20 PM, olcott wrote:
On 4/12/2026 2:01 PM, dart200 wrote:
On 4/12/26 6:14 AM, olcott wrote:
On 4/12/2026 3:46 AM, dart200 wrote:
ofc my understanding is likely incorrect,
i'm literally asking the question to further my
understanding of what you are proposing, as my intuition >>>>>>>>>>>>>> dictates ... which is really the only way i know how to >>>>>>>>>>>>>> learn things like this. i'm sorry.
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);
}
When DD is simulated by proof theoretic halt prover
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
Then HHH simulates that call HHH(DD)
that rejects DD as semantically incoherent
because this inference steps never reach
DD.return Halt_Status;
HHH the recursive simulation that HHH detects
allows DD to be rejected as not having a well-founded >>>>>>>>>>>>> justification tree within PTS.
it's still not answering my question...
Your question proves that you are stupidly incorrect.
what am i incorrect about???
Unless you becomes an expert at proof theoretic semantics
you cannot possibly ever know. Until then it is like
trying to explain modern virology to someone convinced
that disease is caused by evil spirits and have made up
their mind on this and closed it.
i'm sorry asking whether DD is a valid executable machine is
akin to ascribing disease to spirits???
bro it's a true/false question in regards to the objective
nature of DD.
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
*THAT IS NOT HOW PROOF THEORETIC SEMANTICS WORKS*
It is like I ask you to read the exact words
that text says and you take that to mean to say
what you want the words to mean that has nothing
to do with exactly what they actually say.
regurgitating words isn't the same thing as understanding polcott.
semantics before you will understand me. Changing the
subject REALLY WILL NOT HELP !!!
how is asking about the executable nature of DD changing the subject?
A proof theoretic ANYTHING prover does not give a
rat's ass about anything else in the universe besides
its own sequence of inference steps.
look i'll so beating around the bush:
DD is a valid executable machine. when run DD halts, and that is fact.
do u not agree???
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/ #InfeIntuAntiReal
when ur proof theoretic whatever prover analyzes DD it concludes the
input is invalid, and that is always a fact. i can agree with this.
this facts aren't incongruent with each other, both facts can be true.
DD can be a halting machine that is also invalid input in regards to
your proof theoretic whatever prover.
do u not agree???
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/ >>>>>>>>> #InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the total
possible ways a machine can be constructed,
specifically because the possibility for machines referencing
themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind of
circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
On 4/14/2026 1:04 AM, Mikko wrote:
On 13/04/2026 18:01, olcott wrote:
On 4/13/2026 2:09 AM, Mikko wrote:
On 12/04/2026 16:27, olcott wrote:
On 4/12/2026 4:38 AM, Mikko wrote:
On 11/04/2026 17:03, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>> tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic Semantics >>>>>>>> as it
*Become a PTS expert before you dare say these things*
You needn't to know anything about PTS in order to know everythihg >>>>>> that
can be known about the halting problem.
You must become a PTS expert to know anything about
a proof theoretic halt prover.
Not quite. There is one thing I can know anyway: it does not solve
the halting problem.
Tarski Undefinability, Gödel 1931 Incompleteness and
the Halting problem proof have never been anything
more than undiscovered semantic incoherence.
Everything derived from axioms and postulates with truth preserving
inferences is true in every interpretation where the axioms are true.
Gödel doesn't do that. His definition of true sneaks
off somewhere else into a meta-math model.
On 14/04/2026 16:41, olcott wrote:
On 4/14/2026 1:04 AM, Mikko wrote:
On 13/04/2026 18:01, olcott wrote:
On 4/13/2026 2:09 AM, Mikko wrote:
On 12/04/2026 16:27, olcott wrote:
On 4/12/2026 4:38 AM, Mikko wrote:
On 11/04/2026 17:03, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>>> tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic
Semantics as it
*Become a PTS expert before you dare say these things*
You needn't to know anything about PTS in order to know
everythihg that
can be known about the halting problem.
You must become a PTS expert to know anything about
a proof theoretic halt prover.
Not quite. There is one thing I can know anyway: it does not solve
the halting problem.
Tarski Undefinability, Gödel 1931 Incompleteness and
the Halting problem proof have never been anything
more than undiscovered semantic incoherence.
Everything derived from axioms and postulates with truth preserving
inferences is true in every interpretation where the axioms are true.
Gödel doesn't do that. His definition of true sneaks
off somewhere else into a meta-math model.
How is a definition of "true" relevant to Gödel's incomleteness
theorem?
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/ >>>>>>>>>> #InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the total
possible ways a machine can be constructed,
specifically because the possibility for machines referencing
themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind of
circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability problems within computing are _not_ intentionally modeled after the liar's
paradox...
turing when he stumbled on the first undecidable situation within
computing was not considering the liar's paradox or even godel's incompleteness directly. he was considering cantor's diagonal formed
across all circle-free machines. and without certain fixes, the problem arises when the diagonal machine is deciding on itself as circle-free... this was not an intention constructional, but an artifact of self- references within turing machine logic,
they just _are_ a possible construction within all permutations of
turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just declare a
machine that certainly halts as incoherent input to a halting prover (without some further explanation of how the truth of it being halting
is ascertained)
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/ >>>>>>>>>>> #InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the total
possible ways a machine can be constructed,
specifically because the possibility for machines referencing
themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind of
circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability
problems within computing are _not_ intentionally modeled after the
liar's paradox...
turing when he stumbled on the first undecidable situation within
computing was not considering the liar's paradox or even godel's
incompleteness directly. he was considering cantor's diagonal formed
across all circle-free machines. and without certain fixes, the
problem arises when the diagonal machine is deciding on itself as
circle-free... this was not an intention constructional, but an
artifact of self- references within turing machine logic,
they just _are_ a possible construction within all permutations of
turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just declare a
machine that certainly halts as incoherent input to a halting prover
(without some further explanation of how the truth of it being halting
is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-
semantics/ #InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the total >>>>> possible ways a machine can be constructed,
specifically because the possibility for machines referencing
themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind of
circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability
problems within computing are _not_ intentionally modeled after the
liar's paradox...
turing when he stumbled on the first undecidable situation within
computing was not considering the liar's paradox or even godel's
incompleteness directly. he was considering cantor's diagonal formed
across all circle-free machines. and without certain fixes, the
problem arises when the diagonal machine is deciding on itself as
circle-free... this was not an intention constructional, but an
artifact of self- references within turing machine logic,
they just _are_ a possible construction within all permutations of
turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just declare a
machine that certainly halts as incoherent input to a halting prover
(without some further explanation of how the truth of it being
halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a valid machine
that halts when executed,
why do u think u need to insult me back when i point that out?
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish >>>>>>>>>>>>> the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic- >>>>>>>>>>>>> semantics/ #InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the
total possible ways a machine can be constructed,
specifically because the possibility for machines referencing
themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind of >>>>>> circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability
problems within computing are _not_ intentionally modeled after the
liar's paradox...
turing when he stumbled on the first undecidable situation within
computing was not considering the liar's paradox or even godel's
incompleteness directly. he was considering cantor's diagonal formed
across all circle-free machines. and without certain fixes, the
problem arises when the diagonal machine is deciding on itself as
circle-free... this was not an intention constructional, but an
artifact of self- references within turing machine logic,
they just _are_ a possible construction within all permutations of
turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just declare a
machine that certainly halts as incoherent input to a halting prover
(without some further explanation of how the truth of it being
halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a valid machine
that halts when executed,
why do u think u need to insult me back when i point that out?
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
Just because a bunch of knuckleheads have not
construed it as a bad input provides zero
actual evidence that it was not a bad input
all along.
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>> which inferences and the rules of inference establish >>>>>>>>>>>>>> the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic- >>>>>>>>>>>>>> semantics/ #InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the
total possible ways a machine can be constructed,
specifically because the possibility for machines referencing
themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind >>>>>>> of circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability
problems within computing are _not_ intentionally modeled after the >>>>> liar's paradox...
turing when he stumbled on the first undecidable situation within
computing was not considering the liar's paradox or even godel's
incompleteness directly. he was considering cantor's diagonal
formed across all circle-free machines. and without certain fixes,
the problem arises when the diagonal machine is deciding on itself
as circle-free... this was not an intention constructional, but an
artifact of self- references within turing machine logic,
they just _are_ a possible construction within all permutations of
turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just declare a
machine that certainly halts as incoherent input to a halting
prover (without some further explanation of how the truth of it
being halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a valid
machine that halts when executed,
why do u think u need to insult me back when i point that out?
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could correctly
decide on it...
Just because a bunch of knuckleheads have not
construed it as a bad input provides zero
actual evidence that it was not a bad input
all along.
right, but DD still halts, and the prover failed to prove that
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>> which inferences and the rules of inference establish >>>>>>>>>>>>>> the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic- >>>>>>>>>>>>>> semantics/ #InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the
total possible ways a machine can be constructed,
specifically because the possibility for machines referencing
themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind >>>>>>> of circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability
problems within computing are _not_ intentionally modeled after the >>>>> liar's paradox...
turing when he stumbled on the first undecidable situation within
computing was not considering the liar's paradox or even godel's
incompleteness directly. he was considering cantor's diagonal
formed across all circle-free machines. and without certain fixes,
the problem arises when the diagonal machine is deciding on itself
as circle-free... this was not an intention constructional, but an
artifact of self- references within turing machine logic,
they just _are_ a possible construction within all permutations of
turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just declare a
machine that certainly halts as incoherent input to a halting
prover (without some further explanation of how the truth of it
being halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a valid
machine that halts when executed,
why do u think u need to insult me back when i point that out?
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could correctly
decide on it...
Just because a bunch of knuckleheads have not
construed it as a bad input provides zero
actual evidence that it was not a bad input
all along.
right, but DD still halts, and the prover failed to prove that
On 4/15/2026 2:11 AM, Mikko wrote:
On 14/04/2026 16:41, olcott wrote:
On 4/14/2026 1:04 AM, Mikko wrote:
On 13/04/2026 18:01, olcott wrote:
On 4/13/2026 2:09 AM, Mikko wrote:
On 12/04/2026 16:27, olcott wrote:
On 4/12/2026 4:38 AM, Mikko wrote:
On 11/04/2026 17:03, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>>>> tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic
Semantics as it
*Become a PTS expert before you dare say these things*
You needn't to know anything about PTS in order to know
everythihg that
can be known about the halting problem.
You must become a PTS expert to know anything about
a proof theoretic halt prover.
Not quite. There is one thing I can know anyway: it does not solve >>>>>> the halting problem.
Tarski Undefinability, Gödel 1931 Incompleteness and
the Halting problem proof have never been anything
more than undiscovered semantic incoherence.
Everything derived from axioms and postulates with truth preserving
inferences is true in every interpretation where the axioms are true.
Gödel doesn't do that. His definition of true sneaks
off somewhere else into a meta-math model.
How is a definition of "true" relevant to Gödel's incomleteness
theorem?
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F. https://plato.stanford.edu/entries/goedel-incompleteness/
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent.
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs. It thus belongs to inferentialism (a term
coined by Brandom, see his 1994; 2000) according to
which inferences and the rules of inference establish
the meaning of expressions Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/ >>>>>>>>>>> #InfeIntuAntiReal
so you do agree DD halts when executed??? or not???
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the total
possible ways a machine can be constructed,
specifically because the possibility for machines referencing
themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind of
circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability
problems within computing are _not_ intentionally modeled after the
liar's paradox...
turing when he stumbled on the first undecidable situation within
computing was not considering the liar's paradox or even godel's
incompleteness directly. he was considering cantor's diagonal formed
across all circle-free machines. and without certain fixes, the
problem arises when the diagonal machine is deciding on itself as
circle-free... this was not an intention constructional, but an
artifact of self- references within turing machine logic,
they just _are_ a possible construction within all permutations of
turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just declare a
machine that certainly halts as incoherent input to a halting prover
(without some further explanation of how the truth of it being halting
is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
On 4/15/2026 2:11 AM, Mikko wrote:
On 14/04/2026 16:41, olcott wrote:
On 4/14/2026 1:04 AM, Mikko wrote:
On 13/04/2026 18:01, olcott wrote:
On 4/13/2026 2:09 AM, Mikko wrote:
On 12/04/2026 16:27, olcott wrote:
On 4/12/2026 4:38 AM, Mikko wrote:
On 11/04/2026 17:03, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>>>> tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic
Semantics as it
*Become a PTS expert before you dare say these things*
You needn't to know anything about PTS in order to know
everythihg that
can be known about the halting problem.
You must become a PTS expert to know anything about
a proof theoretic halt prover.
Not quite. There is one thing I can know anyway: it does not solve >>>>>> the halting problem.
Tarski Undefinability, Gödel 1931 Incompleteness and
the Halting problem proof have never been anything
more than undiscovered semantic incoherence.
Everything derived from axioms and postulates with truth preserving
inferences is true in every interpretation where the axioms are true.
Gödel doesn't do that. His definition of true sneaks
off somewhere else into a meta-math model.
How is a definition of "true" relevant to Gödel's incomleteness
theorem?
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F. https://plato.stanford.edu/entries/goedel-incompleteness/
Olcott's Minimal Type Theory
G ↔ ¬Prov[PA](⌜G⌝)
https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov[PA] 04
04 Gödel_Number_of 01 // cycle
Proof Theoretic Semantics prover rejects the above
expression because it has a cycle in the directed
graph of its evaluation sequence.
On 4/15/2026 2:11 AM, Mikko wrote:
On 14/04/2026 16:41, olcott wrote:
On 4/14/2026 1:04 AM, Mikko wrote:
On 13/04/2026 18:01, olcott wrote:
On 4/13/2026 2:09 AM, Mikko wrote:
On 12/04/2026 16:27, olcott wrote:
On 4/12/2026 4:38 AM, Mikko wrote:
On 11/04/2026 17:03, olcott wrote:
On 4/11/2026 2:42 AM, Mikko wrote:
On 08/04/2026 21:33, olcott wrote:
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);
}
When DD is simulated by proof theoretic halt prover
HHH the recursive simulation that HHH detects allows
DD to be rejected as not having a well-founded justification >>>>>>>>>>> tree. The only inputs left out are semantically unsound.
The meaning of "halt" is the same with Proof Theoretic
Semantics as it
*Become a PTS expert before you dare say these things*
You needn't to know anything about PTS in order to know
everythihg that
can be known about the halting problem.
You must become a PTS expert to know anything about
a proof theoretic halt prover.
Not quite. There is one thing I can know anyway: it does not solve >>>>>> the halting problem.
Tarski Undefinability, Gödel 1931 Incompleteness and
the Halting problem proof have never been anything
more than undiscovered semantic incoherence.
Everything derived from axioms and postulates with truth preserving
inferences is true in every interpretation where the axioms are true.
Gödel doesn't do that. His definition of true sneaks
off somewhere else into a meta-math model.
How is a definition of "true" relevant to Gödel's incomleteness
theorem?
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F. https://plato.stanford.edu/entries/goedel-incompleteness/
Olcott's Minimal Type Theory
G ↔ ¬Prov[PA](⌜G⌝) https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov[PA] 04
04 Gödel_Number_of 01 // cycle
Proof Theoretic Semantics prover rejects the above
expression because it has a cycle in the directed
graph of its evaluation sequence.
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its definition
is irrelevant to the first incompletness theorem.
On 4/15/2026 8:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>>> which inferences and the rules of inference establish >>>>>>>>>>>>>>> the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic- >>>>>>>>>>>>>>> semantics/ #InfeIntuAntiReal
so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the >>>>>>>> total possible ways a machine can be constructed,
specifically because the possibility for machines referencing >>>>>>>> themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind >>>>>>>> of circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability
problems within computing are _not_ intentionally modeled after
the liar's paradox...
turing when he stumbled on the first undecidable situation within >>>>>> computing was not considering the liar's paradox or even godel's
incompleteness directly. he was considering cantor's diagonal
formed across all circle-free machines. and without certain fixes, >>>>>> the problem arises when the diagonal machine is deciding on itself >>>>>> as circle-free... this was not an intention constructional, but an >>>>>> artifact of self- references within turing machine logic,
they just _are_ a possible construction within all permutations of >>>>>> turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just declare a >>>>>> machine that certainly halts as incoherent input to a halting
prover (without some further explanation of how the truth of it
being halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a valid
machine that halts when executed,
why do u think u need to insult me back when i point that out?
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could correctly
decide on it...
Just because a bunch of knuckleheads have not
construed it as a bad input provides zero
actual evidence that it was not a bad input
all along.
right, but DD still halts, and the prover failed to prove that
This makes me ponder on my fuzzer. You know...
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input
that does the opposite of whatever value a halt
decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already
has the complete and perfect foundational basis
to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>>> which inferences and the rules of inference establish >>>>>>>>>>>>>>> the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic- >>>>>>>>>>>>>>> semantics/ #InfeIntuAntiReal
so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject
an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the >>>>>>>> total possible ways a machine can be constructed,
specifically because the possibility for machines referencing >>>>>>>> themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind >>>>>>>> of circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability
problems within computing are _not_ intentionally modeled after
the liar's paradox...
turing when he stumbled on the first undecidable situation within >>>>>> computing was not considering the liar's paradox or even godel's
incompleteness directly. he was considering cantor's diagonal
formed across all circle-free machines. and without certain fixes, >>>>>> the problem arises when the diagonal machine is deciding on itself >>>>>> as circle-free... this was not an intention constructional, but an >>>>>> artifact of self- references within turing machine logic,
they just _are_ a possible construction within all permutations of >>>>>> turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just declare a >>>>>> machine that certainly halts as incoherent input to a halting
prover (without some further explanation of how the truth of it
being halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a valid
machine that halts when executed,
why do u think u need to insult me back when i point that out?
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could correctly
decide on it...
Can Carol correctly answer “no” to this (yes/no) question?
E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
Just because a bunch of knuckleheads have not
construed it as a bad input provides zero
actual evidence that it was not a bad input
all along.
right, but DD still halts, and the prover failed to prove that
DD simulated by HHH conclusively proves that it
cannot possibly stop running unless HHH aborts it.
Author of #1 best seller for theory of computation texts
<MIT Professor Sipser agreed to ONLY these verbatim words 10/13/2022>
If simulating halt decider H correctly simulates its
input D until H correctly determines that its simulated D
would never stop running unless aborted then
H can abort its simulation of D and correctly report that D
specifies a non-halting sequence of configurations.
</MIT Professor Sipser agreed to ONLY these verbatim words 10/13/2022>
On 4/15/26 8:51 PM, olcott wrote:
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input >>>>>>>>>>>>>>>> that does the opposite of whatever value a halt >>>>>>>>>>>>>>>> decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already >>>>>>>>>>>>>>>> has the complete and perfect foundational basis >>>>>>>>>>>>>>>> to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism >>>>>>>>>>>>>>>> Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>>>> which inferences and the rules of inference establish >>>>>>>>>>>>>>>> the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic- >>>>>>>>>>>>>>>> semantics/ #InfeIntuAntiReal
so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>>
At this point that question becomes pure trolling
with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject >>>>>>>>>>>>>> an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts???
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the >>>>>>>>> total possible ways a machine can be constructed,
specifically because the possibility for machines referencing >>>>>>>>> themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this kind >>>>>>>>> of circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability
problems within computing are _not_ intentionally modeled after >>>>>>> the liar's paradox...
turing when he stumbled on the first undecidable situation within >>>>>>> computing was not considering the liar's paradox or even godel's >>>>>>> incompleteness directly. he was considering cantor's diagonal
formed across all circle-free machines. and without certain
fixes, the problem arises when the diagonal machine is deciding >>>>>>> on itself as circle-free... this was not an intention
constructional, but an artifact of self- references within turing >>>>>>> machine logic,
they just _are_ a possible construction within all permutations >>>>>>> of turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just declare a >>>>>>> machine that certainly halts as incoherent input to a halting
prover (without some further explanation of how the truth of it >>>>>>> being halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a valid
machine that halts when executed,
why do u think u need to insult me back when i point that out?
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could correctly
decide on it...
Can Carol correctly answer “no” to this (yes/no) question?
E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
yes i know that, truth can be defined relative to a reference point.
same is true in physical too,
but u keep repeating on and on about bad input instead of explaining
both perspectives at the same time
Just because a bunch of knuckleheads have not
construed it as a bad input provides zero
actual evidence that it was not a bad input
all along.
right, but DD still halts, and the prover failed to prove that
DD simulated by HHH conclusively proves that it
cannot possibly stop running unless HHH aborts it.
that's the outcome of DD yes, idk why ur repeating it ...
Author of #1 best seller for theory of computation texts
<MIT Professor Sipser agreed to ONLY these verbatim words 10/13/2022>
If simulating halt decider H correctly simulates its
input D until H correctly determines that its simulated D
would never stop running unless aborted then
H can abort its simulation of D and correctly report that D
specifies a non-halting sequence of configurations.
</MIT Professor Sipser agreed to ONLY these verbatim words 10/13/2022>
On 4/16/2026 12:41 PM, dart200 wrote:
On 4/15/26 8:51 PM, olcott wrote:
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input >>>>>>>>>>>>>>>>> that does the opposite of whatever value a halt >>>>>>>>>>>>>>>>> decider returns is a valid input. Ordinary
unadulterated proof theoretic semantics already >>>>>>>>>>>>>>>>> has the complete and perfect foundational basis >>>>>>>>>>>>>>>>> to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism >>>>>>>>>>>>>>>>> Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>>>>> which inferences and the rules of inference establish >>>>>>>>>>>>>>>>> the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic- >>>>>>>>>>>>>>>>> semantics/ #InfeIntuAntiReal
so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>>>
At this point that question becomes pure trolling >>>>>>>>>>>>>>> with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject >>>>>>>>>>>>>>> an input that does the opposite of whatever its
decider reports.
Proof theoretic semantics provides the complete
foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts??? >>>>>>>>>>>>
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the >>>>>>>>>> total possible ways a machine can be constructed,
specifically because the possibility for machines referencing >>>>>>>>>> themselves (proven by kleene's second recursion theorem):
because machines can self-reference their own result, this >>>>>>>>>> kind of circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability >>>>>>>> problems within computing are _not_ intentionally modeled after >>>>>>>> the liar's paradox...
turing when he stumbled on the first undecidable situation
within computing was not considering the liar's paradox or even >>>>>>>> godel's incompleteness directly. he was considering cantor's
diagonal formed across all circle-free machines. and without
certain fixes, the problem arises when the diagonal machine is >>>>>>>> deciding on itself as circle-free... this was not an intention >>>>>>>> constructional, but an artifact of self- references within
turing machine logic,
they just _are_ a possible construction within all permutations >>>>>>>> of turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just declare >>>>>>>> a machine that certainly halts as incoherent input to a halting >>>>>>>> prover (without some further explanation of how the truth of it >>>>>>>> being halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a valid
machine that halts when executed,
why do u think u need to insult me back when i point that out?
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could correctly
decide on it...
Can Carol correctly answer “no” to this (yes/no) question?
E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
yes i know that, truth can be defined relative to a reference point.
same is true in physical too,
but u keep repeating on and on about bad input instead of explaining
both perspectives at the same time
I don't allocate equal weight to falsehoods.
The HP counter-example input has always been
bad and the only reason this is not universally
understood is that sheeple herd together in
the conventional views.
On 4/16/26 11:20 AM, olcott wrote:
On 4/16/2026 12:41 PM, dart200 wrote:
On 4/15/26 8:51 PM, olcott wrote:
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input >>>>>>>>>>>>>>>>>> that does the opposite of whatever value a halt >>>>>>>>>>>>>>>>>> decider returns is a valid input. Ordinary >>>>>>>>>>>>>>>>>> unadulterated proof theoretic semantics already >>>>>>>>>>>>>>>>>> has the complete and perfect foundational basis >>>>>>>>>>>>>>>>>> to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism >>>>>>>>>>>>>>>>>> Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>>>>>> which inferences and the rules of inference establish >>>>>>>>>>>>>>>>>> the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic- >>>>>>>>>>>>>>>>>> semantics/ #InfeIntuAntiReal
so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>>>>
At this point that question becomes pure trolling >>>>>>>>>>>>>>>> with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject >>>>>>>>>>>>>>>> an input that does the opposite of whatever its >>>>>>>>>>>>>>>> decider reports.
Proof theoretic semantics provides the complete >>>>>>>>>>>>>>>> foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts??? >>>>>>>>>>>>>
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of the >>>>>>>>>>> total possible ways a machine can be constructed,
specifically because the possibility for machines referencing >>>>>>>>>>> themselves (proven by kleene's second recursion theorem): >>>>>>>>>>>
because machines can self-reference their own result, this >>>>>>>>>>> kind of circular analytical paradox _is_ possible
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent.
except DD _is_ a valid machine, that _does_ halt, no???
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability >>>>>>>>> problems within computing are _not_ intentionally modeled after >>>>>>>>> the liar's paradox...
turing when he stumbled on the first undecidable situation
within computing was not considering the liar's paradox or even >>>>>>>>> godel's incompleteness directly. he was considering cantor's >>>>>>>>> diagonal formed across all circle-free machines. and without >>>>>>>>> certain fixes, the problem arises when the diagonal machine is >>>>>>>>> deciding on itself as circle-free... this was not an intention >>>>>>>>> constructional, but an artifact of self- references within
turing machine logic,
they just _are_ a possible construction within all permutations >>>>>>>>> of turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just declare >>>>>>>>> a machine that certainly halts as incoherent input to a halting >>>>>>>>> prover (without some further explanation of how the truth of it >>>>>>>>> being halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a valid
machine that halts when executed,
why do u think u need to insult me back when i point that out?
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could
correctly decide on it...
Can Carol correctly answer “no” to this (yes/no) question?
E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
yes i know that, truth can be defined relative to a reference point.
same is true in physical too,
but u keep repeating on and on about bad input instead of explaining
both perspectives at the same time
I don't allocate equal weight to falsehoods.
The HP counter-example input has always been
bad and the only reason this is not universally
understood is that sheeple herd together in
the conventional views.
no, turing's diagonal counter-example, the _original_ problem, is not a trivial program that produces no output.
it actually performs a computation and deciding on that computation is
an issue.
On 4/16/2026 1:29 PM, dart200 wrote:
On 4/16/26 11:20 AM, olcott wrote:
On 4/16/2026 12:41 PM, dart200 wrote:
On 4/15/26 8:51 PM, olcott wrote:
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input >>>>>>>>>>>>>>>>>>> that does the opposite of whatever value a halt >>>>>>>>>>>>>>>>>>> decider returns is a valid input. Ordinary >>>>>>>>>>>>>>>>>>> unadulterated proof theoretic semantics already >>>>>>>>>>>>>>>>>>> has the complete and perfect foundational basis >>>>>>>>>>>>>>>>>>> to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism >>>>>>>>>>>>>>>>>>> Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>>>>>>> which inferences and the rules of inference establish >>>>>>>>>>>>>>>>>>> the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic- >>>>>>>>>>>>>>>>>>> semantics/ #InfeIntuAntiReal
so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>>>>>
At this point that question becomes pure trolling >>>>>>>>>>>>>>>>> with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject >>>>>>>>>>>>>>>>> an input that does the opposite of whatever its >>>>>>>>>>>>>>>>> decider reports.
Proof theoretic semantics provides the complete >>>>>>>>>>>>>>>>> foundational basis for this rejection to be
accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts??? >>>>>>>>>>>>>>
Everyone has been nuts to require a machine to
report on an input that was intentionally designed
to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of >>>>>>>>>>>> the total possible ways a machine can be constructed,
specifically because the possibility for machines
referencing themselves (proven by kleene's second recursion >>>>>>>>>>>> theorem):
because machines can self-reference their own result, this >>>>>>>>>>>> kind of circular analytical paradox _is_ possible
except DD _is_ a valid machine, that _does_ halt, no??? >>>>>>>>>>>>
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent. >>>>>>>>>>>>
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but decidability >>>>>>>>>> problems within computing are _not_ intentionally modeled >>>>>>>>>> after the liar's paradox...
turing when he stumbled on the first undecidable situation >>>>>>>>>> within computing was not considering the liar's paradox or >>>>>>>>>> even godel's incompleteness directly. he was considering
cantor's diagonal formed across all circle-free machines. and >>>>>>>>>> without certain fixes, the problem arises when the diagonal >>>>>>>>>> machine is deciding on itself as circle-free... this was not >>>>>>>>>> an intention constructional, but an artifact of self-
references within turing machine logic,
they just _are_ a possible construction within all
permutations of turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS.
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just
declare a machine that certainly halts as incoherent input to >>>>>>>>>> a halting prover (without some further explanation of how the >>>>>>>>>> truth of it being halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a valid >>>>>>>> machine that halts when executed,
why do u think u need to insult me back when i point that out? >>>>>>>>
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could
correctly decide on it...
Can Carol correctly answer “no” to this (yes/no) question?
E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
yes i know that, truth can be defined relative to a reference point.
same is true in physical too,
but u keep repeating on and on about bad input instead of explaining
both perspectives at the same time
I don't allocate equal weight to falsehoods.
The HP counter-example input has always been
bad and the only reason this is not universally
understood is that sheeple herd together in
the conventional views.
no, turing's diagonal counter-example, the _original_ problem, is not
a trivial program that produces no output.
it actually performs a computation and deciding on that computation is
an issue.
Any input that does the opposite of whatever value its
decider returns should have been rejected as bad input
is dead obvious.
I am not sure how far back PTS has generically
rejected every expression that specifies cycles
in the directed graph of inference steps it may
be as far back as 1930.
The key relevant thing is that ALL PTS experts
now universally agree that such expressions
lack any semantic meaning because all PTS
experts universally agree that ALL semantic
meaning ONLY comes from finite sequences of
inference steps.
This article was written by the guy that coined
the term "proof theoretic semantics"
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs.
It thus belongs to inferentialism (a term coined by
Brandom, see his 1994; 2000) according to which
inferences and the rules of inference establish the
meaning of expressions...
Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics" https://plato.stanford.edu/entries/proof-theoretic-semantics/ #InfeIntuAntiReal
On 4/16/26 11:52 AM, olcott wrote:
On 4/16/2026 1:29 PM, dart200 wrote:
On 4/16/26 11:20 AM, olcott wrote:
On 4/16/2026 12:41 PM, dart200 wrote:
On 4/15/26 8:51 PM, olcott wrote:
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input >>>>>>>>>>>>>>>>>>>> that does the opposite of whatever value a halt >>>>>>>>>>>>>>>>>>>> decider returns is a valid input. Ordinary >>>>>>>>>>>>>>>>>>>> unadulterated proof theoretic semantics already >>>>>>>>>>>>>>>>>>>> has the complete and perfect foundational basis >>>>>>>>>>>>>>>>>>>> to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism >>>>>>>>>>>>>>>>>>>> Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>>>>>>>> which inferences and the rules of inference establish >>>>>>>>>>>>>>>>>>>> the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic- >>>>>>>>>>>>>>>>>>>> semantics/ #InfeIntuAntiReal
so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>>>>>>
At this point that question becomes pure trolling >>>>>>>>>>>>>>>>>> with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject >>>>>>>>>>>>>>>>>> an input that does the opposite of whatever its >>>>>>>>>>>>>>>>>> decider reports.
Proof theoretic semantics provides the complete >>>>>>>>>>>>>>>>>> foundational basis for this rejection to be >>>>>>>>>>>>>>>>>> accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts??? >>>>>>>>>>>>>>>
Everyone has been nuts to require a machine to
report on an input that was intentionally designed >>>>>>>>>>>>>> to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of >>>>>>>>>>>>> the total possible ways a machine can be constructed, >>>>>>>>>>>>>
specifically because the possibility for machines
referencing themselves (proven by kleene's second recursion >>>>>>>>>>>>> theorem):
because machines can self-reference their own result, this >>>>>>>>>>>>> kind of circular analytical paradox _is_ possible
except DD _is_ a valid machine, that _does_ halt, no??? >>>>>>>>>>>>>
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED.
Proof Theoretic Semantics does this very cleanly
it rejects all such inputs as semantically incoherent. >>>>>>>>>>>>>
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but
decidability problems within computing are _not_
intentionally modeled after the liar's paradox...
turing when he stumbled on the first undecidable situation >>>>>>>>>>> within computing was not considering the liar's paradox or >>>>>>>>>>> even godel's incompleteness directly. he was considering >>>>>>>>>>> cantor's diagonal formed across all circle-free machines. and >>>>>>>>>>> without certain fixes, the problem arises when the diagonal >>>>>>>>>>> machine is deciding on itself as circle-free... this was not >>>>>>>>>>> an intention constructional, but an artifact of self-
references within turing machine logic,
they just _are_ a possible construction within all
permutations of turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS. >>>>>>>>>>>>
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just >>>>>>>>>>> declare a machine that certainly halts as incoherent input to >>>>>>>>>>> a halting prover (without some further explanation of how the >>>>>>>>>>> truth of it being halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a valid >>>>>>>>> machine that halts when executed,
why do u think u need to insult me back when i point that out? >>>>>>>>>
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could
correctly decide on it...
Can Carol correctly answer “no” to this (yes/no) question?
E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
yes i know that, truth can be defined relative to a reference
point. same is true in physical too,
but u keep repeating on and on about bad input instead of
explaining both perspectives at the same time
I don't allocate equal weight to falsehoods.
The HP counter-example input has always been
bad and the only reason this is not universally
understood is that sheeple herd together in
the conventional views.
no, turing's diagonal counter-example, the _original_ problem, is not
a trivial program that produces no output.
it actually performs a computation and deciding on that computation
is an issue.
Any input that does the opposite of whatever value its
decider returns should have been rejected as bad input
is dead obvious.
the computation doesn't _try_ to contradict itself, it necessarily does
it as an artifact of it's construction of applying the decider to all input...
I am not sure how far back PTS has generically
rejected every expression that specifies cycles
in the directed graph of inference steps it may
be as far back as 1930.
The key relevant thing is that ALL PTS experts
now universally agree that such expressions
lack any semantic meaning because all PTS
experts universally agree that ALL semantic
meaning ONLY comes from finite sequences of
inference steps.
what the difference between a "finite sequence of inference steps" and a computation???
This article was written by the guy that coined
the term "proof theoretic semantics"
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs.
It thus belongs to inferentialism (a term coined by
Brandom, see his 1994; 2000) according to which
inferences and the rules of inference establish the
meaning of expressions...
Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
On 4/16/2026 9:04 PM, dart200 wrote:
On 4/16/26 11:52 AM, olcott wrote:
On 4/16/2026 1:29 PM, dart200 wrote:
On 4/16/26 11:20 AM, olcott wrote:
On 4/16/2026 12:41 PM, dart200 wrote:
On 4/15/26 8:51 PM, olcott wrote:
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
It has always been nuts to think that an input >>>>>>>>>>>>>>>>>>>>> that does the opposite of whatever value a halt >>>>>>>>>>>>>>>>>>>>> decider returns is a valid input. Ordinary >>>>>>>>>>>>>>>>>>>>> unadulterated proof theoretic semantics already >>>>>>>>>>>>>>>>>>>>> has the complete and perfect foundational basis >>>>>>>>>>>>>>>>>>>>> to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism >>>>>>>>>>>>>>>>>>>>> Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>>>>>>>>> which inferences and the rules of inference establish >>>>>>>>>>>>>>>>>>>>> the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic- >>>>>>>>>>>>>>>>>>>>> semantics/ #InfeIntuAntiReal
so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>>>>>>>
At this point that question becomes pure trolling >>>>>>>>>>>>>>>>>>> with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject >>>>>>>>>>>>>>>>>>> an input that does the opposite of whatever its >>>>>>>>>>>>>>>>>>> decider reports.
Proof theoretic semantics provides the complete >>>>>>>>>>>>>>>>>>> foundational basis for this rejection to be >>>>>>>>>>>>>>>>>>> accomplished algorithmically.
right but that machine DD _does_ halt...
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts??? >>>>>>>>>>>>>>>>
Everyone has been nuts to require a machine to
report on an input that was intentionally designed >>>>>>>>>>>>>>> to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of >>>>>>>>>>>>>> the total possible ways a machine can be constructed, >>>>>>>>>>>>>>
specifically because the possibility for machines >>>>>>>>>>>>>> referencing themselves (proven by kleene's second >>>>>>>>>>>>>> recursion theorem):
because machines can self-reference their own result, this >>>>>>>>>>>>>> kind of circular analytical paradox _is_ possible
except DD _is_ a valid machine, that _does_ halt, no??? >>>>>>>>>>>>>>
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED. >>>>>>>>>>>>>>> Proof Theoretic Semantics does this very cleanly >>>>>>>>>>>>>>> it rejects all such inputs as semantically incoherent. >>>>>>>>>>>>>>
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but
decidability problems within computing are _not_
intentionally modeled after the liar's paradox...
turing when he stumbled on the first undecidable situation >>>>>>>>>>>> within computing was not considering the liar's paradox or >>>>>>>>>>>> even godel's incompleteness directly. he was considering >>>>>>>>>>>> cantor's diagonal formed across all circle-free machines. >>>>>>>>>>>> and without certain fixes, the problem arises when the >>>>>>>>>>>> diagonal machine is deciding on itself as circle-free... >>>>>>>>>>>> this was not an intention constructional, but an artifact of >>>>>>>>>>>> self- references within turing machine logic,
they just _are_ a possible construction within all
permutations of turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS. >>>>>>>>>>>>>
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework
of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just >>>>>>>>>>>> declare a machine that certainly halts as incoherent input >>>>>>>>>>>> to a halting prover (without some further explanation of how >>>>>>>>>>>> the truth of it being halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a valid >>>>>>>>>> machine that halts when executed,
why do u think u need to insult me back when i point that out? >>>>>>>>>>
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could
correctly decide on it...
Can Carol correctly answer “no” to this (yes/no) question?
E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
yes i know that, truth can be defined relative to a reference
point. same is true in physical too,
but u keep repeating on and on about bad input instead of
explaining both perspectives at the same time
I don't allocate equal weight to falsehoods.
The HP counter-example input has always been
bad and the only reason this is not universally
understood is that sheeple herd together in
the conventional views.
no, turing's diagonal counter-example, the _original_ problem, is
not a trivial program that produces no output.
it actually performs a computation and deciding on that computation
is an issue.
Any input that does the opposite of whatever value its
decider returns should have been rejected as bad input
is dead obvious.
the computation doesn't _try_ to contradict itself, it necessarily
does it as an artifact of it's construction of applying the decider to
all input...
It is isomorphic to the Liar Paradox and the sheeple
of humanity never figured that out because the would
rather herd together than know the truth.
I am not sure how far back PTS has generically
rejected every expression that specifies cycles
in the directed graph of inference steps it may
be as far back as 1930.
The key relevant thing is that ALL PTS experts
now universally agree that such expressions
lack any semantic meaning because all PTS
experts universally agree that ALL semantic
meaning ONLY comes from finite sequences of
inference steps.
what the difference between a "finite sequence of inference steps" and
a computation???
What is wrong with a payroll system that gets
stuck in an infinite loop so that no one ever
gets paid? (same thing)
Unless the other paragraphs below are over-your-head
they provide the crucial foundational basis for how I
have been correct all along:
In analytic philosophy, anti-realism is the position
that the truth of a statement rests on its demonstrability
through internal logic mechanisms... https://en.wikipedia.org/wiki/Anti-realism
All that "anti-realism" is really saying is that truth
is computable even though the compositional meaning of
"anti-realism" says something like a psychotic break
from reality.
This article was written by the guy that coined
the term "proof theoretic semantics"
1.2 Inferentialism, intuitionism, anti-realism
Proof-theoretic semantics is inherently inferential,
as it is inferential activity which manifests itself
in proofs.
It thus belongs to inferentialism (a term coined by
Brandom, see his 1994; 2000) according to which
inferences and the rules of inference establish the
meaning of expressions...
Schroeder-Heister, Peter,
2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof-theoretic-semantics/
#InfeIntuAntiReal
On 4/16/26 7:21 PM, olcott wrote:
On 4/16/2026 9:04 PM, dart200 wrote:
On 4/16/26 11:52 AM, olcott wrote:
On 4/16/2026 1:29 PM, dart200 wrote:
On 4/16/26 11:20 AM, olcott wrote:
On 4/16/2026 12:41 PM, dart200 wrote:
On 4/15/26 8:51 PM, olcott wrote:
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote:
On 4/14/26 6:30 AM, olcott wrote:
so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>>>>>>>>
It has always been nuts to think that an input >>>>>>>>>>>>>>>>>>>>>> that does the opposite of whatever value a halt >>>>>>>>>>>>>>>>>>>>>> decider returns is a valid input. Ordinary >>>>>>>>>>>>>>>>>>>>>> unadulterated proof theoretic semantics already >>>>>>>>>>>>>>>>>>>>>> has the complete and perfect foundational basis >>>>>>>>>>>>>>>>>>>>>> to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism >>>>>>>>>>>>>>>>>>>>>> Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>>>>>>>>>> which inferences and the rules of inference establish >>>>>>>>>>>>>>>>>>>>>> the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics"
https://plato.stanford.edu/entries/proof- >>>>>>>>>>>>>>>>>>>>>> theoretic- semantics/ #InfeIntuAntiReal >>>>>>>>>>>>>>>>>>>>>
At this point that question becomes pure trolling >>>>>>>>>>>>>>>>>>>> with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject >>>>>>>>>>>>>>>>>>>> an input that does the opposite of whatever its >>>>>>>>>>>>>>>>>>>> decider reports.
Proof theoretic semantics provides the complete >>>>>>>>>>>>>>>>>>>> foundational basis for this rejection to be >>>>>>>>>>>>>>>>>>>> accomplished algorithmically.
right but that machine DD _does_ halt... >>>>>>>>>>>>>>>>>>>
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts??? >>>>>>>>>>>>>>>>>
Everyone has been nuts to require a machine to >>>>>>>>>>>>>>>> report on an input that was intentionally designed >>>>>>>>>>>>>>>> to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part of >>>>>>>>>>>>>>> the total possible ways a machine can be constructed, >>>>>>>>>>>>>>>
specifically because the possibility for machines >>>>>>>>>>>>>>> referencing themselves (proven by kleene's second >>>>>>>>>>>>>>> recursion theorem):
because machines can self-reference their own result, >>>>>>>>>>>>>>> this kind of circular analytical paradox _is_ possible >>>>>>>>>>>>>>>
except DD _is_ a valid machine, that _does_ halt, no??? >>>>>>>>>>>>>>>
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED. >>>>>>>>>>>>>>>> Proof Theoretic Semantics does this very cleanly >>>>>>>>>>>>>>>> it rejects all such inputs as semantically incoherent. >>>>>>>>>>>>>>>
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but
decidability problems within computing are _not_
intentionally modeled after the liar's paradox...
turing when he stumbled on the first undecidable situation >>>>>>>>>>>>> within computing was not considering the liar's paradox or >>>>>>>>>>>>> even godel's incompleteness directly. he was considering >>>>>>>>>>>>> cantor's diagonal formed across all circle-free machines. >>>>>>>>>>>>> and without certain fixes, the problem arises when the >>>>>>>>>>>>> diagonal machine is deciding on itself as circle-free... >>>>>>>>>>>>> this was not an intention constructional, but an artifact >>>>>>>>>>>>> of self- references within turing machine logic,
they just _are_ a possible construction within all
permutations of turing machine definitions
It also seems completely psychotic that even the
Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS. >>>>>>>>>>>>>>
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework >>>>>>>>>>>>>> of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just >>>>>>>>>>>>> declare a machine that certainly halts as incoherent input >>>>>>>>>>>>> to a halting prover (without some further explanation of >>>>>>>>>>>>> how the truth of it being halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING*
an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS*
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a >>>>>>>>>>> valid machine that halts when executed,
why do u think u need to insult me back when i point that out? >>>>>>>>>>>
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could
correctly decide on it...
Can Carol correctly answer “no” to this (yes/no) question? >>>>>>>> E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
yes i know that, truth can be defined relative to a reference
point. same is true in physical too,
but u keep repeating on and on about bad input instead of
explaining both perspectives at the same time
I don't allocate equal weight to falsehoods.
The HP counter-example input has always been
bad and the only reason this is not universally
understood is that sheeple herd together in
the conventional views.
no, turing's diagonal counter-example, the _original_ problem, is
not a trivial program that produces no output.
it actually performs a computation and deciding on that computation >>>>> is an issue.
Any input that does the opposite of whatever value its
decider returns should have been rejected as bad input
is dead obvious.
the computation doesn't _try_ to contradict itself, it necessarily
does it as an artifact of it's construction of applying the decider
to all input...
It is isomorphic to the Liar Paradox and the sheeple
is it not "isomorhpic" to the liar's paradox, it an infinitely running computation that tests the entire enumeration of machines, and in doing
so stumbles on trying to decide on itself as either a circular or circle-free machine, both of which are infinitely running results.
the liar's paradox does no such thing even remotely
the circle-free paradox is not an intentional construction to deceive a decider ... it just is a result of trying to universally apply a true/
false circle-free decider to all machines, causing the decider to fail
on deciding itself.
On 4/16/2026 9:59 PM, dart200 wrote:
On 4/16/26 7:21 PM, olcott wrote:
On 4/16/2026 9:04 PM, dart200 wrote:
On 4/16/26 11:52 AM, olcott wrote:
On 4/16/2026 1:29 PM, dart200 wrote:
On 4/16/26 11:20 AM, olcott wrote:
On 4/16/2026 12:41 PM, dart200 wrote:
On 4/15/26 8:51 PM, olcott wrote:
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote: >>>>>>>>>>>>>>>>>>>>>> On 4/14/26 6:30 AM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>
It has always been nuts to think that an input >>>>>>>>>>>>>>>>>>>>>>> that does the opposite of whatever value a halt >>>>>>>>>>>>>>>>>>>>>>> decider returns is a valid input. Ordinary >>>>>>>>>>>>>>>>>>>>>>> unadulterated proof theoretic semantics already >>>>>>>>>>>>>>>>>>>>>>> has the complete and perfect foundational basis >>>>>>>>>>>>>>>>>>>>>>> to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>>>>>>>>>so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism >>>>>>>>>>>>>>>>>>>>>>> Proof-theoretic semantics is inherently inferential, >>>>>>>>>>>>>>>>>>>>>>> as it is inferential activity which manifests itself >>>>>>>>>>>>>>>>>>>>>>> in proofs. It thus belongs to inferentialism (a term >>>>>>>>>>>>>>>>>>>>>>> coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>>>>>>>>>>> which inferences and the rules of inference >>>>>>>>>>>>>>>>>>>>>>> establish
the meaning of expressions Schroeder-Heister, Peter, >>>>>>>>>>>>>>>>>>>>>>> 2024 "Proof-Theoretic Semantics" >>>>>>>>>>>>>>>>>>>>>>>
https://plato.stanford.edu/entries/proof- >>>>>>>>>>>>>>>>>>>>>>> theoretic- semantics/ #InfeIntuAntiReal >>>>>>>>>>>>>>>>>>>>>>
At this point that question becomes pure trolling >>>>>>>>>>>>>>>>>>>>> with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject >>>>>>>>>>>>>>>>>>>>> an input that does the opposite of whatever its >>>>>>>>>>>>>>>>>>>>> decider reports.
Proof theoretic semantics provides the complete >>>>>>>>>>>>>>>>>>>>> foundational basis for this rejection to be >>>>>>>>>>>>>>>>>>>>> accomplished algorithmically.
right but that machine DD _does_ halt... >>>>>>>>>>>>>>>>>>>>
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts??? >>>>>>>>>>>>>>>>>>
Everyone has been nuts to require a machine to >>>>>>>>>>>>>>>>> report on an input that was intentionally designed >>>>>>>>>>>>>>>>> to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part >>>>>>>>>>>>>>>> of the total possible ways a machine can be constructed, >>>>>>>>>>>>>>>>
specifically because the possibility for machines >>>>>>>>>>>>>>>> referencing themselves (proven by kleene's second >>>>>>>>>>>>>>>> recursion theorem):
because machines can self-reference their own result, >>>>>>>>>>>>>>>> this kind of circular analytical paradox _is_ possible >>>>>>>>>>>>>>>>
except DD _is_ a valid machine, that _does_ halt, no??? >>>>>>>>>>>>>>>>
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED. >>>>>>>>>>>>>>>>> Proof Theoretic Semantics does this very cleanly >>>>>>>>>>>>>>>>> it rejects all such inputs as semantically incoherent. >>>>>>>>>>>>>>>>
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but >>>>>>>>>>>>>> decidability problems within computing are _not_
intentionally modeled after the liar's paradox...
turing when he stumbled on the first undecidable situation >>>>>>>>>>>>>> within computing was not considering the liar's paradox or >>>>>>>>>>>>>> even godel's incompleteness directly. he was considering >>>>>>>>>>>>>> cantor's diagonal formed across all circle-free machines. >>>>>>>>>>>>>> and without certain fixes, the problem arises when the >>>>>>>>>>>>>> diagonal machine is deciding on itself as circle-free... >>>>>>>>>>>>>> this was not an intention constructional, but an artifact >>>>>>>>>>>>>> of self- references within turing machine logic,
they just _are_ a possible construction within all >>>>>>>>>>>>>> permutations of turing machine definitions
It also seems completely psychotic that even the >>>>>>>>>>>>>>> Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS. >>>>>>>>>>>>>>>
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework >>>>>>>>>>>>>>> of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just >>>>>>>>>>>>>> declare a machine that certainly halts as incoherent input >>>>>>>>>>>>>> to a halting prover (without some further explanation of >>>>>>>>>>>>>> how the truth of it being halting is ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING* >>>>>>>>>>>>> an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS* >>>>>>>>>>>>>
Proof Theoretic Semantics inherently does this for
every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed
to be considered.
i don't need to insult you to point out the fact DD is a >>>>>>>>>>>> valid machine that halts when executed,
why do u think u need to insult me back when i point that out? >>>>>>>>>>>>
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could >>>>>>>>>> correctly decide on it...
Can Carol correctly answer “no” to this (yes/no) question? >>>>>>>>> E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
yes i know that, truth can be defined relative to a reference >>>>>>>> point. same is true in physical too,
but u keep repeating on and on about bad input instead of
explaining both perspectives at the same time
I don't allocate equal weight to falsehoods.
The HP counter-example input has always been
bad and the only reason this is not universally
understood is that sheeple herd together in
the conventional views.
no, turing's diagonal counter-example, the _original_ problem, is >>>>>> not a trivial program that produces no output.
it actually performs a computation and deciding on that
computation is an issue.
Any input that does the opposite of whatever value its
decider returns should have been rejected as bad input
is dead obvious.
the computation doesn't _try_ to contradict itself, it necessarily
does it as an artifact of it's construction of applying the decider
to all input...
It is isomorphic to the Liar Paradox and the sheeple
is it not "isomorhpic" to the liar's paradox, it an infinitely running
computation that tests the entire enumeration of machines, and in
doing so stumbles on trying to decide on itself as either a circular
or circle-free machine, both of which are infinitely running results.
the liar's paradox does no such thing even remotely
the circle-free paradox is not an intentional construction to deceive
a decider ... it just is a result of trying to universally apply a
true/ false circle-free decider to all machines, causing the decider
to fail on deciding itself.
I proved the HP input is the same as the Liar Paradox back in 2004
On 4/16/26 8:15 PM, olcott wrote:
On 4/16/2026 9:59 PM, dart200 wrote:
On 4/16/26 7:21 PM, olcott wrote:
On 4/16/2026 9:04 PM, dart200 wrote:
On 4/16/26 11:52 AM, olcott wrote:
On 4/16/2026 1:29 PM, dart200 wrote:
On 4/16/26 11:20 AM, olcott wrote:
On 4/16/2026 12:41 PM, dart200 wrote:
On 4/15/26 8:51 PM, olcott wrote:
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote:
On 4/14/26 4:01 PM, olcott wrote:
On 4/14/2026 3:53 PM, dart200 wrote: >>>>>>>>>>>>>>>>>>>>>>> On 4/14/26 6:30 AM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>
It has always been nuts to think that an input >>>>>>>>>>>>>>>>>>>>>>>> that does the opposite of whatever value a halt >>>>>>>>>>>>>>>>>>>>>>>> decider returns is a valid input. Ordinary >>>>>>>>>>>>>>>>>>>>>>>> unadulterated proof theoretic semantics already >>>>>>>>>>>>>>>>>>>>>>>> has the complete and perfect foundational basis >>>>>>>>>>>>>>>>>>>>>>>> to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>>>>>>>>>>so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism >>>>>>>>>>>>>>>>>>>>>>>> Proof-theoretic semantics is inherently >>>>>>>>>>>>>>>>>>>>>>>> inferential,
as it is inferential activity which manifests >>>>>>>>>>>>>>>>>>>>>>>> itself
in proofs. It thus belongs to inferentialism (a >>>>>>>>>>>>>>>>>>>>>>>> term
coined by Brandom, see his 1994; 2000) according to >>>>>>>>>>>>>>>>>>>>>>>> which inferences and the rules of inference >>>>>>>>>>>>>>>>>>>>>>>> establish
the meaning of expressions Schroeder-Heister, >>>>>>>>>>>>>>>>>>>>>>>> Peter,
2024 "Proof-Theoretic Semantics" >>>>>>>>>>>>>>>>>>>>>>>>
https://plato.stanford.edu/entries/proof- >>>>>>>>>>>>>>>>>>>>>>>> theoretic- semantics/ #InfeIntuAntiReal >>>>>>>>>>>>>>>>>>>>>>>
At this point that question becomes pure trolling >>>>>>>>>>>>>>>>>>>>>> with zero honest dialogue intent.
It has ALWAYS been 100% TOTALLY NUTS to not reject >>>>>>>>>>>>>>>>>>>>>> an input that does the opposite of whatever its >>>>>>>>>>>>>>>>>>>>>> decider reports.
Proof theoretic semantics provides the complete >>>>>>>>>>>>>>>>>>>>>> foundational basis for this rejection to be >>>>>>>>>>>>>>>>>>>>>> accomplished algorithmically.
right but that machine DD _does_ halt... >>>>>>>>>>>>>>>>>>>>>
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts??? >>>>>>>>>>>>>>>>>>>
Everyone has been nuts to require a machine to >>>>>>>>>>>>>>>>>> report on an input that was intentionally designed >>>>>>>>>>>>>>>>>> to do the opposite of whatever it reports.
but it's not "intentional", it just happens to be part >>>>>>>>>>>>>>>>> of the total possible ways a machine can be constructed, >>>>>>>>>>>>>>>>>
specifically because the possibility for machines >>>>>>>>>>>>>>>>> referencing themselves (proven by kleene's second >>>>>>>>>>>>>>>>> recursion theorem):
because machines can self-reference their own result, >>>>>>>>>>>>>>>>> this kind of circular analytical paradox _is_ possible >>>>>>>>>>>>>>>>>
except DD _is_ a valid machine, that _does_ halt, no??? >>>>>>>>>>>>>>>>>
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED. >>>>>>>>>>>>>>>>>> Proof Theoretic Semantics does this very cleanly >>>>>>>>>>>>>>>>>> it rejects all such inputs as semantically incoherent. >>>>>>>>>>>>>>>>>
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but >>>>>>>>>>>>>>> decidability problems within computing are _not_ >>>>>>>>>>>>>>> intentionally modeled after the liar's paradox... >>>>>>>>>>>>>>>
turing when he stumbled on the first undecidable >>>>>>>>>>>>>>> situation within computing was not considering the liar's >>>>>>>>>>>>>>> paradox or even godel's incompleteness directly. he was >>>>>>>>>>>>>>> considering cantor's diagonal formed across all circle- >>>>>>>>>>>>>>> free machines. and without certain fixes, the problem >>>>>>>>>>>>>>> arises when the diagonal machine is deciding on itself as >>>>>>>>>>>>>>> circle-free... this was not an intention constructional, >>>>>>>>>>>>>>> but an artifact of self- references within turing machine >>>>>>>>>>>>>>> logic,
they just _are_ a possible construction within all >>>>>>>>>>>>>>> permutations of turing machine definitions
It also seems completely psychotic that even the >>>>>>>>>>>>>>>> Liar Paradox has not been OFFICIALLY ruled to
have always been incoherent nonsense AFTER 2000 YEARS. >>>>>>>>>>>>>>>>
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>>>>>>>> false.
The above unequivocally proves that the Liar
Paradox exactly and precisely within the framework >>>>>>>>>>>>>>>> of Proof Theoretic Semantics is semantically
incoherent.
i agree something fishy is going on, but we cannot just >>>>>>>>>>>>>>> declare a machine that certainly halts as incoherent >>>>>>>>>>>>>>> input to a halting prover (without some further >>>>>>>>>>>>>>> explanation of how the truth of it being halting is >>>>>>>>>>>>>>> ascertained)
Unless UR nuts (or so indoctrinated to drink the
Kool-Aid of the conventional view that you can't
think clearly) you would realize that *NOT REJECTING* >>>>>>>>>>>>>> an input that does the opposite of whatever value
its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS* >>>>>>>>>>>>>>
Proof Theoretic Semantics inherently does this for >>>>>>>>>>>>>> every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of
the C programming language cannot possibly reach
its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed >>>>>>>>>>>>>> to be considered.
i don't need to insult you to point out the fact DD is a >>>>>>>>>>>>> valid machine that halts when executed,
why do u think u need to insult me back when i point that out? >>>>>>>>>>>>>
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could >>>>>>>>>>> correctly decide on it...
Can Carol correctly answer “no” to this (yes/no) question? >>>>>>>>>> E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
yes i know that, truth can be defined relative to a reference >>>>>>>>> point. same is true in physical too,
but u keep repeating on and on about bad input instead of
explaining both perspectives at the same time
I don't allocate equal weight to falsehoods.
The HP counter-example input has always been
bad and the only reason this is not universally
understood is that sheeple herd together in
the conventional views.
no, turing's diagonal counter-example, the _original_ problem, is >>>>>>> not a trivial program that produces no output.
it actually performs a computation and deciding on that
computation is an issue.
Any input that does the opposite of whatever value its
decider returns should have been rejected as bad input
is dead obvious.
the computation doesn't _try_ to contradict itself, it necessarily
does it as an artifact of it's construction of applying the decider >>>>> to all input...
It is isomorphic to the Liar Paradox and the sheeple
is it not "isomorhpic" to the liar's paradox, it an infinitely
running computation that tests the entire enumeration of machines,
and in doing so stumbles on trying to decide on itself as either a
circular or circle-free machine, both of which are infinitely running
results.
the liar's paradox does no such thing even remotely
the circle-free paradox is not an intentional construction to deceive
a decider ... it just is a result of trying to universally apply a
true/ false circle-free decider to all machines, causing the decider
to fail on deciding itself.
I proved the HP input is the same as the Liar Paradox back in 2004
the circle-free problem found in turing's diagonals are not the same
thing as the halting problem, peter
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its definition
is irrelevant to the first incompletness theorem.
Olcott's Minimal Type Theory
G ↔ ¬Prov[PA](⌜G⌝)
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov[PA] 04
04 Gödel_Number_of 01 // cycle
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first incompleteness theorem sentence
has a cycle in the directed graph of its
evaluation sequence making it semantically
incoherent.
This kind of semantically incoherence is
foundational in proof theoretic semantics.
DD simulated by HHH conclusively proves that it
cannot possibly stop running unless HHH aborts it.
Author of #1 best seller for theory of computation texts
<MIT Professor Sipser agreed to ONLY these verbatim words 10/13/2022>
If simulating halt decider H correctly simulates its
input D until H correctly determines that its simulated D
would never stop running unless aborted then
H can abort its simulation of D and correctly report that D
specifies a non-halting sequence of configurations.
</MIT Professor Sipser agreed to ONLY these verbatim words 10/13/2022>
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its definition >>> is irrelevant to the first incompletness theorem.
Olcott's Minimal Type Theory
G ↔ ¬Prov[PA](⌜G⌝)
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov[PA] 04
04 Gödel_Number_of 01 // cycle
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first incompleteness theorem sentence
has a cycle in the directed graph of its
evaluation sequence making it semantically
incoherent.
This kind of semantically incoherence is
foundational in proof theoretic semantics.
Nice to see that you don't disagree.
On 4/16/2026 10:21 PM, dart200 wrote:
On 4/16/26 8:15 PM, olcott wrote:
On 4/16/2026 9:59 PM, dart200 wrote:
On 4/16/26 7:21 PM, olcott wrote:
On 4/16/2026 9:04 PM, dart200 wrote:
On 4/16/26 11:52 AM, olcott wrote:
On 4/16/2026 1:29 PM, dart200 wrote:
On 4/16/26 11:20 AM, olcott wrote:
On 4/16/2026 12:41 PM, dart200 wrote:
On 4/15/26 8:51 PM, olcott wrote:
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:but it's not "intentional", it just happens to be part >>>>>>>>>>>>>>>>>> of the total possible ways a machine can be constructed, >>>>>>>>>>>>>>>>>>
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote: >>>>>>>>>>>>>>>>>>>>>> On 4/14/26 4:01 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>> On 4/14/2026 3:53 PM, dart200 wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 4/14/26 6:30 AM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>
It has always been nuts to think that an input >>>>>>>>>>>>>>>>>>>>>>>>> that does the opposite of whatever value a halt >>>>>>>>>>>>>>>>>>>>>>>>> decider returns is a valid input. Ordinary >>>>>>>>>>>>>>>>>>>>>>>>> unadulterated proof theoretic semantics already >>>>>>>>>>>>>>>>>>>>>>>>> has the complete and perfect foundational basis >>>>>>>>>>>>>>>>>>>>>>>>> to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>>>>>>>>>>>so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism >>>>>>>>>>>>>>>>>>>>>>>>> Proof-theoretic semantics is inherently >>>>>>>>>>>>>>>>>>>>>>>>> inferential,
as it is inferential activity which manifests >>>>>>>>>>>>>>>>>>>>>>>>> itself
in proofs. It thus belongs to inferentialism (a >>>>>>>>>>>>>>>>>>>>>>>>> term
coined by Brandom, see his 1994; 2000) >>>>>>>>>>>>>>>>>>>>>>>>> according to
which inferences and the rules of inference >>>>>>>>>>>>>>>>>>>>>>>>> establish
the meaning of expressions Schroeder-Heister, >>>>>>>>>>>>>>>>>>>>>>>>> Peter,
2024 "Proof-Theoretic Semantics" >>>>>>>>>>>>>>>>>>>>>>>>>
https://plato.stanford.edu/entries/proof- >>>>>>>>>>>>>>>>>>>>>>>>> theoretic- semantics/ #InfeIntuAntiReal >>>>>>>>>>>>>>>>>>>>>>>>
At this point that question becomes pure trolling >>>>>>>>>>>>>>>>>>>>>>> with zero honest dialogue intent. >>>>>>>>>>>>>>>>>>>>>>>
It has ALWAYS been 100% TOTALLY NUTS to not reject >>>>>>>>>>>>>>>>>>>>>>> an input that does the opposite of whatever its >>>>>>>>>>>>>>>>>>>>>>> decider reports.
Proof theoretic semantics provides the complete >>>>>>>>>>>>>>>>>>>>>>> foundational basis for this rejection to be >>>>>>>>>>>>>>>>>>>>>>> accomplished algorithmically.
right but that machine DD _does_ halt... >>>>>>>>>>>>>>>>>>>>>>
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts??? >>>>>>>>>>>>>>>>>>>>
Everyone has been nuts to require a machine to >>>>>>>>>>>>>>>>>>> report on an input that was intentionally designed >>>>>>>>>>>>>>>>>>> to do the opposite of whatever it reports. >>>>>>>>>>>>>>>>>>
specifically because the possibility for machines >>>>>>>>>>>>>>>>>> referencing themselves (proven by kleene's second >>>>>>>>>>>>>>>>>> recursion theorem):
because machines can self-reference their own result, >>>>>>>>>>>>>>>>>> this kind of circular analytical paradox _is_ possible >>>>>>>>>>>>>>>>>>
except DD _is_ a valid machine, that _does_ halt, no??? >>>>>>>>>>>>>>>>>>
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED. >>>>>>>>>>>>>>>>>>> Proof Theoretic Semantics does this very cleanly >>>>>>>>>>>>>>>>>>> it rejects all such inputs as semantically incoherent. >>>>>>>>>>>>>>>>>>
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but >>>>>>>>>>>>>>>> decidability problems within computing are _not_ >>>>>>>>>>>>>>>> intentionally modeled after the liar's paradox... >>>>>>>>>>>>>>>>
turing when he stumbled on the first undecidable >>>>>>>>>>>>>>>> situation within computing was not considering the >>>>>>>>>>>>>>>> liar's paradox or even godel's incompleteness directly. >>>>>>>>>>>>>>>> he was considering cantor's diagonal formed across all >>>>>>>>>>>>>>>> circle- free machines. and without certain fixes, the >>>>>>>>>>>>>>>> problem arises when the diagonal machine is deciding on >>>>>>>>>>>>>>>> itself as circle-free... this was not an intention >>>>>>>>>>>>>>>> constructional, but an artifact of self- references >>>>>>>>>>>>>>>> within turing machine logic,
they just _are_ a possible construction within all >>>>>>>>>>>>>>>> permutations of turing machine definitions
It also seems completely psychotic that even the >>>>>>>>>>>>>>>>> Liar Paradox has not been OFFICIALLY ruled to >>>>>>>>>>>>>>>>> have always been incoherent nonsense AFTER 2000 YEARS. >>>>>>>>>>>>>>>>>
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>>>>>>>>> false.
The above unequivocally proves that the Liar >>>>>>>>>>>>>>>>> Paradox exactly and precisely within the framework >>>>>>>>>>>>>>>>> of Proof Theoretic Semantics is semantically >>>>>>>>>>>>>>>>> incoherent.
i agree something fishy is going on, but we cannot just >>>>>>>>>>>>>>>> declare a machine that certainly halts as incoherent >>>>>>>>>>>>>>>> input to a halting prover (without some further >>>>>>>>>>>>>>>> explanation of how the truth of it being halting is >>>>>>>>>>>>>>>> ascertained)
Unless UR nuts (or so indoctrinated to drink the >>>>>>>>>>>>>>> Kool-Aid of the conventional view that you can't >>>>>>>>>>>>>>> think clearly) you would realize that *NOT REJECTING* >>>>>>>>>>>>>>> an input that does the opposite of whatever value >>>>>>>>>>>>>>> its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS* >>>>>>>>>>>>>>>
Proof Theoretic Semantics inherently does this for >>>>>>>>>>>>>>> every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of >>>>>>>>>>>>>>> the C programming language cannot possibly reach >>>>>>>>>>>>>>> its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed >>>>>>>>>>>>>>> to be considered.
i don't need to insult you to point out the fact DD is a >>>>>>>>>>>>>> valid machine that halts when executed,
why do u think u need to insult me back when i point that >>>>>>>>>>>>>> out?
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could >>>>>>>>>>>> correctly decide on it...
Can Carol correctly answer “no” to this (yes/no) question? >>>>>>>>>>> E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
yes i know that, truth can be defined relative to a reference >>>>>>>>>> point. same is true in physical too,
but u keep repeating on and on about bad input instead of >>>>>>>>>> explaining both perspectives at the same time
I don't allocate equal weight to falsehoods.
The HP counter-example input has always been
bad and the only reason this is not universally
understood is that sheeple herd together in
the conventional views.
no, turing's diagonal counter-example, the _original_ problem, >>>>>>>> is not a trivial program that produces no output.
it actually performs a computation and deciding on that
computation is an issue.
Any input that does the opposite of whatever value its
decider returns should have been rejected as bad input
is dead obvious.
the computation doesn't _try_ to contradict itself, it necessarily >>>>>> does it as an artifact of it's construction of applying the
decider to all input...
It is isomorphic to the Liar Paradox and the sheeple
is it not "isomorhpic" to the liar's paradox, it an infinitely
running computation that tests the entire enumeration of machines,
and in doing so stumbles on trying to decide on itself as either a
circular or circle-free machine, both of which are infinitely
running results.
the liar's paradox does no such thing even remotely
the circle-free paradox is not an intentional construction to
deceive a decider ... it just is a result of trying to universally
apply a true/ false circle-free decider to all machines, causing the
decider to fail on deciding itself.
I proved the HP input is the same as the Liar Paradox back in 2004
the circle-free problem found in turing's diagonals are not the same
thing as the halting problem, peter
Are claiming that all of the textbooks about the
halting problem are a complete misrepresentation this: https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf
My process is to start with the succinct essence of
enormously difficult analytical problems and then
spend decades boiling them down to their barest
possible essence.
This is the succinct essence that I started with. https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
The barest possible essence is that a proof theoretic
halt prover H rejects the HP counter-example input
D as meaningless. In PTS meaning is only acquired
through a finite sequence of inference steps. Infinite
sequences are rejected as ungrounded.
The above uses exactly standard PTS terminology
to the best of my current ability.
On 4/16/26 9:29 PM, olcott wrote:
On 4/16/2026 10:21 PM, dart200 wrote:
On 4/16/26 8:15 PM, olcott wrote:
On 4/16/2026 9:59 PM, dart200 wrote:
On 4/16/26 7:21 PM, olcott wrote:
On 4/16/2026 9:04 PM, dart200 wrote:
On 4/16/26 11:52 AM, olcott wrote:
On 4/16/2026 1:29 PM, dart200 wrote:
On 4/16/26 11:20 AM, olcott wrote:
On 4/16/2026 12:41 PM, dart200 wrote:
On 4/15/26 8:51 PM, olcott wrote:
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:but it's not "intentional", it just happens to be >>>>>>>>>>>>>>>>>>> part of the total possible ways a machine can be >>>>>>>>>>>>>>>>>>> constructed,
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote: >>>>>>>>>>>>>>>>>>>>>>> On 4/14/26 4:01 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 4/14/2026 3:53 PM, dart200 wrote: >>>>>>>>>>>>>>>>>>>>>>>>> On 4/14/26 6:30 AM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>>
It has always been nuts to think that an input >>>>>>>>>>>>>>>>>>>>>>>>>> that does the opposite of whatever value a halt >>>>>>>>>>>>>>>>>>>>>>>>>> decider returns is a valid input. Ordinary >>>>>>>>>>>>>>>>>>>>>>>>>> unadulterated proof theoretic semantics already >>>>>>>>>>>>>>>>>>>>>>>>>> has the complete and perfect foundational basis >>>>>>>>>>>>>>>>>>>>>>>>>> to reject these inputs as semantically >>>>>>>>>>>>>>>>>>>>>>>>>> incoherent.so you do agree DD halts when executed??? or >>>>>>>>>>>>>>>>>>>>>>>>> not???
1.2 Inferentialism, intuitionism, anti-realism >>>>>>>>>>>>>>>>>>>>>>>>>> Proof-theoretic semantics is inherently >>>>>>>>>>>>>>>>>>>>>>>>>> inferential,
as it is inferential activity which manifests >>>>>>>>>>>>>>>>>>>>>>>>>> itself
in proofs. It thus belongs to inferentialism >>>>>>>>>>>>>>>>>>>>>>>>>> (a term
coined by Brandom, see his 1994; 2000) >>>>>>>>>>>>>>>>>>>>>>>>>> according to
which inferences and the rules of inference >>>>>>>>>>>>>>>>>>>>>>>>>> establish
the meaning of expressions Schroeder-Heister, >>>>>>>>>>>>>>>>>>>>>>>>>> Peter,
2024 "Proof-Theoretic Semantics" >>>>>>>>>>>>>>>>>>>>>>>>>>
https://plato.stanford.edu/entries/proof- >>>>>>>>>>>>>>>>>>>>>>>>>> theoretic- semantics/ #InfeIntuAntiReal >>>>>>>>>>>>>>>>>>>>>>>>>
At this point that question becomes pure trolling >>>>>>>>>>>>>>>>>>>>>>>> with zero honest dialogue intent. >>>>>>>>>>>>>>>>>>>>>>>>
It has ALWAYS been 100% TOTALLY NUTS to not reject >>>>>>>>>>>>>>>>>>>>>>>> an input that does the opposite of whatever its >>>>>>>>>>>>>>>>>>>>>>>> decider reports.
Proof theoretic semantics provides the complete >>>>>>>>>>>>>>>>>>>>>>>> foundational basis for this rejection to be >>>>>>>>>>>>>>>>>>>>>>>> accomplished algorithmically.
right but that machine DD _does_ halt... >>>>>>>>>>>>>>>>>>>>>>>
Sew UR nuts.
i'm nuts for suggesting that a halting machine >>>>>>>>>>>>>>>>>>>>> halts???
Everyone has been nuts to require a machine to >>>>>>>>>>>>>>>>>>>> report on an input that was intentionally designed >>>>>>>>>>>>>>>>>>>> to do the opposite of whatever it reports. >>>>>>>>>>>>>>>>>>>
specifically because the possibility for machines >>>>>>>>>>>>>>>>>>> referencing themselves (proven by kleene's second >>>>>>>>>>>>>>>>>>> recursion theorem):
because machines can self-reference their own result, >>>>>>>>>>>>>>>>>>> this kind of circular analytical paradox _is_ possible >>>>>>>>>>>>>>>>>>>
except DD _is_ a valid machine, that _does_ halt, no??? >>>>>>>>>>>>>>>>>>>
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED. >>>>>>>>>>>>>>>>>>>> Proof Theoretic Semantics does this very cleanly >>>>>>>>>>>>>>>>>>>> it rejects all such inputs as semantically incoherent. >>>>>>>>>>>>>>>>>>>
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but >>>>>>>>>>>>>>>>> decidability problems within computing are _not_ >>>>>>>>>>>>>>>>> intentionally modeled after the liar's paradox... >>>>>>>>>>>>>>>>>
turing when he stumbled on the first undecidable >>>>>>>>>>>>>>>>> situation within computing was not considering the >>>>>>>>>>>>>>>>> liar's paradox or even godel's incompleteness directly. >>>>>>>>>>>>>>>>> he was considering cantor's diagonal formed across all >>>>>>>>>>>>>>>>> circle- free machines. and without certain fixes, the >>>>>>>>>>>>>>>>> problem arises when the diagonal machine is deciding on >>>>>>>>>>>>>>>>> itself as circle-free... this was not an intention >>>>>>>>>>>>>>>>> constructional, but an artifact of self- references >>>>>>>>>>>>>>>>> within turing machine logic,
they just _are_ a possible construction within all >>>>>>>>>>>>>>>>> permutations of turing machine definitions
It also seems completely psychotic that even the >>>>>>>>>>>>>>>>>> Liar Paradox has not been OFFICIALLY ruled to >>>>>>>>>>>>>>>>>> have always been incoherent nonsense AFTER 2000 YEARS. >>>>>>>>>>>>>>>>>>
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>>>>>>>>>> false.
The above unequivocally proves that the Liar >>>>>>>>>>>>>>>>>> Paradox exactly and precisely within the framework >>>>>>>>>>>>>>>>>> of Proof Theoretic Semantics is semantically >>>>>>>>>>>>>>>>>> incoherent.
i agree something fishy is going on, but we cannot just >>>>>>>>>>>>>>>>> declare a machine that certainly halts as incoherent >>>>>>>>>>>>>>>>> input to a halting prover (without some further >>>>>>>>>>>>>>>>> explanation of how the truth of it being halting is >>>>>>>>>>>>>>>>> ascertained)
Unless UR nuts (or so indoctrinated to drink the >>>>>>>>>>>>>>>> Kool-Aid of the conventional view that you can't >>>>>>>>>>>>>>>> think clearly) you would realize that *NOT REJECTING* >>>>>>>>>>>>>>>> an input that does the opposite of whatever value >>>>>>>>>>>>>>>> its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS* >>>>>>>>>>>>>>>>
Proof Theoretic Semantics inherently does this for >>>>>>>>>>>>>>>> every aspect of any input that does not have a >>>>>>>>>>>>>>>> finite back-chained sequence of inference steps >>>>>>>>>>>>>>>> to valid closure.
DD simulated by HHH according to the semantics of >>>>>>>>>>>>>>>> the C programming language cannot possibly reach >>>>>>>>>>>>>>>> its own return instruction in any finite number >>>>>>>>>>>>>>>> of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed >>>>>>>>>>>>>>>> to be considered.
i don't need to insult you to point out the fact DD is a >>>>>>>>>>>>>>> valid machine that halts when executed,
why do u think u need to insult me back when i point that >>>>>>>>>>>>>>> out?
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could >>>>>>>>>>>>> correctly decide on it...
Can Carol correctly answer “no” to this (yes/no) question? >>>>>>>>>>>> E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
yes i know that, truth can be defined relative to a reference >>>>>>>>>>> point. same is true in physical too,
but u keep repeating on and on about bad input instead of >>>>>>>>>>> explaining both perspectives at the same time
I don't allocate equal weight to falsehoods.
The HP counter-example input has always been
bad and the only reason this is not universally
understood is that sheeple herd together in
the conventional views.
no, turing's diagonal counter-example, the _original_ problem, >>>>>>>>> is not a trivial program that produces no output.
it actually performs a computation and deciding on that
computation is an issue.
Any input that does the opposite of whatever value its
decider returns should have been rejected as bad input
is dead obvious.
the computation doesn't _try_ to contradict itself, it
necessarily does it as an artifact of it's construction of
applying the decider to all input...
It is isomorphic to the Liar Paradox and the sheeple
is it not "isomorhpic" to the liar's paradox, it an infinitely
running computation that tests the entire enumeration of machines,
and in doing so stumbles on trying to decide on itself as either a
circular or circle-free machine, both of which are infinitely
running results.
the liar's paradox does no such thing even remotely
the circle-free paradox is not an intentional construction to
deceive a decider ... it just is a result of trying to universally
apply a true/ false circle-free decider to all machines, causing
the decider to fail on deciding itself.
I proved the HP input is the same as the Liar Paradox back in 2004
the circle-free problem found in turing's diagonals are not the same
thing as the halting problem, peter
Are claiming that all of the textbooks about the
halting problem are a complete misrepresentation this:
https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf
My process is to start with the succinct essence of
enormously difficult analytical problems and then
spend decades boiling them down to their barest
possible essence.
This is the succinct essence that I started with.
https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
The barest possible essence is that a proof theoretic
halt prover H rejects the HP counter-example input
D as meaningless. In PTS meaning is only acquired
through a finite sequence of inference steps. Infinite
sequences are rejected as ungrounded.
The above uses exactly standard PTS terminology
to the best of my current ability.
On 4/16/2026 10:21 PM, dart200 wrote:
On 4/16/26 8:15 PM, olcott wrote:
On 4/16/2026 9:59 PM, dart200 wrote:
On 4/16/26 7:21 PM, olcott wrote:
On 4/16/2026 9:04 PM, dart200 wrote:
On 4/16/26 11:52 AM, olcott wrote:
On 4/16/2026 1:29 PM, dart200 wrote:
On 4/16/26 11:20 AM, olcott wrote:
On 4/16/2026 12:41 PM, dart200 wrote:
On 4/15/26 8:51 PM, olcott wrote:
On 4/15/2026 10:23 PM, dart200 wrote:
On 4/15/26 8:18 PM, olcott wrote:
On 4/15/2026 9:37 PM, dart200 wrote:
On 4/15/26 8:19 AM, olcott wrote:
On 4/14/2026 10:30 PM, dart200 wrote:
On 4/14/26 7:15 PM, olcott wrote:
On 4/14/2026 8:27 PM, dart200 wrote:
On 4/14/26 6:11 PM, olcott wrote:
On 4/14/2026 7:26 PM, dart200 wrote:but it's not "intentional", it just happens to be part >>>>>>>>>>>>>>>>>> of the total possible ways a machine can be constructed, >>>>>>>>>>>>>>>>>>
On 4/14/26 5:14 PM, olcott wrote:
On 4/14/2026 6:44 PM, dart200 wrote: >>>>>>>>>>>>>>>>>>>>>> On 4/14/26 4:01 PM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>> On 4/14/2026 3:53 PM, dart200 wrote: >>>>>>>>>>>>>>>>>>>>>>>> On 4/14/26 6:30 AM, olcott wrote: >>>>>>>>>>>>>>>>>>>>>>>>>
It has always been nuts to think that an input >>>>>>>>>>>>>>>>>>>>>>>>> that does the opposite of whatever value a halt >>>>>>>>>>>>>>>>>>>>>>>>> decider returns is a valid input. Ordinary >>>>>>>>>>>>>>>>>>>>>>>>> unadulterated proof theoretic semantics already >>>>>>>>>>>>>>>>>>>>>>>>> has the complete and perfect foundational basis >>>>>>>>>>>>>>>>>>>>>>>>> to reject these inputs as semantically incoherent. >>>>>>>>>>>>>>>>>>>>>>>>>so you do agree DD halts when executed??? or not??? >>>>>>>>>>>>>>>>>>>>>>>>
1.2 Inferentialism, intuitionism, anti-realism >>>>>>>>>>>>>>>>>>>>>>>>> Proof-theoretic semantics is inherently >>>>>>>>>>>>>>>>>>>>>>>>> inferential,
as it is inferential activity which manifests >>>>>>>>>>>>>>>>>>>>>>>>> itself
in proofs. It thus belongs to inferentialism (a >>>>>>>>>>>>>>>>>>>>>>>>> term
coined by Brandom, see his 1994; 2000) >>>>>>>>>>>>>>>>>>>>>>>>> according to
which inferences and the rules of inference >>>>>>>>>>>>>>>>>>>>>>>>> establish
the meaning of expressions Schroeder-Heister, >>>>>>>>>>>>>>>>>>>>>>>>> Peter,
2024 "Proof-Theoretic Semantics" >>>>>>>>>>>>>>>>>>>>>>>>>
https://plato.stanford.edu/entries/proof- >>>>>>>>>>>>>>>>>>>>>>>>> theoretic- semantics/ #InfeIntuAntiReal >>>>>>>>>>>>>>>>>>>>>>>>
At this point that question becomes pure trolling >>>>>>>>>>>>>>>>>>>>>>> with zero honest dialogue intent. >>>>>>>>>>>>>>>>>>>>>>>
It has ALWAYS been 100% TOTALLY NUTS to not reject >>>>>>>>>>>>>>>>>>>>>>> an input that does the opposite of whatever its >>>>>>>>>>>>>>>>>>>>>>> decider reports.
Proof theoretic semantics provides the complete >>>>>>>>>>>>>>>>>>>>>>> foundational basis for this rejection to be >>>>>>>>>>>>>>>>>>>>>>> accomplished algorithmically.
right but that machine DD _does_ halt... >>>>>>>>>>>>>>>>>>>>>>
Sew UR nuts.
i'm nuts for suggesting that a halting machine halts??? >>>>>>>>>>>>>>>>>>>>
Everyone has been nuts to require a machine to >>>>>>>>>>>>>>>>>>> report on an input that was intentionally designed >>>>>>>>>>>>>>>>>>> to do the opposite of whatever it reports. >>>>>>>>>>>>>>>>>>
specifically because the possibility for machines >>>>>>>>>>>>>>>>>> referencing themselves (proven by kleene's second >>>>>>>>>>>>>>>>>> recursion theorem):
because machines can self-reference their own result, >>>>>>>>>>>>>>>>>> this kind of circular analytical paradox _is_ possible >>>>>>>>>>>>>>>>>>
except DD _is_ a valid machine, that _does_ halt, no??? >>>>>>>>>>>>>>>>>>
THIS IS A CLEAR CASE OF BAD DATA TO BE REJECTED. >>>>>>>>>>>>>>>>>>> Proof Theoretic Semantics does this very cleanly >>>>>>>>>>>>>>>>>>> it rejects all such inputs as semantically incoherent. >>>>>>>>>>>>>>>>>>
IT WAS MODELED AFTER THE LIAR PARADOX.
it happens to fit that form much of the time, but >>>>>>>>>>>>>>>> decidability problems within computing are _not_ >>>>>>>>>>>>>>>> intentionally modeled after the liar's paradox... >>>>>>>>>>>>>>>>
turing when he stumbled on the first undecidable >>>>>>>>>>>>>>>> situation within computing was not considering the >>>>>>>>>>>>>>>> liar's paradox or even godel's incompleteness directly. >>>>>>>>>>>>>>>> he was considering cantor's diagonal formed across all >>>>>>>>>>>>>>>> circle- free machines. and without certain fixes, the >>>>>>>>>>>>>>>> problem arises when the diagonal machine is deciding on >>>>>>>>>>>>>>>> itself as circle-free... this was not an intention >>>>>>>>>>>>>>>> constructional, but an artifact of self- references >>>>>>>>>>>>>>>> within turing machine logic,
they just _are_ a possible construction within all >>>>>>>>>>>>>>>> permutations of turing machine definitions
It also seems completely psychotic that even the >>>>>>>>>>>>>>>>> Liar Paradox has not been OFFICIALLY ruled to >>>>>>>>>>>>>>>>> have always been incoherent nonsense AFTER 2000 YEARS. >>>>>>>>>>>>>>>>>
% This sentence is not true.
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>>>>>>>>> false.
The above unequivocally proves that the Liar >>>>>>>>>>>>>>>>> Paradox exactly and precisely within the framework >>>>>>>>>>>>>>>>> of Proof Theoretic Semantics is semantically >>>>>>>>>>>>>>>>> incoherent.
i agree something fishy is going on, but we cannot just >>>>>>>>>>>>>>>> declare a machine that certainly halts as incoherent >>>>>>>>>>>>>>>> input to a halting prover (without some further >>>>>>>>>>>>>>>> explanation of how the truth of it being halting is >>>>>>>>>>>>>>>> ascertained)
Unless UR nuts (or so indoctrinated to drink the >>>>>>>>>>>>>>> Kool-Aid of the conventional view that you can't >>>>>>>>>>>>>>> think clearly) you would realize that *NOT REJECTING* >>>>>>>>>>>>>>> an input that does the opposite of whatever value >>>>>>>>>>>>>>> its decider returns *HAS ALWAYS BEEN COMPLETELY NUTS* >>>>>>>>>>>>>>>
Proof Theoretic Semantics inherently does this for >>>>>>>>>>>>>>> every aspect of any input that does not have a
finite back-chained sequence of inference steps
to valid closure.
DD simulated by HHH according to the semantics of >>>>>>>>>>>>>>> the C programming language cannot possibly reach >>>>>>>>>>>>>>> its own return instruction in any finite number
of steps. With PTS these inference steps are
THE WHOLE GAME. Absolutely nothing else is allowed >>>>>>>>>>>>>>> to be considered.
i don't need to insult you to point out the fact DD is a >>>>>>>>>>>>>> valid machine that halts when executed,
why do u think u need to insult me back when i point that >>>>>>>>>>>>>> out?
You keep changing the subject away from the
fact that DD has always been a bad input to
any halt decider.
i thought we agreed an HHH1 which is not named in DD could >>>>>>>>>>>> correctly decide on it...
Can Carol correctly answer “no” to this (yes/no) question? >>>>>>>>>>> E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf
yes i know that, truth can be defined relative to a reference >>>>>>>>>> point. same is true in physical too,
but u keep repeating on and on about bad input instead of >>>>>>>>>> explaining both perspectives at the same time
I don't allocate equal weight to falsehoods.
The HP counter-example input has always been
bad and the only reason this is not universally
understood is that sheeple herd together in
the conventional views.
no, turing's diagonal counter-example, the _original_ problem, >>>>>>>> is not a trivial program that produces no output.
it actually performs a computation and deciding on that
computation is an issue.
Any input that does the opposite of whatever value its
decider returns should have been rejected as bad input
is dead obvious.
the computation doesn't _try_ to contradict itself, it necessarily >>>>>> does it as an artifact of it's construction of applying the
decider to all input...
It is isomorphic to the Liar Paradox and the sheeple
is it not "isomorhpic" to the liar's paradox, it an infinitely
running computation that tests the entire enumeration of machines,
and in doing so stumbles on trying to decide on itself as either a
circular or circle-free machine, both of which are infinitely
running results.
the liar's paradox does no such thing even remotely
the circle-free paradox is not an intentional construction to
deceive a decider ... it just is a result of trying to universally
apply a true/ false circle-free decider to all machines, causing the
decider to fail on deciding itself.
I proved the HP input is the same as the Liar Paradox back in 2004
the circle-free problem found in turing's diagonals are not the same
thing as the halting problem, peter
Are claiming that all of the textbooks about the
halting problem are a complete misrepresentation this: https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf
My process is to start with the succinct essence of
enormously difficult analytical problems and then
spend decades boiling them down to their barest
possible essence.
This is the succinct essence that I started with. https://www.liarparadox.org/Peter_Linz_HP_317-320.pdf
The barest possible essence is that a proof theoretic
halt prover H rejects the HP counter-example input
D as meaningless. In PTS meaning is only acquired
through a finite sequence of inference steps. Infinite
sequences are rejected as ungrounded.
The above uses exactly standard PTS terminology
to the best of my current ability.
On 4/17/2026 1:54 AM, Mikko wrote:
On 16/04/2026 15:38, olcott wrote:
On 4/16/2026 3:20 AM, Mikko wrote:
On 15/04/2026 14:52, olcott wrote:
The first incompleteness theorem states that in
any consistent formal system F within which a
certain amount of arithmetic can be carried out,
there are statements of the language of F which
can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/
That's right. You did no not use the word "true" above so its
definition
is irrelevant to the first incompletness theorem.
Olcott's Minimal Type Theory
G ↔ ¬Prov[PA](⌜G⌝)
Directed Graph of evaluation sequence
00 ↔ 01 02
01 G
02 ¬ 03
03 Prov[PA] 04
04 Gödel_Number_of 01 // cycle
% This sentence cannot be proven in F
?- G = not(provable(F, G)).
G = not(provable(F, G)).
?- unify_with_occurs_check(G, not(provable(F, G))).
false.
The first incompleteness theorem sentence
has a cycle in the directed graph of its
evaluation sequence making it semantically
incoherent.
This kind of semantically incoherence is
foundational in proof theoretic semantics.
Nice to see that you don't disagree.
Gödel's G is merely semantically incoherent when
examined within the foundation of Proof Theoretic
Semantics.
A cycle is detected in the directed graphs of its
evaluation sequence proving that it does not represent
a well-founded justification tree.
| Sysop: | DaiTengu |
|---|---|
| Location: | Appleton, WI |
| Users: | 1,113 |
| Nodes: | 10 (0 / 10) |
| Uptime: | 492335:43:38 |
| Calls: | 14,238 |
| Files: | 186,312 |
| D/L today: |
3,558 files (1,159M bytes) |
| Messages: | 2,514,865 |