Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

Not one person on this forum ever gave me a fair and honest review

326 views
Skip to first unread message

olcott

unread,
Nov 28, 2022, 12:56:29 PM11/28/22
to
void D(void (*x)())
{
int Halt_Status = H(x, x);
if (Halt_Status)
HERE: goto HERE;
return;
}

int main()
{
D(D);
H(D, D);
}

The fact that no D(D) ever stops running unless H(D,D) aborts the
simlation of its input conclusively proves that the input to H(D,D)
specifies a non-halting sequence of configurations.

--
Copyright 2022 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

Richard Damon

unread,
Nov 28, 2022, 7:06:46 PM11/28/22
to
On 11/28/22 12:56 PM, olcott wrote:
> void D(void (*x)())
> {
>   int Halt_Status = H(x, x);
>   if (Halt_Status)
>     HERE: goto HERE;
>   return;
> }
>
> int main()
> {
>   D(D);
>   H(D, D);
> }
>
> The fact that no D(D) ever stops running unless H(D,D) aborts the
> simlation of its input conclusively proves that the input to H(D,D)
> specifies a non-halting sequence of configurations.
>


No, THIS D(D) will Halt even if THIS copy of H doesn't abort it.

(There is EXACTLY ONE D and ONE H presentd at a time).

It will halt because the copy of H that it calls WILL abort is
simulation of the copy of the input it is given. Those are different
copies of the supposed program H, and have the exact code that you
define the H that gives the answer to have.

Note, to SHOW that "Unless" you need to change JUST the outer H that
main calls, without changing the H that D calls, as that is what that
word mean in this context.

Otherwise you are just the despicable liar for talking about the
behavior of a "non-input", as the input D needs to remain calling the H
that it was defined to call, which is the H that returns the answer.

Your problem is that you have entangled two independent programs to the
point that they are no longer independent.

It is not possible to create an INDEPENDENT program H that you give as
an input an INDEPENDET program D for it to decide on.

Neither your subroutine H or subroutine D end up being actual
"Computations" or "Algiortiths applied to an input" per the definitions
of Computation Theory, so neither of them end up being independently the
equivalent of a Turing Machine.

That is why you fail. You just don't understand the basics of the problem.

You are just proving your ignorance of the material. The fact that you
try to bring in "Sets" when there are none in the problem just shows this.

olcott

unread,
Nov 29, 2022, 11:35:33 AM11/29/22
to
On 11/28/2022 11:56 AM, olcott wrote:
> void D(void (*x)())
> {
>   int Halt_Status = H(x, x);
>   if (Halt_Status)
>     HERE: goto HERE;
>   return;
> }
>
> int main()
> {
>   D(D);
>   H(D, D);
> }
>
> The fact that no D(D) ever stops running unless H(D,D) aborts the
> simlation of its input conclusively proves that the input to H(D,D)
> specifies a non-halting sequence of configurations.
>

[Ignoring stack overflow]

The above D(D) never stops running unless the H(D,D) that it invokes
aborts the simulation of its input.

D(D) correctly simulated by the above H(D,D) never stops running unless
aborted.

Thus no D(D) ever stops running unless an H(D,D) aborts the simulation
of its input.

This conclusively proves that the input to H(D,D) specifies a

Richard Damon

unread,
Nov 29, 2022, 6:47:18 PM11/29/22
to
On 11/29/22 11:35 AM, olcott wrote:
> On 11/28/2022 11:56 AM, olcott wrote:
>> void D(void (*x)())
>> {
>>    int Halt_Status = H(x, x);
>>    if (Halt_Status)
>>      HERE: goto HERE;
>>    return;
>> }
>>
>> int main()
>> {
>>    D(D);
>>    H(D, D);
>> }
>>
>> The fact that no D(D) ever stops running unless H(D,D) aborts the
>> simlation of its input conclusively proves that the input to H(D,D)
>> specifies a non-halting sequence of configurations.
>>
>
> [Ignoring stack overflow]
>
> The above D(D) never stops running unless the H(D,D) that it invokes
> aborts the simulation of its input.

Right, but that is ok, and doesn't make that D non-halting by the
DEFINITION of what a Halt Decider needs to ddcide.

H(M,x) needs to return Halting if M(x) Halts.

Since D(D) halts, this means that H(D,D) needs to return Halting.

Nothing in that ask anything about D using a simulation that happens to
be aborted.

You are just using wrong definitions.

>
> D(D) correctly simulated by the above H(D,D) never stops running unless
> aborted.

Nope, UTM(D,D) which is the DEFINITION of a "Correct Simulation" will
Halt. Thus the "Correct Simulation" of this input WILL HALT.

The H you have provided never does a correct wsimulation, so what it
does is actually irrelevent.

>
> Thus no D(D) ever stops running unless an H(D,D) aborts the simulation
> of its input.

Nope, since the H(D,D) that D calls DOES abort its simulation, the
H(D,D) simulating this D didn't actually NEED to abort its simulation,
as the UTM simulation shows, so it did so incorrectly.

You can't use "unless" to ask about something that is fixed in the
input, only about THIS instance of H.

You just don't understand what "input" or "Turing Machine" mean.


>
> This conclusively proves that the input to H(D,D) specifies a
> non-halting sequence of configurations.
>
>

Nope, it proves you don't understand the meaning of the words you are
using, and that you aren't actually working on the halting problem due
to that error.

Thus you have wasted the last 18 year of your life (or is it 19 yet)
because you made yourself INTENTIONALLY IGNORANT of what you actually
needed to know to do the problem.

olcott

unread,
Nov 29, 2022, 7:52:26 PM11/29/22
to
You are not paying close enough attention to the exact words that I just
said.

If No H(D,D) in the universe ever stops simulating its input then no
corresponding executed or simulated D(D) in the universe ever stops
running.

Richard Damon

unread,
Nov 29, 2022, 8:48:26 PM11/29/22
to
So, you are just PROVING that you are not working on the Halting
Problem, because that isn't the Halting Problem criteria.

The Halting Problem is that H(M,x) must return Halting if M(x) Halts and
Non-Halting if M(x) will NEVER halt even after an unbounded number of steps.

D(D) Does Halt if the H it is built on returns Non-Halting for H(D,D),
so that answer can NOT be correct. PERIOD.

The fact that you can not construct any H by your template that can
simulate the D built on it to a final state is NOT a restatement of that
statement. YOU FAIL.

That, or you are just stating the fact that you can't actually build a
Halting Decider that can correctly answer for H(D,D) for the D built
from it per the Linz template.

You are also proving that you are ignorant of what these things are
actually about, because you keep on LYING by insisting that you are
working on it.

You are shown to be DECEPTIVE, as you keep on adding and removing the
"by H".

Note, we don't care about "Any" H(D,D), we care about the SPEICIFIC
H(D,D) that is claimed to get the right answer about the D built on IT.

Note, that for THAT H, the way you have currently defined it, then the
correctly simulated or executed D(D) does Halt. You just get confuse
because that H doesn't do a correct simuation, so you look at a
DIFFERENT H and a DIFFERENT D where H does a correct simulaition, but of
the WRONG D, and shows the correct answer for that OTHER D, but never
gives it, so it fails.

Your confusion just proves that you don't understand what a Turing
Machine actually is, or what a Program actually is, or how computers
actually work.

You are just showing the word how bad you grasp of logic is, and how
little you understand. You have destroyed what little reputation you
might have had by your instance on things that aren't actually what you
are trying to claim about.

olcott

unread,
Nov 29, 2022, 9:30:10 PM11/29/22
to
I have already shown that people having a much deeper understanding than
the mere rote memorization of textbooks understand that my adaptation of
the halt status criteria is equivalent to the conventional notions.

Richard Damon

unread,
Nov 29, 2022, 9:54:38 PM11/29/22
to
Nope. You are perhaps DECEIVED them into giving assent to a statement
whixh appears to match the actual definition but doesn't with your
unusual meaning of the words.

Note, your CLAIM they are actually eqivalent means you thing that D(D)
Halting means it is correct to say it is non-halting.

That shows that YOUR logic system has gone inconsistent and is TOTALLLY
WORTHLESS.

Your failure to understand that means you are totally ignorant of how
logic works or are just a pahtological liar.

You failure to see this just proves your stupidity.

You claim of "Equivalence" is EXACTLY like saying 1 == 2 or True == FALSE.

You have failed but seem to be too stupid to understand it.

olcott

unread,
Nov 29, 2022, 10:29:58 PM11/29/22
to
He has written a textbook on the subject and many many papers,
It is ridiculous to believe that:
(a) He could be fooled into agreeing with a statement that he
did not fully understand.
AND
(b) Give me permission to quote his agreement with this statement.

I do not believe that Ben believed that he was fooled when Ben made the
claim that he was fooled. Ben knows better than this. Ben simply ran out
of options for rebuttal and thus grasped at straws.

Richard Damon

unread,
Nov 29, 2022, 11:03:07 PM11/29/22
to
Right, and he agreed that if H shows that the CORRECT SIMULATION of its
input is non-halting, which is the simulation by a UTM. H only does a
correct simulaition if its simulation agrees with THAT simulation.

Since UTM(D,D) will halt if H(D,D) returns 0, your H can NOT "correctly
determine" that ANY correct simulation, let alone its own, would not
reach a final state, so you don't have a basis to make your claim of
correctly determine.

YOU make the INCORRECGT leap from "Correct Simulation" (which to someone
in the field implies COMPLETE, ala the simulation of an actual UTM) to a
PARTIAL simulation that H does.

When you interprete the statement you gave with the understanding that
"Correct Simulation" will be taken to mean the exact simulation of a
UTM, you can see what he was agreeing to.

Remember, you SPECIFICALLY have pointed out that was the exact and
complete statement he was agreeing to, it did NOT include your perverse
logic that tries to justify that a PARTIAL simulation by H not reaching
an end state is also sufficient to show non-halting, because that just
doesn't fit the ACTUAL definition of the words as used in the field.

Correct doesn't mean correct as far as it goes, it means correct and
going to the end.

WRONG DEFINITION -> WRONG CONCLUSIONS.

YOU FAIL.



olcott

unread,
Nov 29, 2022, 11:38:08 PM11/29/22
to
I am only willing to have a mutually honest dialogue.

When I prove that you are incorrect on a point you never acknowledge
that I proved that you are incorrect you simply change the subject.

Acknowledge that he was not fooled and that he most likely fully
understood what he agreed to or we cannot move on to the next point.

Richard Damon

unread,
Nov 30, 2022, 7:01:09 AM11/30/22
to
I'm AM being Honest.

> When I prove that you are incorrect on a point you never acknowledge
> that I proved that you are incorrect you simply change the subject.

Except that you never have proven me wrong on any major point.

>
> Acknowledge that he was not fooled and that he most likely fully
> understood what he agreed to or we cannot move on to the next point.
>

"Fooled" may be a stronger word then needed. He does not interpret the
words the way you do. This is in part due to your enforced IGNORANCE of
the subject.

As I said, to HIM, "CORRECT SIMULATION" means a COMPLETE SIMULATION,
like a UTM, that WILL match the behavior of the direct exectution of
that input.

Since D(D) will Halt since H(D,D) returns 0, any "Correct Simulation" of
the input to H(D,D) will be Halting.

Thus, IF H can correctly determine that its correct simulation of the
input would never halt can only be true if the direct exectution of THAT
input, exactly as it is, would not halt. Not the input built on a
DIFFERENT H that actually DOES a correct simulation, but THIS input,
built on the H that DOES abott its simulation and return 0.

You are just showing that you don't know the meaning of the basic words,
and thus incorrectly, and deceptively (at least to yourself) twist the
meaning so you don't really understand what they mean to people how
understand the materiaal.

Note, you like using the term "Learned by Rote". Well, statements
"Learned by rote" tend to be statements that are accepted true.

Until you can show where they are incorrect in this case, siteing other
accepted statements, CORRECTLY interpreted, you can't dismiss them as
just "Learned by rote".

Note also, I do NOT "learn by rote", and in fact, have a slight
disability that I have a very hard time "learning by rote". I need to
know WHY something works and understand the basic princples, and then I
can remember it.

Your problem seems to be that you never learned the material in the
first place, but are working in a universe where you are GUESSING as to
what things mean, and thus since you don't actually KNOW what people are
talking about with statements, you get things wrong.

Your talk of "First Principles" is off, "First Principles" is a method
where you START by LEARNING the actual fundamentals, and learning them
welll. Then you move forward using those basics and try to not rest on
the directions that others took in deciding how to Engineer a solution
to the problem.

It needs the study of the actual First Principles, or it becomes just an
exercise in fantasy.

That is what you have done, you didn't learn the basic principles, and
are just repeating the errors of a century ago. You have refused to
learn from History, and are repeating it.

olcott

unread,
Nov 30, 2022, 9:38:06 AM11/30/22
to
Until you acknowledge that you were wrong and he was not fooled at all
we cannot proceed.

Richard Damon

unread,
Nov 30, 2022, 7:09:23 PM11/30/22
to
No, untill YOU acknowledge that you don't understand the actual meaning
of the words, in context, that you have been using, you are just going
to continue to show your stupidity.

Remember, To Prof Sipser, "Correct Simulation" means a Complete and
Correct Simulation, just like a UTM.

Since even you admit that D(D) returns when H(D,D) answers 0, this means
that since you are claiming your "correct H" does answer 0, then the
D(D) of this problem Halts, and thuis the ONLY possible results of a
"Correct Simulation" of the input to H(D,D) is Halting, so it is
IMPOSSIBLE for H to "Correct Determine that a Correct Simulaiton of its
input would be non-halting". This applies whether you restrict that
correct simulation to being by H or not.

Thus, your arguement FAILS.

Yes, if H COULD prove that, it would be correct, because that means that
the D given it must have been some other machine that doesn't halt, but
your proof stipulates that it IS the machine that was described in his
proof, which DOES call the H that is claimed to be correct, and which by
your stipulation DOES abort its simulaition and return 0.

Thus, your H can NOT prove the needed condition, so its aborting is
proved to be in error.

Your problem seems to be that you just don't know what any of the
important words actually mean.

You are just continuing to mount the evidence of your own ignorance and
stupidity.

olcott

unread,
Nov 30, 2022, 7:30:01 PM11/30/22
to
OK so you don't want to talk anymore, that is fine with me.

Richard Damon

unread,
Nov 30, 2022, 8:00:31 PM11/30/22
to
I will point out that I have nothing to prove, as the Halting Theory, as
proved, is on my side.

Everything I have said, is just a restating of the accepted Truth.

You, on the other hand, are making a significant claim, and need to
actually PROVE your position with mathematical rigor, which you haven't
done, and I th9nk you know it (otherwise you would be writing and trying
to publishing the paper).

As long as there are unresolved rebutalls to your "claims", you really
can't say you have proved your point.

You may think to your self that you have proved things, but you know
that no one actually belives you.

Thus, YOU are the one that needs to move on, and it seems that I am one
of the few that will actually engage you.

Its fine with me if you just decide to disappear and give up on the subject.

olcott

unread,
Nov 30, 2022, 8:07:43 PM11/30/22
to
You refuse to acknowledge any of the points where I am proved to be
correct because you (as everyone else here) are only interested in
rebuttal, thus have no interest what-so-ever in an honest dialogue.

This is intolerable.

Richard Damon

unread,
Nov 30, 2022, 8:29:17 PM11/30/22
to
Becausse you HAVEN'T proved them, because you just don't understand what
you are talking about. If you start with incorrect definitions, you just
can't get anywhere.

I am interested in TRUTH, so when you state error, I wll rebut it.

YOU are the one not interested in a Honest dialogue, it appears because
you just don't kow how to be HONEST.

Your problem is that it seems that you INTENTIONALLY refused to learn
the basics, so you have nothing to work with to establish what you want
to show.

This just shows your own STUPIDITY.

olcott

unread,
Nov 30, 2022, 8:35:00 PM11/30/22
to
Until you acknowledge that you were wrong and he was never fooled you
will get no more words from me.

Richard Damon

unread,
Nov 30, 2022, 9:08:15 PM11/30/22
to
So, you aren't reading?

I ppointed out that "fooled" may be not quite the right word, as it
isn't so much you "tricked" him into agreeing to a false statement, but
that you don't understand the statement that you wrote, because you
don't understand the basics of the language of the field.

Yes, the statement is "correct" when interpreted by the actual
contextual meaning of the words, where "correctly simulated" means
showing the behavior of the direct execution of the program, which is
what it DOES mean in the field.

YOU are the one "Fooled", and you did it to yourself.

Sorry, you are just making yourself into a laughing stock as you reveal
how "dumb" you are.

Any reputable journal that in checking on things finds these threads is
just going to trash can your paper, as you have so discredited your
reputation.

olcott

unread,
Dec 1, 2022, 12:43:07 AM12/1/22
to
You must specifically admit that your were wrong.

> Yes, the statement is "correct" when interpreted by the actual
> contextual meaning of the words,

That is progress.

> where "correctly simulated" means
> showing the behavior of the direct execution of the program, which is
> what it DOES mean in the field.
>
> YOU are the one "Fooled", and you did it to yourself.
>
> Sorry, you are just making yourself into a laughing stock as you reveal
> how "dumb" you are.
>
> Any reputable journal that in checking on things finds these threads is
> just going to trash can your paper, as you have so discredited your
> reputation.

Richard Damon

unread,
Dec 1, 2022, 6:46:05 AM12/1/22
to
Since I am not, that won't happen.

YOU need to specifically admit that you are, and always have been, WRONG.
>
>> Yes, the statement is "correct" when interpreted by the actual
>> contextual meaning of the words,
>
> That is progress.

If you think so.

You still don't understand what he sees that statement to mean, so you
are no closer to proving your version.

olcott

unread,
Dec 1, 2022, 10:40:38 AM12/1/22
to
Acknowledge that [you were wrong when you said] he was fooled or we
cannot move on to the next point.

You must say this words: "I was wrong when I said he was fooled."

> YOU need to specifically admit that you are, and always have been, WRONG.
>>
>>> Yes, the statement is "correct" when interpreted by the actual
>>> contextual meaning of the words,
>>
>> That is progress.
>
> If you think so.
>
> You still don't understand what he sees that statement to mean, so you
> are no closer to proving your version.

If you cannot admit your mistakes then you have not shown that you will
commit to an honest dialogue. I am not willing to tolerate anything
besides an honest dialogue.

>
>>
>>> where "correctly simulated" means showing the behavior of the direct
>>> execution of the program, which is what it DOES mean in the field.
>>>
>>> YOU are the one "Fooled", and you did it to yourself.
>>>
>>> Sorry, you are just making yourself into a laughing stock as you
>>> reveal how "dumb" you are.
>>>
>>> Any reputable journal that in checking on things finds these threads
>>> is just going to trash can your paper, as you have so discredited
>>> your reputation.
>>
>

Richard Damon

unread,
Dec 1, 2022, 6:34:11 PM12/1/22
to
No, because in a real sense he was, because you use a deceptive statment
which you take to mean something that he doesn't.

>
>> YOU need to specifically admit that you are, and always have been, WRONG.
>>>
>>>> Yes, the statement is "correct" when interpreted by the actual
>>>> contextual meaning of the words,
>>>
>>> That is progress.
>>
>> If you think so.
>>
>> You still don't understand what he sees that statement to mean, so you
>> are no closer to proving your version.
>
> If you cannot admit your mistakes then you have not shown that you will
> commit to an honest dialogue. I am not willing to tolerate anything
> besides an honest dialogue.

BUT I AM NOT THE ONE WHO HAS MADE A MISTAKE.

THAT IS YOUR PROBLEM, becaue you don't know the meaning of the words.

If you point out exactly where I am wrong with my explaination, and can
point out an actual reliable source to back it up, maybe you can try to
convince me.

So try to show that my explation of what HE would mean by the statement
isn't what he would take it to mean, or how that is actually compatible
with your meaning.

Remember, the key point is that to people in the field, "Correct
Simulation" mean corresponding the the actual FULL run of the actual
machine with that EXACT input, which even you have agreed Halts.

You claim it somehow can be match with something that says non-halting.
THAT is a LIE.

Your refusal to see that, shows you are just STUPID.

You have never shown that your interpreation has ANY merit by the
definitions of the field, and in fact point that out by trying to use
definitions of basically unrelated fields.

I will note that "Software Engineering" is a VERY different subject that
Computation Theory, looking at VERY different sorts of problems.

You don't seem to understand that, because you are too stupid.

olcott

unread,
Dec 1, 2022, 7:37:07 PM12/1/22
to
Even if this is true that would not be any evidence at all that he was
deceived. Because you already know this you have sufficiently proven
that you are not interested in an honest dialogue.

olcott

unread,
Dec 1, 2022, 7:43:19 PM12/1/22
to
Even if this is true [AND IT IS NOT TRUE**] that would not be any
evidence at all that he was deceived. Because you already know this you
have sufficiently proven that you are not interested in an honest dialogue.

** A CORRECT SIMULATION IS A WELL DEFINED CONCEPT

Richard Damon

unread,
Dec 1, 2022, 9:43:11 PM12/1/22
to
No, the fact that you refuse to accept the truth shows that you do not
understand what truth IS.

You are showing your STUPIDITY.

>
> ** A CORRECT SIMULATION IS A WELL DEFINED CONCEPT
>

Right, and in compuation theory it means a simultion that exactly
reproduces the results of a (complete) direct execution of the program
being simulated.

"Partially but correct so far" may be considered correct in some
contexts, but not in many.

Have you correctly assembled a puzzle that you have only put together
10% of the pieces, even if every piece you have put together is
correctly conneted?

Have your correctly done an exam (worthy of a grade of 100%) if you did
1 problem out of 10, even if you got that one problem exactly right.

NO.

In the same manner, a partial simulation, even if correct in all the
steps it has done, is not generally considered to be a "Correct
Simulation". It is a Correct Partial Simulation, or you can use other
words that include the indication that it was not to completion.

Your failure to understand shows your ignorance of the subject.

olcott

unread,
Dec 1, 2022, 9:51:50 PM12/1/22
to
What does this have to do with me fooling him?

You were wrong when you said he was fooled and you failed to flatly
admit that you were wrong thus proving that honesty is not your policy.

Richard Damon

unread,
Dec 1, 2022, 10:38:14 PM12/1/22
to
Because you have claimed he was agreeing to your "partial simulaiton is
a correct simulation" by agreeing with your statement.

As I have said, the statement he THOUGHT he as agreeing to was based on
"Correct Simulation" being defined as per UTM COMPLETE Simulation.

You are claiming that his agreemeent makes your partial simulation are
correct simulation logic correct.

Thus, you "Fooled" him by getting him to agree to an ambiguous statement
that you are then using "against" him to say he is agreeing to a
statement, whose meaning he doesn't actually agree with.


You still don't understand that I have admitted "fooled" is probably
slightly to extream of a word, but I guess you just don't understande
even convestaional Englist, do you.

You are just proving how stupid and childish you are.

You have destroyed your reputation, and will be remembered for being the
ignoramous you have showed yourself to be.

Skep Dick

unread,
Dec 2, 2022, 3:39:02 AM12/2/22
to
On Friday, 2 December 2022 at 04:51:50 UTC+2, olcott wrote:
> blah blah blah

Olcott, how long did your doctor give you?

Just trying to figure out when the spam stops.

Skep Dick

unread,
Dec 2, 2022, 3:51:30 AM12/2/22
to
On Friday, 2 December 2022 at 05:38:14 UTC+2, richar...@gmail.com wrote:
> You have destroyed your reputation, and will be remembered for being the
> ignoramous you have showed yourself to be.

Hey moron! You still haven't figured out that the entire debate is literally about assigning meaning to function outputs?

ANY function (human; or a C program) will produce whatever output it produces.

Olcott is trolling you hard on the fact that you have (somehow) decided that the answer is "correct"; or "incorrect". As if you have an authoritative decision procedure on "correctness"




Skep Dick

unread,
Dec 2, 2022, 4:28:26 AM12/2/22
to
On Friday, 2 December 2022 at 04:43:11 UTC+2, richar...@gmail.com wrote:
> Right, and in compuation theory it means a simultion that exactly
> reproduces the results of a (complete) direct execution of the program
> being simulated.

So what is the complete result of the direct execution of this Ruby program?

def f:
loop {}
return 1
end

Whatever answer you give to the above: please provide the algorithm which obtained the answer.
And specifically - if you your answer is "the program doesn't halt" - please provide the halting decider which produced the answer.

Richard Damon

unread,
Dec 2, 2022, 7:28:01 AM12/2/22
to
On 12/2/22 3:51 AM, Skep Dick wrote:
> On Friday, 2 December 2022 at 05:38:14 UTC+2, richar...@gmail.com wrote:
>> You have destroyed your reputation, and will be remembered for being the
>> ignoramous you have showed yourself to be.
>
> Hey moron! You still haven't figured out that the entire debate is literally about assigning meaning to function outputs?

The problem is we are in a domain that is fully defined on this point,
and the possible answer of H have strictly defined meanings.

Olcott seem to think that this specific H can sometimes give one answer
and sometimes another.

>
> ANY function (human; or a C program) will produce whatever output it produces.

Right, and the answer that H produces doesn't match the answer required
by the problem statement, so is wrong.

>
> Olcott is trolling you hard on the fact that you have (somehow) decided that the answer is "correct"; or "incorrect". As if you have an authoritative decision procedure on "correctness"
>

Because the answer from a Halt Decider IS either correct or incorrect
since it IS a pure "Binary" decision, that always has a answer.


Message has been deleted

Skep Dick

unread,
Dec 2, 2022, 7:49:00 AM12/2/22
to
On Friday, 2 December 2022 at 14:28:01 UTC+2, richar...@gmail.com wrote:
> The problem is we are in a domain that is fully defined on this point,
> and the possible answer of H have strictly defined meanings.
If that were true then your formal system is necessarily complete.

> Olcott seem to think that this specific H can sometimes give one answer
> and sometimes another.
It's not a matter of what anyone thinks. Indeed, any specific H could be non-deterministic.

> Right, and the answer that H produces doesn't match the answer required
> by the problem statement, so is wrong.
If you know what answer is required by the problem-statement why are you even asking H?

You already know the answer - just produce it.

> Because the answer from a Halt Decider IS either correct or incorrect
> since it IS a pure "Binary" decision, that always has a answer.
This is incoherent. The Halt Decider returns whatever it returns.

Given program A - it returns True (halts)
Given program B - it returns False (it doesn't halt).

HOW do you know that "A halts" is a correct statement?
HOW do you know that "B doesn't halt" is a correct statement?

If you are disputing the results of H then not only are you implying that you also have a halt-decider; but you are implying that your halt-decider is disagrees with H and THEREFORE H is incorrect.

Richard Damon

unread,
Dec 2, 2022, 8:01:55 AM12/2/22
to
On 12/2/22 7:40 AM, Todor Genov wrote:
> On Friday, 2 December 2022 at 14:28:01 UTC+2, richar...@gmail.com wrote:
>> The problem is we are in a domain that is fully defined on this point,
>> and the possible answer of H have strictly defined meanings.
> If that were true then your formal system is necessarily complete.
>

No, completenes is about the PROVABILITY of statement. A statement can
be known to have a correct answer, but we can not actually know that answer.

>> Olcott seem to think that this specific H can sometimes give one answer
>> and sometimes another.
> It's not a matter of what anyone thinks. Indeed, any specific H could be non-deterministic.

Not an be a Turing Machine Equivalent.

>
>> Right, and the answer that H produces doesn't match the answer required
>> by the problem statement, so is wrong.
> If you know what answer is required by the problem-statement why are you even asking H?

So, you don't understand that problem either.

>
> You already know the answer - just produce it.

The problem is H needs to produce it, but can't

>
>> Because the answer from a Halt Decider IS either correct or incorrect
>> since it IS a pure "Binary" decision, that always has a answer.
> This is incoherent. The Halt Decider returns whatever it returns.
>
> Given program A - it returns True (halts)
> Given program B - it returns False (it doesn't halt).
>
> HOW do you know that "A halts" is a correct statement?
> HOW do you know that "B doesn't halt" is a correct statement?

A program that halts, can always be proven to halt by just running it
till it reaches that final step.

For programs that don't halt, we can often actually PROVE that they
don't, but not for all cases. That is actually one way to show the
Halting Problem.

Note, it is possible for us to not know if the answer from H is correct
or incorrect.

If H answers Halting, and it is correct, we can prove it correct by just
running the input program.

If H answers Halting, and that is incorrect, we MIGHT be able to prove
it wrong, if this is a case that we can prove to be non-halting.

If H answers Non-Halting, and that is incorrect, we can prove it wrong
by running the input and seeing it halt (as we do in the case in question).

If H answers Non-Halting, and that is correct, we MIGHT be able to prove
it right, or we might not.

This shows the difference between PROVING something is correct or
incorrect or it actually being correct or incorrect.

A binary, but non-computable, answer WILL be either correct or
incorrect, but we might not know which it is in a given case.

>
> If you are disputing the results of H then not only are you implying that you also have a halt-decider; but you are implying that your halt-decider is disagrees with H and THEREFORE H is incorrect.
>
>

No, we can show that THIS program WILL halt if H returns non-halting, so
we can prove that this H gave the wrong answer.

For the original proof, we can also prove that the H^ program WILL be
non-halting if the H is shown to return Halting for H applied to H^ H^,
in part because the final state of H^ is exactly the code step for the
final state of H that says Halting.

The only way we can't show the halting behavior of this H^ is it we
don't know if H gives an answer, but to be a Halt Decider it MUST give
an answer, so we can actually PROVE that IF it gives an answer, it is
wrong, and if it doesn't give an answer, then it is also wrong by
definition.

Halting is a property which obeys the law of the excluded middle, so we
have shown that H must be wrong.

To disprove a machine from being a Halt Decider, since that requires
being able to answer correctly about EVERY input, we only need to show
it wrong about one. There may be many other answers we can't determine
if it is right or wrong, but if we can show it wrong about one, it is wrong.

The H^ template has the special property that we can show that H WILL be
wrong (either by giving the wrong answer or by not answering) for any
possible decider H we build it on, because it uses a copy of that
decider to ask it the same question. This lets us prove that ALL
machines that might claim to be halt deciders have to be wrong about a
specific program built from them.

Richard Damon

unread,
Dec 2, 2022, 8:02:54 AM12/2/22
to
So, did you just break your "Secret Identity"?

Skep Dick

unread,
Dec 2, 2022, 8:49:57 AM12/2/22
to
On Friday, 2 December 2022 at 15:01:55 UTC+2, richar...@gmail.com wrote:
> No, completenes is about the PROVABILITY of statement.
>A statement can be known to have a correct answer, but we can not actually know that answer.
It's the exact same thing.

If you can't prove whether a **particular** answer is "correct" then your system is incomplete with respect to "correctness"!

What the hell does it mean for the statement "2+2" to have a correct answer if you can't actually determine whether 4 is a "correct" answer?

> >> Olcott seem to think that this specific H can sometimes give one answer
> >> and sometimes another.
> > It's not a matter of what anyone thinks. Indeed, any specific H could be non-deterministic.
> Not an be a Turing Machine Equivalent.
Nonsense. Deterministic and non-deterministic Turing Machines are sub-types of Turing Machines.

> So, you don't understand that problem either.
There's nothing to understand. You ask a question (2+2) - some function produces an answer (4).

The answer "4" is either correct or incorrect. Which one is it?

> > You already know the answer - just produce it.
> The problem is H needs to produce it, but can't
That's a lie. H produces an answer.

The answer H produces is either correct or incorrect. Which one is it?

> A program that halts, can always be proven to halt by just running it
> till it reaches that final step.
This is incoherent. a Proof IS a program. A proof either halts; or it doesn't.

> For programs that don't halt, we can often actually PROVE that they
> don't, but not for all cases. That is actually one way to show the
> Halting Problem.
Incoherent nonsense. How do you prove that a program halts when a proof is a program?

How do you prove that a proof halts?

> Note, it is possible for us to not know if the answer from H is correct
> or incorrect.
How do you know? Surely you must have some method in mind by which you can prove that an answer is "correct" or "incorrect"?

Provide it please.

> If H answers Halting, and it is correct, we can prove it correct by just
> running the input program.
Huh?!? How? Any running program could halt. Eventually.

If P hasn't yet halted but could in future WHEN do you assert that H was "incorrect" ?

> If H answers Halting, and that is incorrect, we MIGHT be able to prove
> it wrong, if this is a case that we can prove to be non-halting.
Huh?!? How? Proofs are programs.

What sort of program are you going to write which proves that another program halts?

> If H answers Non-Halting, and that is incorrect, we can prove it wrong
> by running the input and seeing it halt (as we do in the case in question).
But you would be doing EXACTLY what H did!?!?

It ran/simulated the program! How is your runner/simulator better than H's runner/simulator?

> If H answers Non-Halting, and that is correct, we MIGHT be able to prove
> it right, or we might not.
Huh?!? How?!? Proofs are programs.

What sort of program (other than H) would you produce to prove that another program doesn't halt?

> This shows the difference between PROVING something is correct or
> incorrect or it actually being correct or incorrect.
No, this shows sophistry. Proofs are programs.

If program A proves that program B is correct, you still have no proof that program A is correct about program B being correct.

> A binary, but non-computable, answer WILL be either correct or
> incorrect, but we might not know which it is in a given case.
You are equivocating "knowing".

How would you know whether an answer is "correct" in the cases where you can know?

> No, we can show that THIS program WILL halt....
How? Surely you have to run/simulate THIS program.

When you run/simulate THIS program - you are doing EXACTLY the same thing as the simulating halt-decider.

> we can prove that this H gave the wrong answer.
Oh, you can prove it. Can you? Proofs are programs.

Since you are volunteering a proof - please provide a program/proof which correctly determines that H is incorrect.

> For the original proof
In what programming language are you going to present this "proof"?

>we can also prove that the H^ program WILL be non-halting if the H is shown to return Halting for H applied to H^ H^
In what programming language are you going to present this "proof"?

>so we can actually PROVE that IF it gives an answer
In what programming language can we PROVE this?

> Halting is a property which obeys the law of the excluded middle, so we
> have shown that H must be wrong.
This is immaterial. Since both "halting" and "wrongness" are both non-trivial semantic properties subject to Rice's theorem.


> To disprove a machine from being a Halt Decider, since that requires
In what programming language are you going to disprove this?

> This lets us prove that ALL machines that might claim to be halt deciders have to be wrong about a specific program built from them.
What programming language lets you prove that?

Surely you are aware that you are guilty of equivocation? SURELY? Unless, of course you are not a logician.

Because you keep equivocating the term "proof", "to prove" and "program".
Proofs are not LIKE programs. Proofs are not related to programs but different.
Proofs ARE programs. They are two different words for exactly the same objects.

https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence



olcott

unread,
Dec 2, 2022, 10:54:32 AM12/2/22
to
On 12/2/2022 7:49 AM, Skep Dick wrote:
> On Friday, 2 December 2022 at 15:01:55 UTC+2, richar...@gmail.com wrote:
>> No, completenes is about the PROVABILITY of statement.
>> A statement can be known to have a correct answer, but we can not actually know that answer.
> It's the exact same thing.
>
> If you can't prove whether a **particular** answer is "correct" then your system is incomplete with respect to "correctness"!
>
> What the hell does it mean for the statement "2+2" to have a correct answer if you can't actually determine whether 4 is a "correct" answer?
>
>>>> Olcott seem to think that this specific H can sometimes give one answer
>>>> and sometimes another.
>>> It's not a matter of what anyone thinks. Indeed, any specific H could be non-deterministic.
>> Not an be a Turing Machine Equivalent.
> Nonsense. Deterministic and non-deterministic Turing Machines are sub-types of Turing Machines.
>
>> So, you don't understand that problem either.
> There's nothing to understand. You ask a question (2+2) - some function produces an answer (4).
>
> The answer "4" is either correct or incorrect. Which one is it?
>
>>> You already know the answer - just produce it.
>> The problem is H needs to produce it, but can't
> That's a lie. H produces an answer.
>
> The answer H produces is either correct or incorrect. Which one is it?

https://liarparadox.org/2022_11_14.zip

The H(D,D) of the above fully operational software system
correctly determines that its input specifies a non-halting
sequence of configurations according to this criteria:

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.

*Correct simulation of D by H* is defined as a line-by-line
mapping from the x86 source code of D to each line of the
execution trace of D.

Only a diverge of this mapping shows that the simulation is
incorrect, it is otherwise correct even if incomplete.

_D()
[000019b3] 55 push ebp
[000019b4] 8bec mov ebp,esp
[000019b6] 51 push ecx
[000019b7] 8b4508 mov eax,[ebp+08]
[000019ba] 50 push eax
[000019bb] 8b4d08 mov ecx,[ebp+08]
[000019be] 51 push ecx
[000019bf] e8bff9ffff call 00001383
[000019c4] 83c408 add esp,+08
[000019c7] 8945fc mov [ebp-04],eax
[000019ca] 837dfc00 cmp dword [ebp-04],+00
[000019ce] 7402 jz 000019d2
[000019d0] ebfe jmp 000019d0
[000019d2] 8be5 mov esp,ebp
[000019d4] 5d pop ebp
[000019d5] c3 ret
Size in bytes:(0035) [000019d5]

_main()
[000019e3] 55 push ebp
[000019e4] 8bec mov ebp,esp
[000019e6] 68b3190000 push 000019b3 // push D
[000019eb] 68b3190000 push 000019b3 // push D
[000019f0] e88ef9ffff call 00001383 // call H
[000019f5] 83c408 add esp,+08
[000019f8] 33c0 xor eax,eax
[000019fa] 5d pop ebp
[000019fb] c3 ret
Size in bytes:(0025) [000019fb]

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
[000019e3][00102a39][00000000] 55 push ebp // begin main
[000019e4][00102a39][00000000] 8bec mov ebp,esp
[000019e6][00102a35][000019b3] 68b3190000 push 000019b3 // push D
[000019eb][00102a31][000019b3] 68b3190000 push 000019b3 // push D
[000019f0][00102a2d][000019f5] e88ef9ffff call 00001383 // call H

When H correctly simulates D it finds that D remains stuck in recursive
simulation

H: Begin Simulation Execution Trace Stored at:112ae5
Address_of_H:1383
[000019b3][00112ad1][00112ad5] 55 push ebp // begin D
[000019b4][00112ad1][00112ad5] 8bec mov ebp,esp
[000019b6][00112acd][00102aa1] 51 push ecx
[000019b7][00112acd][00102aa1] 8b4508 mov eax,[ebp+08]
[000019ba][00112ac9][000019b3] 50 push eax // call D
[000019bb][00112ac9][000019b3] 8b4d08 mov ecx,[ebp+08]
[000019be][00112ac5][000019b3] 51 push ecx // push D
[000019bf][00112ac1][000019c4] e8bff9ffff call 00001383 // call H
H: Infinitely Recursive Simulation Detected Simulation Stopped

We can see that the first seven instructions of D simulated by H
precisely match the first seven instructions of the x86 source-code of
D. This conclusively proves that these instructions were simulated
correctly.

Skep Dick

unread,
Dec 2, 2022, 11:04:00 AM12/2/22
to
Shut up, Olcott.

Everything you've done so far is one giant, pointless tautology.

It's an argument from authority. Your H(D,D) function is the authority you've appointed to decide the "correctness" property.

Skep Dick

unread,
Dec 2, 2022, 11:21:15 AM12/2/22
to
On Friday, 2 December 2022 at 17:54:32 UTC+2, olcott wrote:
> This conclusively proves that these instructions were simulated
> correctly.
You are doing the exact same thing as the other moron. Asserting "correctness" instead of proving it.

What makes the simulation "correct"? Show me the source code for the "correctness" decider.


olcott

unread,
Dec 2, 2022, 11:26:33 AM12/2/22
to
The entire body of analytic knowledge of the analytic/synthetic
distinction is a subset of the body of analytic truth. Every element of
the body of analytic truth is only true because of mutual semantic
tautologies with other elements in this body.

“Analytic” sentences, such as “Pediatricians are doctors,” have
historically been characterized as ones that are true by virtue of the
meanings of their words alone and/or can be known to be so solely by
knowing those meanings.
https://plato.stanford.edu/entries/analytic-synthetic/ *AKA mutual
semantic tautologies*


A philosopher of logic examines the foundations of logic (thinking
outside the box) whereas logicians merely take these foundations for
granted and force all of their thinking inside the box of these given
foundations. This makes all logicians utterly blind to foundational
errors.

This conventional definition of Incomplete(T)
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ))
is proven to be incorrect on the basis that every self-contradictory
expression of language φ "proves" that T is "Incomplete".

Here is the correct assessment:
Not_a_Truth_Bearer_in_T(φ) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ))

olcott

unread,
Dec 2, 2022, 11:35:57 AM12/2/22
to
How do you prove that a "pile of bricks" is not a type of {baby kitten}?

Stipulated relations between concepts forming mutually self-defining
semantic tautologies encoded as finite strings.

AKA the body of analytic truth of the analytic/synthetic distinction.
https://plato.stanford.edu/entries/analytic-synthetic/

“Analytic” sentences ... are true by virtue of the meanings
of their words alone and/or can be known to be so solely by
knowing those meanings.

Skep Dick

unread,
Dec 2, 2022, 11:45:26 AM12/2/22
to
On Friday, 2 December 2022 at 18:26:33 UTC+2, olcott wrote:
> The entire body of analytic knowledge of the analytic/synthetic
> distinction is a subset of the body of analytic truth. Every element of
> the body of analytic truth is only true because of mutual semantic
> tautologies with other elements in this body.
>
> “Analytic” sentences, such as “Pediatricians are doctors,” have
> historically been characterized as ones that are true by virtue of the
> meanings of their words alone and/or can be known to be so solely by
> knowing those meanings.
> https://plato.stanford.edu/entries/analytic-synthetic/ *AKA mutual
> semantic tautologies*
Not going through this nonsense with you again.

Everything in computation is strictly structuralism - it's about the elements and structure of sets/spaces/types (however you conceptualise them) and relations between those spaces.
Your philosophical grounding is wonky.

> A philosopher of logic examines the foundations of logic (thinking
> outside the box) whereas logicians merely take these foundations for
> granted and force all of their thinking inside the box of these given
> foundations. This makes all logicians utterly blind to foundational
> errors.
Yes. It's called metalogic. You have no idea what an "error" is in logical terms.
And you haven't defined it in metalogical terms.

> This conventional definition of Incomplete(T)
> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ))
> is proven to be incorrect on the basis that every self-contradictory
> expression of language φ "proves" that T is "Incomplete".
Your head is so far up your ass you don't even know that ∃φ ∨ ¬∃φ is a computational statement. A decision procedure.
It's a statement that Either ∃φ is true; or ¬∃φ is true. You've heard of the Either monad, right?


Skep Dick

unread,
Dec 2, 2022, 11:46:01 AM12/2/22
to
On Friday, 2 December 2022 at 18:35:57 UTC+2, olcott wrote:
> How do you prove that a "pile of bricks" is not a type of {baby kitten}?
You don't.

Proof theory is about formal systems. It has nothing to do with the real world.

olcott

unread,
Dec 2, 2022, 11:55:13 AM12/2/22
to
Proof theory is not theory end all be all of every sort of proof.

The way that you prove that a "pile of bricks" is not a type of
{baby kitten} is within the knowledge ontology defining the
semantic meaning of natural language words.

Skep Dick

unread,
Dec 2, 2022, 12:19:01 PM12/2/22
to
On Friday, 2 December 2022 at 18:55:13 UTC+2, olcott wrote:
> Proof theory is not theory end all be all of every sort of proof.
It is. That's why it's called "proof theory" because it's about proofs being actual Mathematical objects.

If you have some other theory about what it means "to prove" something - share it with us.

> The way that you prove that a "pile of bricks" is not a type of
> {baby kitten} is within the knowledge ontology defining the
> semantic meaning of natural language words.
You are incredibly confused. "Knowledge ontology" is an oxymoron.

You have confused epistemology and ontology.

Skep Dick

unread,
Dec 2, 2022, 12:24:29 PM12/2/22
to
On Friday, 2 December 2022 at 18:55:13 UTC+2, olcott wrote:
> The way that you prove that a "pile of bricks" is not a type of
> {baby kitten} is within the knowledge ontology defining the
> semantic meaning of natural language words.
Your stupidity stems from confusing syntax and semantics.

The syntax says "This text is black". Define the semantics of "black" and prove that the sentence is true.

Mr Flibble

unread,
Dec 2, 2022, 12:32:52 PM12/2/22
to
A semantic definition can be constrained by the abstraction layer to which
it is being applied.

/Flibble

olcott

unread,
Dec 2, 2022, 12:47:27 PM12/2/22
to
On 12/2/2022 11:18 AM, Skep Dick wrote:
> On Friday, 2 December 2022 at 18:55:13 UTC+2, olcott wrote:
>> Proof theory is not theory end all be all of every sort of proof.
> It is. That's why it's called "proof theory" because it's about proofs being actual Mathematical objects.
>
> If you have some other theory about what it means "to prove" something - share it with us.

{Prove} always means applying truth preserving operations to expressions
of language deriving another expression of language typically called the
consequence/conclusion.

>
>> The way that you prove that a "pile of bricks" is not a type of
>> {baby kitten} is within the knowledge ontology defining the
>> semantic meaning of natural language words.
> You are incredibly confused. "Knowledge ontology" is an oxymoron.
>
> You have confused epistemology and ontology.

In computer science and information science, an ontology encompasses a
representation, formal naming, and definition of the categories,
properties, and relations between the concepts, data, and entities that
substantiate one, many, or all domains of discourse.
https://en.wikipedia.org/wiki/Ontology_(information_science)

olcott

unread,
Dec 2, 2022, 12:56:37 PM12/2/22
to
Rudolf Carnap and Richard Montague showed the details of how to specify
semantics syntactically, thus no need for any arbitrary division between
them.

dklei...@gmail.com

unread,
Dec 2, 2022, 1:28:48 PM12/2/22
to
On Friday, December 2, 2022 at 9:56:37 AM UTC-8, olcott wrote:
> Rudolf Carnap and Richard Montague showed the details of how to specify
> semantics syntactically, thus no need for any arbitrary division between
> them.
>
This statement is VERY wrong but comp.theory is not the place to discuss.

Skep Dick

unread,
Dec 2, 2022, 1:34:53 PM12/2/22
to
On Friday, 2 December 2022 at 19:32:52 UTC+2, Mr Flibble wrote:
> A semantic definition can be constrained by the abstraction layer to which
> it is being applied.

Don't tell me. Show me. Provide the semantic definition for "abstraction layer".

olcott

unread,
Dec 2, 2022, 1:37:51 PM12/2/22
to
It is required when the term {prove} is defined across the scope of
formal and natural languages.

{Prove} always means applying truth preserving operations to expressions
of language deriving another expression of language typically called the
consequence/conclusion.

This was required so that it can be proved that D is correctly simulated
by H.

Skep Dick

unread,
Dec 2, 2022, 1:38:02 PM12/2/22
to
On Friday, 2 December 2022 at 19:47:27 UTC+2, olcott wrote:
> On 12/2/2022 11:18 AM, Skep Dick wrote:
> > On Friday, 2 December 2022 at 18:55:13 UTC+2, olcott wrote:
> >> Proof theory is not theory end all be all of every sort of proof.
> > It is. That's why it's called "proof theory" because it's about proofs being actual Mathematical objects.
> >
> > If you have some other theory about what it means "to prove" something - share it with us.
> {Prove} always means applying truth preserving operations to expressions
> of language deriving another expression of language typically called the
> consequence/conclusion.
What do you mean by "operations". Do you perhaps have some meaning in mind other than the ideas captured in Operator Theory?

https://en.wikipedia.org/wiki/Operator_theory

> > You have confused epistemology and ontology.
> In computer science and information science, an ontology encompasses a
> representation, formal naming, and definition of the categories
> properties, and relations between the concepts, data, and entities that
> substantiate one, many, or all domains of discourse.
> https://en.wikipedia.org/wiki/Ontology_(information_science)
What do you mean by "representation". Do you perhaps have some meaning in mind other than the ideas captured in Representation Theory?

https://en.wikipedia.org/wiki/Representation_theory

Skep Dick

unread,
Dec 2, 2022, 1:42:41 PM12/2/22
to
On Friday, 2 December 2022 at 19:56:37 UTC+2, olcott wrote:
> Rudolf Carnap and Richard Montague showed the details of how to specify
> semantics syntactically, thus no need for any arbitrary division between
> them.
Don't tell me. Show me.

Given the expression "Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ))"

Define the meaning of the symbol "↔" using the syntax above.

Mr Flibble

unread,
Dec 2, 2022, 1:49:27 PM12/2/22
to
As best that is an uninteresting meta discussion, at worst it is just hand
waving on your part.

/Flibble

olcott

unread,
Dec 2, 2022, 1:50:08 PM12/2/22
to
I tend to apply my use of terms to their generic base meaning.
All proofs involve finite string transformation rules such that finite
strings having the semantic property of Boolean true are transformed
into finite strings having the semantic property of Boolean true.

Davidson's truth conditional semantics elaborates some of the details of
this. https://en.wikipedia.org/wiki/Truth-conditional_semantics

My reasoning applies across formal and natural languages. Truth
conditional semantics need not be restricted to natural language.

Skep Dick

unread,
Dec 2, 2022, 1:54:15 PM12/2/22
to
It's a meta-discussion, alright. Provide the semantic definition for "uninteresting" and prove it true.

olcott

unread,
Dec 2, 2022, 1:55:58 PM12/2/22
to
Simply a truth table showing that the LHS always has the same truth
value as the RHS.

Skep Dick

unread,
Dec 2, 2022, 2:04:12 PM12/2/22
to
On Friday, 2 December 2022 at 20:55:58 UTC+2, olcott wrote:
> On 12/2/2022 12:42 PM, Skep Dick wrote:
> > On Friday, 2 December 2022 at 19:56:37 UTC+2, olcott wrote:
> >> Rudolf Carnap and Richard Montague showed the details of how to specify
> >> semantics syntactically, thus no need for any arbitrary division between
> >> them.
> > Don't tell me. Show me.
> >
> > Given the expression "Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ))"
> >
> > Define the meaning of the symbol "↔" using the syntax above.
> Simply a truth table showing that the LHS always has the same truth
> value as the RHS.
So show me the source-code. for the decider ↔(lhs, rhs).

What does ↔(T,∃) mean ?

olcott

unread,
Dec 2, 2022, 2:11:45 PM12/2/22
to
It is only a truth table, have you ever heard of those?

> What does ↔(T,∃) mean ?

Gibberish to me.
↔(p,q) is the correct way to say this.

if (p.Boolean == q.Boolean)
return true;
return false;

Skep Dick

unread,
Dec 2, 2022, 2:18:23 PM12/2/22
to
On Friday, 2 December 2022 at 21:11:45 UTC+2, olcott wrote:
> It is only a truth table, have you ever heard of those?
> > What does ↔(T,∃) mean ?
> Gibberish to me.
I don't care what you think.
I want to know what your function would return if invoked as above?

> ↔(p,q) is the correct way to say this.
*sigh* idiot.
let p = T
let q = ∃

What would evaluating the expression "↔(p,q)" do?

> if (p.Boolean == q.Boolean)
> return true;
> return false;
Sorry. I have no idea what you mean by "==".

Please show me the source code for ==(p,q).

olcott

unread,
Dec 2, 2022, 2:28:22 PM12/2/22
to
Just playing head games...

Skep Dick

unread,
Dec 2, 2022, 2:33:36 PM12/2/22
to
On Friday, 2 December 2022 at 21:28:22 UTC+2, olcott wrote:
> > Please show me the source code for ==(p,q).
> Just playing head games...

No. Try again. Please show me the source code for the function ==(p,q) such that...

==(1,1) returns true; and ==(1,2) returns false.

Maybe you'll finally understand the difference between intensional and and extensional definitions of terms.

olcott

unread,
Dec 2, 2022, 2:48:50 PM12/2/22
to
C syntax mapped to x86 semantics implemented using hardware circuits.

Skep Dick

unread,
Dec 2, 2022, 2:52:56 PM12/2/22
to
On Friday, 2 December 2022 at 21:48:50 UTC+2, olcott wrote:
> C syntax mapped to x86 semantics implemented using hardware circuits.
*cough* bullshit *cough*

You are welcome to provide the source code for the ==(p,q) hardware circuit in your favourite HDL (Hardware Description Language).

https://en.wikipedia.org/wiki/Hardware_description_language

olcott

unread,
Dec 2, 2022, 2:57:12 PM12/2/22
to
I stop talking to people that deny things that they know are true.

Skep Dick

unread,
Dec 2, 2022, 2:59:26 PM12/2/22
to
On Friday, 2 December 2022 at 21:48:50 UTC+2, olcott wrote:
> C syntax mapped to x86 semantics implemented using hardware circuits.
And just so you catch a wake up call. the CMP x86 operator (which is basically what == maps to for small integers) is implemented using subtraction.

cmp(p,q) subtracts q from p which then checks the CPU's zero-flag. Buuuut, you have probably already guessed what I will ask you next...

Please show me the source code for -(p,q)

Skep Dick

unread,
Dec 2, 2022, 3:02:00 PM12/2/22
to
On Friday, 2 December 2022 at 21:57:12 UTC+2, olcott wrote:
> On 12/2/2022 1:52 PM, Skep Dick wrote:
> > On Friday, 2 December 2022 at 21:48:50 UTC+2, olcott wrote:
> >> C syntax mapped to x86 semantics implemented using hardware circuits.
> > *cough* bullshit *cough*
> >
> > You are welcome to provide the source code for the ==(p,q) hardware circuit in your favourite HDL (Hardware Description Language).
> >
> > https://en.wikipedia.org/wiki/Hardware_description_language
> I stop talking to people that deny things that they know are true.
Yeah. I am calling bullshit!

Of course I know that =(p,q) is true when p=1; q=1.
And of course I know that =(p,q) is false when p=1; q=2

That's not the issue here!

I am asking you for the source code of the =(p,q) decider.

Mr Flibble

unread,
Dec 2, 2022, 5:38:44 PM12/2/22
to
If you wish to know what the word "uninteresting" MEANS then I suggest you
invest in a dictionary of the English language. Prove that the meaning of
the word is true? The meaning of the word? That is a category error on
your part.

/Flibble

Richard Damon

unread,
Dec 2, 2022, 8:02:49 PM12/2/22
to
On 12/2/22 10:54 AM, olcott wrote:
> On 12/2/2022 7:49 AM, Skep Dick wrote:
>> On Friday, 2 December 2022 at 15:01:55 UTC+2, richar...@gmail.com wrote:
>>> No, completenes is about the PROVABILITY of statement.
>>> A statement can be known to have a correct answer, but we can not
>>> actually know that answer.
>> It's the exact same thing.
>>
>> If you can't prove whether a **particular** answer is "correct" then
>> your system is incomplete with respect to "correctness"!
>>
>> What the hell does it mean for the statement "2+2" to have a correct
>> answer if you can't actually determine whether 4 is a "correct" answer?
>>
>>>>> Olcott seem to think that this specific H can sometimes give one
>>>>> answer
>>>>> and sometimes another.
>>>> It's not a matter of what anyone thinks. Indeed, any specific H
>>>> could be non-deterministic.
>>> Not an be a Turing Machine Equivalent.
>> Nonsense. Deterministic and non-deterministic Turing Machines are
>> sub-types of Turing Machines.
>>
>>> So, you don't understand that problem either.
>> There's nothing to understand.  You ask a question (2+2)  - some
>> function produces an answer (4).
>>
>> The answer "4" is either correct or incorrect. Which one is it?
>>
>>>> You already know the answer - just produce it.
>>> The problem is H needs to produce it, but can't
>> That's a lie. H produces an answer.
>>
>> The answer H produces is either correct or incorrect. Which one is it?
>
> https://liarparadox.org/2022_11_14.zip
>
> The H(D,D) of the above fully operational software system
> correctly determines that its input specifies a non-halting
> sequence of configurations according to this criteria:
>
>   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.

So it BY DEFINITION isn't a Halt Decider. PERIOD.

Because the DEFINITION of a Halt Decider is that it MUST report Halting
from H(M,x) if M(x) halts when run, and Non-Halting from H(M,x) if M(x)
will NEVER stop running after an unbounded number of steps.

Since D(D) WILL Halt since H(D,D) returns 0, the correct answer for an
ACTUAL Halt Decider is Halting.

Since your critera says something different, it isn't equivalent, and
thus you have just PROVED that your "Simulating Halt Deciders" are not
actually Halt Decider.

The fact that you keep on claiming they are just shows that you are
either a pathologica liar or totally mentally incompetent.

>
> *Correct simulation of D by H* is defined as a line-by-line
> mapping from the x86 source code of D to each line of the
> execution trace of D.

Which isn't the definition of Correct Simulation if the field, which is
one reason you get different

>
> Only a diverge of this mapping shows that the simulation is
> incorrect, it is otherwise correct even if incomplete.

Thus again PROVING that yoy are not working on the ACTUAL Halting
Problem, and are proven to be a LIAR when you claim you are.

Either that or totally mentally incompetent to not to be able to
understand that basic definition and rules of logic.

You are just PROVING you have wasted the last 18 years of your life.

>
> _D()
> [000019b3] 55         push ebp
> [000019b4] 8bec       mov ebp,esp
> [000019b6] 51         push ecx
> [000019b7] 8b4508     mov eax,[ebp+08]
> [000019ba] 50         push eax
> [000019bb] 8b4d08     mov ecx,[ebp+08]
> [000019be] 51         push ecx
> [000019bf] e8bff9ffff call 00001383
> [000019c4] 83c408     add esp,+08
> [000019c7] 8945fc     mov [ebp-04],eax
> [000019ca] 837dfc00   cmp dword [ebp-04],+00
> [000019ce] 7402       jz 000019d2
> [000019d0] ebfe       jmp 000019d0
> [000019d2] 8be5       mov esp,ebp
> [000019d4] 5d         pop ebp
> [000019d5] c3         ret
> Size in bytes:(0035) [000019d5]
>
> _main()
> [000019e3] 55             push ebp
> [000019e4] 8bec           mov ebp,esp
> [000019e6] 68b3190000     push 000019b3 // push D
> [000019eb] 68b3190000     push 000019b3 // push D
> [000019f0] e88ef9ffff     call 00001383 // call H
> [000019f5] 83c408         add esp,+08
> [000019f8] 33c0           xor eax,eax
> [000019fa] 5d             pop ebp
> [000019fb] c3             ret
> Size in bytes:(0025) [000019fb]
>
>  machine   stack     stack     machine    assembly
>  address   address   data      code       language
>  ========  ========  ========  =========  =============
> [000019e3][00102a39][00000000] 55         push ebp      // begin main
> [000019e4][00102a39][00000000] 8bec       mov ebp,esp
> [000019e6][00102a35][000019b3] 68b3190000 push 000019b3 // push D
> [000019eb][00102a31][000019b3] 68b3190000 push 000019b3 // push D
> [000019f0][00102a2d][000019f5] e88ef9ffff call 00001383 // call H
>
> When H correctly simulates D it finds that D remains stuck in recursive
> simulation
>
> H: Begin Simulation   Execution Trace Stored at:112ae5
> Address_of_H:1383
> [000019b3][00112ad1][00112ad5] 55         push ebp       // begin D
> [000019b4][00112ad1][00112ad5] 8bec       mov ebp,esp
> [000019b6][00112acd][00102aa1] 51         push ecx
> [000019b7][00112acd][00102aa1] 8b4508     mov eax,[ebp+08]
> [000019ba][00112ac9][000019b3] 50         push eax       // call D
> [000019bb][00112ac9][000019b3] 8b4d08     mov ecx,[ebp+08]
> [000019be][00112ac5][000019b3] 51         push ecx       // push D
> [000019bf][00112ac1][000019c4] e8bff9ffff call 00001383  // call H
> H: Infinitely Recursive Simulation Detected Simulation Stopped
>
> We can see that the first seven instructions of D simulated by H
> precisely match the first seven instructions of the x86 source-code of
> D. This conclusively proves that these instructions were simulated
> correctly.
>
>

Mr Flibble

unread,
Dec 2, 2022, 8:35:40 PM12/2/22
to
Why do you persist in posting the same thing again and again and again? Do
you somehow think it will eventually make one iota of a difference?
Haven't you got anything better to do with your time?

/Flibble

Richard Damon

unread,
Dec 2, 2022, 8:38:54 PM12/2/22
to
On 12/2/22 8:49 AM, Skep Dick wrote:
> On Friday, 2 December 2022 at 15:01:55 UTC+2, richar...@gmail.com wrote:
>> No, completenes is about the PROVABILITY of statement.
>> A statement can be known to have a correct answer, but we can not actually know that answer.
> It's the exact same thing.

Nope, we might know that an answer MUST exist, as the problem falls into
the domain of the Law of the Excluded Middle, and thus DOES have a
corret answer, but we are unable to find what that answer is.

>
> If you can't prove whether a **particular** answer is "correct" then your system is incomplete with respect to "correctness"!

Right, which is what I was showing. Perhap you have a comprehension issue.

>
> What the hell does it mean for the statement "2+2" to have a correct answer if you can't actually determine whether 4 is a "correct" answer?

Who said we couldn't show the correct answer for 2+2?

>
>>>> Olcott seem to think that this specific H can sometimes give one answer
>>>> and sometimes another.
>>> It's not a matter of what anyone thinks. Indeed, any specific H could be non-deterministic.
>> Not an be a Turing Machine Equivalent.
> Nonsense. Deterministic and non-deterministic Turing Machines are sub-types of Turing Machines.
>
>> So, you don't understand that problem either.
> There's nothing to understand. You ask a question (2+2) - some function produces an answer (4).

Not my question, so the rest is totally irrelevant. The fact that for
SOME questions we can't prove the correct answer doesn't mean that we
can't prove the correct answer for others.

>
> The answer "4" is either correct or incorrect. Which one is it?
>
>>> You already know the answer - just produce it.
>> The problem is H needs to produce it, but can't
> That's a lie. H produces an answer.
>
> The answer H produces is either correct or incorrect. Which one is it?

The answer his H (or in fact ANY H for the question based on that
particular H) is wrong.

>
>> A program that halts, can always be proven to halt by just running it
>> till it reaches that final step.
> This is incoherent. a Proof IS a program. A proof either halts; or it doesn't.

So? You don't understand that BY DEFINITION, if a given program does
Ha;t, that means it halts in some finite number of steps, and thus by
doing those finite number of steps, we have just proven that it does halt.

You seem to be having a comprehension issue.

>
>> For programs that don't halt, we can often actually PROVE that they
>> don't, but not for all cases. That is actually one way to show the
>> Halting Problem.
> Incoherent nonsense. How do you prove that a program halts when a proof is a program?
>
> How do you prove that a proof halts?

On way to prove it halts is to do it, and show that it reaches the final
step in a finite number of steps.

A proof is a finite sequence of logical steps. That sequence of steps
CAN be the steps of the program. So, the running of a halting program,
will eventually reach that final state, and PROVES that it is a halting
program.

It seems you are the one having problems seeing that a prove can be a
program that halts.

>
>> Note, it is possible for us to not know if the answer from H is correct
>> or incorrect.
> How do you know? Surely you must have some method in mind by which you can prove that an answer is "correct" or "incorrect"?

It follows from the fact that not all programs are deciable with regard
to halting.

>
> Provide it please.

You can't necessarily prove that something is unknowable. That is part
of incompleteness.

>
>> If H answers Halting, and it is correct, we can prove it correct by just
>> running the input program.
> Huh?!? How? Any running program could halt. Eventually.


If the program WILL Halt, then by running it, we will see that and PROVE
that it halts.

Note, there are patterns that are provably non-halting, for instance,
any Turing Machine that returns to an exact state (including the
contents and placement of the tape) MUST continue on the same path it
did last time, and thus we can prove by induction that it will never halt.


>
> If P hasn't yet halted but could in future WHEN do you assert that H was "incorrect" ?

Irrelevent to the point you are refering to, since that case was
assuming that H answered Halting and WAS correct.

You are asking about the case BELOW, and as I mentioned just above,
there are SOME cases you can prove that a program will never halt.

>
>> If H answers Halting, and that is incorrect, we MIGHT be able to prove
>> it wrong, if this is a case that we can prove to be non-halting.
> Huh?!? How? Proofs are programs.

So, you don't understand how induction can be used to prove something in
a finite number of steps about an infinite set?

>
> What sort of program are you going to write which proves that another program halts?

I am not writing "Programs", I am talking about PROOF,

>
>> If H answers Non-Halting, and that is incorrect, we can prove it wrong
>> by running the input and seeing it halt (as we do in the case in question).
> But you would be doing EXACTLY what H did!?!?
>
> It ran/simulated the program! How is your runner/simulator better than H's runner/simulator?

Because D isn't built to contradict me.

Yes, there are some programs that I will be unable to decide on, but
because I can see the relationship between H and D, and can use logic
based on that.

>
>> If H answers Non-Halting, and that is correct, we MIGHT be able to prove
>> it right, or we might not.
> Huh?!? How?!? Proofs are programs.

Not to me. Maybe you are limiting your thinking to programatic proofs.

>
> What sort of program (other than H) would you produce to prove that another program doesn't halt?

I didn't say I was using a program, I used a PROOF, using the knowledge
of the construction of D.

>
>> This shows the difference between PROVING something is correct or
>> incorrect or it actually being correct or incorrect.
> No, this shows sophistry. Proofs are programs.
>
> If program A proves that program B is correct, you still have no proof that program A is correct about program B being correct.

So, it seems your logic system has no concept of things being actually
true or proven. If you can't believe your own proof, you know nothing.

>
>> A binary, but non-computable, answer WILL be either correct or
>> incorrect, but we might not know which it is in a given case.
> You are equivocating "knowing".
>
> How would you know whether an answer is "correct" in the cases where you can know?

When I can actually prove them. Everything actually Proven is True.

>
>> No, we can show that THIS program WILL halt....
> How? Surely you have to run/simulate THIS program.

Right, the program mentioned is know to Halt, and that can be proven by
just running it and seeing that it does halts.

I note you are taking answers out of context, showing you are being a
DECEPTIVE Skep Dick

>
> When you run/simulate THIS program - you are doing EXACTLY the same thing as the simulating halt-decider.

No, the simulation Halt-decider aborted its simulation to give the
non-halting answer. I didn't, and because the program isn't based on me,
we don't get the problem that H runs into.

>
>> we can prove that this H gave the wrong answer.
> Oh, you can prove it. Can you? Proofs are programs.
>
> Since you are volunteering a proof - please provide a program/proof which correctly determines that H is incorrect.

By Inspecting of P, P(P) will Halt if H(P,P) returns non-halting (in the
Turing Machine case, a final state of P is the exact state of the final
state of H that reports non-halting).

Since it is claimed that H(P,P) will "correctly" return Non-Halting, we
see that that can't be correct, as if H(P,P) returns non-halting P(P)
will Halt.

We can then go father and show that if H(P,P) returns Halting, that P(P)
will not halt, as by constuction, the final state of H that reports
non-halting has been converted into an infinite loop, which will clearly
never halt.

Since by requirement, H to give a correct answer must do one of the two
above behaviors, it will ALWAYS be wrong.

>
>> For the original proof
> In what programming language are you going to present this "proof"?

LOGIC.

>
>> we can also prove that the H^ program WILL be non-halting if the H is shown to return Halting for H applied to H^ H^
> In what programming language are you going to present this "proof"?
>

LOGIC.

>> so we can actually PROVE that IF it gives an answer
> In what programming language can we PROVE this?
>

LOGIC.

>> Halting is a property which obeys the law of the excluded middle, so we
>> have shown that H must be wrong.
> This is immaterial. Since both "halting" and "wrongness" are both non-trivial semantic properties subject to Rice's theorem.


Right, so there exists SOME programs and statements that can not be
decided if they will Halt or are incorrect.
>
>
>> To disprove a machine from being a Halt Decider, since that requires
> In what programming language are you going to disprove this?

LOGIC. Maybe you don't understand it, because it predates you.

>
>> This lets us prove that ALL machines that might claim to be halt deciders have to be wrong about a specific program built from them.
> What programming language lets you prove that?

LOGIC, I wrote the proof above.

>
> Surely you are aware that you are guilty of equivocation? SURELY? Unless, of course you are not a logician.
>
> Because you keep equivocating the term "proof", "to prove" and "program".
> Proofs are not LIKE programs. Proofs are not related to programs but different.
> Proofs ARE programs. They are two different words for exactly the same objects.

Nope.

>
> https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
>
>
>

Which says that proofs CORRESPOND to programs, not ARE programs.

You don't seem to understand the system you are working in.

Note, that statement of "A Proof is a Program" is listed as an ABSTRACTION.

I don't need to abstract my Proofs into a program of your restricted
languge, and apparently, your programming paradym can't actually show
that things are correct, so seems to be massively inferior to actual logic.

Richard Damon

unread,
Dec 2, 2022, 8:40:20 PM12/2/22
to
On 12/2/22 8:35 PM, Mr Flibble wrote:

> Why do you persist in posting the same thing again and again and again? Do
> you somehow think it will eventually make one iota of a difference?
> Haven't you got anything better to do with your time?
>
> /Flibble

I could ask the same thing of you. Why do YOU complain about my posting?

Skep Dick

unread,
Dec 3, 2022, 12:48:00 AM12/3/22
to
On Saturday, 3 December 2022 at 03:38:54 UTC+2, richar...@gmail.com wrote:
> Nope, we might know that an answer MUST exist, as the problem falls into
> the domain of the Law of the Excluded Middle, and thus DOES have a
> corret answer, but we are unable to find what that answer is.
Bullshit! The search-space has 2 elements! Brute force it!

If you already have access to a correctness-decider (and you MUST have access to one because you keep asserting which answers are "correct" and which are "incorrect")

then just test both cases for "correctness" and tell us which one is "correct".

> > If you can't prove whether a **particular** answer is "correct" then your system is incomplete with respect to "correctness"!
> Right, which is what I was showing. Perhap you have a comprehension issue.
You are lying. You haven't shown any such thing because you haven't produced a "correctness" decider.

> > What the hell does it mean for the statement "2+2" to have a correct answer if you can't actually determine whether 4 is a "correct" answer?
> Who said we couldn't show the correct answer for 2+2?
Who even asked you such a question?!?!

I asked you whether 4 is the correct answer to 2+2.

Show me your correctness decider.

> > There's nothing to understand. You ask a question (2+2) - some function produces an answer (4).
> Not my question, so the rest is totally irrelevant. The fact that for
> SOME questions we can't prove the correct answer doesn't mean that we
> can't prove the correct answer for others.
But I am not asking you to PROVE the answer ?!?! I am asking you to VERIFY whether a given answer is correct!

Why is this confusing you?

> > The answer H produces is either correct or incorrect. Which one is it?
> The answer his H (or in fact ANY H for the question based on that
> particular H) is wrong.
HOW have you verified this?

> >> A program that halts, can always be proven to halt by just running it
> >> till it reaches that final step.
> > This is incoherent. a Proof IS a program. A proof either halts; or it doesn't.
>
> So? You don't understand that BY DEFINITION, if a given program does
> Ha;t, that means it halts in some finite number of steps, and thus by
> doing those finite number of steps, we have just proven that it does halt.
Yes but you keep avoiding the question.

HOW do YOU know whether a proof halts or not ? Given that you don't have a working halt-decider - HOW do you keep acquiring this knowledge?

> You seem to be having a comprehension issue.
Not me... It's definitely you.

> On way to prove it halts is to do it, and show that it reaches the final
> step in a finite number of steps.
OK. HOW do you show that?

> A proof is a finite sequence of logical steps. That sequence of steps
> CAN be the steps of the program. So, the running of a halting program,
> will eventually reach that final state, and PROVES that it is a halting
> program.
HOW do you know that the final state is reached?

> It seems you are the one having problems seeing that a prove can be a
> program that halts.
I know THAT a proof is a program that halts. That's not what I am asking you!

I am asking you to explain HOW you've come to acquire the knowledge THAT the program halts.
And far more importantly - I am asking you to explain HOW you've come to know that you knowledge is "correct"

What if you have "proven" that a program halts, but your proof is wrong?

> It follows from the fact that not all programs are deciable with regard
> to halting.
OK, but nobody asked you that.

I asked you whether the "correctness" of a halt-decider is decidable.

> You can't necessarily prove that something is unknowable. That is part
> of incompleteness.
You keep using the word "unknowable". You must know that something is unknowable to call it "unknowable". Surely !

Or are you saying that you may be incorrect in asserting it "unknowable".

> If the program WILL Halt, then by running it, we will see that and PROVE
> that it halts.
But that's exactly what Olcott's simulating halt-decider does!!!!

How is it that when he does it his answer is "incorrect".
But when you do it your answer will be "correct".

What are you using as a correctness-decider ?!?

> Note, there are patterns that are provably non-halting, for instance,
> any Turing Machine that returns to an exact state (including the
> contents and placement of the tape) MUST continue on the same path it
> did last time, and thus we can prove by induction that it will never halt.
But that's PRECISELY what Olcott's halt-decider does?!?!?!

It observes the stack trace. Sees that the state machine calls the same function with the same parameters TWICE and aborts because it has detected an infinite loop.

YOU are the one who keeps calling that "incorrect" but here you are now advocating for it ?!?!?


> > If P hasn't yet halted but could in future WHEN do you assert that H was "incorrect" ?
>
> Irrelevent to the point you are refering to, since that case was
> assuming that H answered Halting and WAS correct.
100% relevant. I am asking you to tell us (and you continue to refuse) HOW you've determined the "correctness".

Which decider did you use?

> You are asking about the case BELOW, and as I mentioned just above,
> there are SOME cases you can prove that a program will never halt.
HOW DO YOU KNOW which case we find ourselves in?

Without a correctness-decider we could be dealing with the case where "H answers Halting, and that's correct" OR the case where "H answers Halting, and that's incorrect"

HOW DO YOU KNOW which case you are in ?!?!?

> So, you don't understand how induction can be used to prove something in
> a finite number of steps about an infinite set?
Oh, I think I understand just fine!

Inductive/recursive proofs don't halt.
Co-inductive/co-recursive proofs halt.


> I am not writing "Programs", I am talking about PROOF,
PROOFS ARE PROGRAMS. Two different words for the exact same Mathematical object.

So you are talking about the same thing using two different names.

> Because D isn't built to contradict me.
D is built to contradict its appointed halt-decider.

If YOU are the appointed halt decider (and not H) then D is built to contradict YOU (and not H).

If D doesn't contradict you - then you are not the halt-decider for D.

You know. By definition...

> Yes, there are some programs that I will be unable to decide on, but
> because I can see the relationship between H and D, and can use logic
> based on that.
Proofs. Programs. Logic. Same thing.

> Not to me. Maybe you are limiting your thinking to programatic proofs.
I am "limiting my thinking" to the general concept of proof. As captured in proof theory.

If you have any broader and more comprehensive notion/conceptions of "proof" - by all means. Share it with us.


> I didn't say I was using a program, I used a PROOF, using the knowledge
> of the construction of D.
Proofs ARE programs. Different words for the same construct!

So you didn't say you are using a program/proofs, you used a program/proof.

Idiot.

> So, it seems your logic system has no concept of things being actually
> true or proven. If you can't believe your own proof, you know nothing.
Bullshit. That is ALL my logic has.

You give inputs to functions - they produces outputs. If the input "2+2=5" produces the output "true" then the string "2+2=5" has been proven true.

Whether that proof is "correct"... I don't know. My logic is incomplete with respect to correctness.

> When I can actually prove them. Everything actually Proven is True.
What nonsense. Everything that's Proven is Proven. Be it proven true; or proven false; or proven a Boolean. Or proven a Number. Or proven Halting.

> Right, the program mentioned is know to Halt, and that can be proven by
> just running it and seeing that it does halts.
Which is exactly what Olcott's H does. Yet you disagreed with it.

> I note you are taking answers out of context, showing you are being a
> DECEPTIVE Skep Dick
I am NOT taking the answers out of context. So it must be you who's being deceptive.

> No, the simulation Halt-decider aborted its simulation to give the
> non-halting answer.
Yes. Because it does proof-by-induction. It detected the program returning to the same state twice.

You literally just said that you can prove things about infinite objects in finite time. But now ?!?!?

>I didn't, and because the program isn't based on me, we don't get the problem that H runs into.
Oh, so you didn't abort the program after N steps? You ran it for infinitely-many steps?


> By Inspecting of P, P(P) will Halt if H(P,P) returns non-halting (in the
> Turing Machine case, a final state of P is the exact state of the final
> state of H that reports non-halting).
What sort of "inspection" are YOU performing that you can't give us programmatically - in source code ?!?!

> Since it is claimed that H(P,P) will "correctly" return Non-Halting, we
> see that that can't be correct, as if H(P,P) returns non-halting P(P)
> will Halt.
What is it that you think you can "see" that H cannot "see" !?!?!

> We can then go father and show that if H(P,P) returns Halting, that P(P)
> will not halt, as by constuction, the final state of H that reports
> non-halting has been converted into an infinite loop, which will clearly
> never halt.
"We" ?!?! So we are, in fact doing a step-trace execution of H(P,P) ?!?!?!

EXACTLY like Olcott is doing?!?

> Since by requirement, H to give a correct answer must do one of the two
> above behaviors, it will ALWAYS be wrong.
Holy shit dude, you keep spinning in circles.

HOW DO YOU KNOW that H gave you an "incorrect" answer?
HOW did you obtain the "correct" one

Without the a priori knowledge of WHICH answer is "correct"; and WHICH answer is "incorrect" you can't possibly decide that H is correct; or incorrect.

So WHERE did you get the knowledge from if not H?

> >> For the original proof
> > In what programming language are you going to present this "proof"?
>
> LOGIC.
WHICH ONE?

> >> we can also prove that the H^ program WILL be non-halting if the H is shown to return Halting for H applied to H^ H^
> > In what programming language are you going to present this "proof"?
> >
>
> LOGIC.
WHICH ONE?

> >> so we can actually PROVE that IF it gives an answer
> > In what programming language can we PROVE this?
> >
>
> LOGIC.
WHICH ONE?


> Right, so there exists SOME programs and statements that can not be
> decided if they will Halt or are incorrect.
Right! So is your assertion that H is "incorrect" one of those programs; or not?!?

Is your assertion about the incorrectness of H correct or incorrect?

> >> To disprove a machine from being a Halt Decider, since that requires
> > In what programming language are you going to disprove this?
>
> LOGIC. Maybe you don't understand it, because it predates you.
WHICH ONE?

I keep asking you this because there are hundreds of different logics!

Classical. Intuitionistic. Temporal. Linear. Many-sorted. Many-valued. Boolean. Ternary. Infinitary.

Maybe you don't understand because you just don't understand anything?

> >> This lets us prove that ALL machines that might claim to be halt deciders have to be wrong about a specific program built from them.
> > What programming language lets you prove that?
>
> LOGIC, I wrote the proof above.
WHICH ONE?

You certainly haven't produces anything in any LOGIC.

> Which says that proofs CORRESPOND to programs, not ARE programs.
And thus we have proven that you don't actually understand anything.

> You don't seem to understand the system you are working in.
Dude. You don't even know WHICH logic you are using.

You are incompetent at identification. And you have incompetently mis-identified WHO doesn't understand.

It's you, not me.

> I don't need to abstract my Proofs into a program of your restricted
> languge , and apparently, your programming paradym can't actually show
> that things are correct, so seems to be massively inferior to actual logic.
Idiot. Your paradigm can't even verify the correctness of an answer.

Skep Dick

unread,
Dec 3, 2022, 1:20:10 AM12/3/22
to
On Saturday, 3 December 2022 at 00:38:44 UTC+2, Mr Flibble wrote:
> If you wish to know what the word "uninteresting" MEANS then I suggest you
> invest in a dictionary of the English language. Prove that the meaning of
> the word is true? The meaning of the word? That is a category error on
> your part.
We are talking about formal logic and proof-systems and you randomly ended up talking about dictionaries and the English language?

Talk about a category error...

Mr Flibble

unread,
Dec 3, 2022, 8:24:51 AM12/3/22
to
You asked me to prove the semantic definition of the word "uninteresting"
is true: that is a nonsense in the form of a category error: you cannot
prove a definition is true, the definition JUST IS, i.e. it is agreed as
part of the vernacular (as far as the MEANING of words is concerned).
SEMANTICS is about MEANING.

/Flibble

Skep Dick

unread,
Dec 3, 2022, 8:36:13 AM12/3/22
to
On Saturday, 3 December 2022 at 15:24:51 UTC+2, Mr Flibble wrote:
> You asked me to prove the semantic definition of the word "uninteresting"
> is true: that is a nonsense in the form of a category error: you cannot
> prove a definition is true, the definition JUST IS, i.e. it is agreed as
> part of the vernacular (as far as the MEANING of words is concerned).
> SEMANTICS is about MEANING.

So you can't; or won't provide formal semantics for the notion of "uninteresting".

Why are you still participating in this discussion if it's so "uninteresting" to you?

Richard Damon

unread,
Dec 3, 2022, 9:14:27 AM12/3/22
to
On 12/3/22 12:47 AM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 03:38:54 UTC+2, richar...@gmail.com wrote:
>> Nope, we might know that an answer MUST exist, as the problem falls into
>> the domain of the Law of the Excluded Middle, and thus DOES have a
>> corret answer, but we are unable to find what that answer is.
> Bullshit! The search-space has 2 elements! Brute force it!
>
> If you already have access to a correctness-decider (and you MUST have access to one because you keep asserting which answers are "correct" and which are "incorrect")

No, I have a "PARTIAL Correctness-Decider", that can handle THIS
particular case.

Remember, the definition of a "Decider" is a machine that handles ALL
cases. We don't need such a machine for this, just one that can handle
THIS case.

>
> then just test both cases for "correctness" and tell us which one is "correct".

And the problem is that one case can possible take infinite time, which
isn't allowe.

That has been explaied to you several times, but you seem to dense to
understand that.

>
>>> If you can't prove whether a **particular** answer is "correct" then your system is incomplete with respect to "correctness"!
>> Right, which is what I was showing. Perhap you have a comprehension issue.
> You are lying. You haven't shown any such thing because you haven't produced a "correctness" decider.
>
>>> What the hell does it mean for the statement "2+2" to have a correct answer if you can't actually determine whether 4 is a "correct" answer?
>> Who said we couldn't show the correct answer for 2+2?
> Who even asked you such a question?!?!
>
> I asked you whether 4 is the correct answer to 2+2.
>
> Show me your correctness decider.

I don't think you would understand the math needed for that sort of proof.

Note also, that isn't the question that I was talking about, so my
partial decider doesn't need to work on it

>
>>> There's nothing to understand. You ask a question (2+2) - some function produces an answer (4).
>> Not my question, so the rest is totally irrelevant. The fact that for
>> SOME questions we can't prove the correct answer doesn't mean that we
>> can't prove the correct answer for others.
> But I am not asking you to PROVE the answer ?!?! I am asking you to VERIFY whether a given answer is correct!

And what is the difference between PROVING something and VERIFYING it?

Both are showing steps that demonstrate that the statement must be true.

>
> Why is this confusing you?
>
>>> The answer H produces is either correct or incorrect. Which one is it?
>> The answer his H (or in fact ANY H for the question based on that
>> particular H) is wrong.
> HOW have you verified this?

Because I have a valid proof of it.

If you don't believe in proofs, then you can't actually know anything.

>
>>>> A program that halts, can always be proven to halt by just running it
>>>> till it reaches that final step.
>>> This is incoherent. a Proof IS a program. A proof either halts; or it doesn't.
>>
>> So? You don't understand that BY DEFINITION, if a given program does
>> Ha;t, that means it halts in some finite number of steps, and thus by
>> doing those finite number of steps, we have just proven that it does halt.
> Yes but you keep avoiding the question.
>
> HOW do YOU know whether a proof halts or not ? Given that you don't have a working halt-decider - HOW do you keep acquiring this knowledge?

Because I reached the end of it and it became final.

Again, you don't seem to understand the ability to show A particular
case from having a general proof.

>
>> You seem to be having a comprehension issue.
> Not me... It's definitely you.

Nope. Its you. You are even showing that you don't understand the
difference between proving one case and solving the general.

>
>> On way to prove it halts is to do it, and show that it reaches the final
>> step in a finite number of steps.
> OK. HOW do you show that?

As I said, run it and see that it reaches a final state.

For someone who claims that proofs are programs, no understanding that
the can actually be run to see they reach a final state seems utterly
stupid.

>
>> A proof is a finite sequence of logical steps. That sequence of steps
>> CAN be the steps of the program. So, the running of a halting program,
>> will eventually reach that final state, and PROVES that it is a halting
>> program.
> HOW do you know that the final state is reached?

Because it DID when I ran it.

Reality IS a proof.

>
>> It seems you are the one having problems seeing that a prove can be a
>> program that halts.
> I know THAT a proof is a program that halts. That's not what I am asking you!

Nope, you THINK a proof is a program that halts. I gave you a proof that
wasn't a program (but perhaps could be converted into a program) thus I
have demonstated that you statement is FALSE, and you are ignorant.

>
> I am asking you to explain HOW you've come to acquire the knowledge THAT the program halts.
> And far more importantly - I am asking you to explain HOW you've come to know that you knowledge is "correct"

I've done it, but it seems to be beyound your understanding.

>
> What if you have "proven" that a program halts, but your proof is wrong?

I used only demonstartably correct steps, so the proof is valid.

IF you want to challange my proof, show the incorrect step I used.

You seem to have a fundamental problem with knowing what Truth is.

This is one of the problems of thinking of Proofs as Programs when you
start to try to reason about Programs. Proofs, when built by the rules,
are necessarily correct, just like a program will always produce the
answer that that program produces.

>
>> It follows from the fact that not all programs are deciable with regard
>> to halting.
> OK, but nobody asked you that.
>
> I asked you whether the "correctness" of a halt-decider is decidable.

And, as I have explianed, often yes, but there are cases where it can't
be, thus, in it is not decidable in general.

You seem to have a problem understanding that undecidable in general
still allows the proposition to be able to be decided for many specific
cases.

>
>> You can't necessarily prove that something is unknowable. That is part
>> of incompleteness.
> You keep using the word "unknowable". You must know that something is unknowable to call it "unknowable". Surely !
>
> Or are you saying that you may be incorrect in asserting it "unknowable".

That is a funny thing about unknowability. We know that some things are
unknowable, but in many cases we can't prove that a particual something
is unknowable, becuase by its nature, if we knew we couldn't prove its
answer, we would know the answer.

Halting is a property like that. If we KNEW that the halting status of a
given machine/input combination was proved to be "Unknowable", then we
would know that it must be non-halting, as all Halting Machines are
provably Halting by just running them, which by DEFINITION means they
will reach a final state in a finite time, thus they become the proof of
their own finiteness.

Thus if we could somehow proof that we can't do that, it means by
definition, the machine must never stop, so ALL unknowable Halting
problems must be non-halting, so we must not be able to prove that they
ARE unknowable, just they are currently unknown, because that class
could inlcude Halting Machines that we just haven't run long enough to
reach a final state.


>
>> If the program WILL Halt, then by running it, we will see that and PROVE
>> that it halts.
> But that's exactly what Olcott's simulating halt-decider does!!!!

Nope, and that is his flaw. He runs it for a while, until it meets a
condition that he THINKS (incorrectly) shows non-halting behavior, then
he stops.

>
> How is it that when he does it his answer is "incorrect".
> But when you do it your answer will be "correct".

because his program, by its structure, gives up and gets the wrong answer.

If he wrote is program diferently, to not give up, then that program
fails by not answering at all, becuase it then gets a DIFFERENT input
based on this new machine.

This new input actually needs a decider that recognize the infinite
behavior pattern that now exists in the program.

>
> What are you using as a correctness-decider ?!?

I show that the program halts by just running it.

>
>> Note, there are patterns that are provably non-halting, for instance,
>> any Turing Machine that returns to an exact state (including the
>> contents and placement of the tape) MUST continue on the same path it
>> did last time, and thus we can prove by induction that it will never halt.
> But that's PRECISELY what Olcott's halt-decider does?!?!?!
>
> It observes the stack trace. Sees that the state machine calls the same function with the same parameters TWICE and aborts because it has detected an infinite loop.

Which isn't an actual non-halting pattern. it ignores the behavior of
the copy of itself, and thus gets the wrong answer.

>
> YOU are the one who keeps calling that "incorrect" but here you are now advocating for it ?!?!?

Because I an not using that same patttern. You are just showing your
ignorance in thinking I am.

>
>
>>> If P hasn't yet halted but could in future WHEN do you assert that H was "incorrect" ?
>>
>> Irrelevent to the point you are refering to, since that case was
>> assuming that H answered Halting and WAS correct.
> 100% relevant. I am asking you to tell us (and you continue to refuse) HOW you've determined the "correctness".

Then READ the proof I quoted.

>
> Which decider did you use?

VALID LOGIC.

Note, I am NOT claiming it to be a decider, because it doens't handle
ALL cases, just THIS case.


>
>> You are asking about the case BELOW, and as I mentioned just above,
>> there are SOME cases you can prove that a program will never halt.
> HOW DO YOU KNOW which case we find ourselves in?
>
> Without a correctness-decider we could be dealing with the case where "H answers Halting, and that's correct" OR the case where "H answers Halting, and that's incorrect"
>
> HOW DO YOU KNOW which case you are in ?!?!?

You might not. But you do SOMETIMES, which is often good enough.

You seem to have a failure to understand the difference between a case
and in general.

>
>> So, you don't understand how induction can be used to prove something in
>> a finite number of steps about an infinite set?
> Oh, I think I understand just fine!
>
> Inductive/recursive proofs don't halt.
> Co-inductive/co-recursive proofs halt.
>

No, at least the definitions I work with, and "Inductive Proof" has two
steps.

1) Prove that the thing is true for a starting case N.

2) Prove that if it is true for case n, for every n >= N, that it is
true for case n+1.

Then, but the induction proof, it has been proved true for ALL n >= N

>
>> I am not writing "Programs", I am talking about PROOF,
> PROOFS ARE PROGRAMS. Two different words for the exact same Mathematical object.

Nope, you misusing the terms, showing your ignorance.

>
> So you are talking about the same thing using two different names.
>
>> Because D isn't built to contradict me.
> D is built to contradict its appointed halt-decider.
>
> If YOU are the appointed halt decider (and not H) then D is built to contradict YOU (and not H).

Right, but it wasn't.

>
> If D doesn't contradict you - then you are not the halt-decider for D.

I am not the APPOINTED Halt Decider that it is proving incorrect.

I can still be able to decide on D. D has no magical power that keeps
otehr deciders from being able to decide it, it specificaly makes it so
that its appointed decider will be wrong about it.

>
> You know. By definition...

You seem to have your definitions mixed up.

>
>> Yes, there are some programs that I will be unable to decide on, but
>> because I can see the relationship between H and D, and can use logic
>> based on that.
> Proofs. Programs. Logic. Same thing.

Nope, as proven by logic.

>
>> Not to me. Maybe you are limiting your thinking to programatic proofs.
> I am "limiting my thinking" to the general concept of proof. As captured in proof theory.
>
> If you have any broader and more comprehensive notion/conceptions of "proof" - by all means. Share it with us.

A proof is just a sequence of know true statements, combined by known
true operations, that result in showing that desired statement is true.

>
>
>> I didn't say I was using a program, I used a PROOF, using the knowledge
>> of the construction of D.
> Proofs ARE programs. Different words for the same construct!

Nope, shows you don't understand the meaning of the words.

>
> So you didn't say you are using a program/proofs, you used a program/proof.

Nope,

>
> Idiot.


Thats YOU, who doesn't know the DIFFERENCE between a program and a proof.


>
>> So, it seems your logic system has no concept of things being actually
>> true or proven. If you can't believe your own proof, you know nothing.
> Bullshit. That is ALL my logic has.
>
> You give inputs to functions - they produces outputs. If the input "2+2=5" produces the output "true" then the string "2+2=5" has been proven true.

That just shows that programs are not proofs. BY DEFINITION, since a
program can say that 2+2=5 is True, and we know that it is not, then
programs are not proofs.

>
> Whether that proof is "correct"... I don't know. My logic is incomplete with respect to correctness.

Yep, that is your problem, you are working in a logic system that has no
knowledge, and thus can't actually determine anything.

>
>> When I can actually prove them. Everything actually Proven is True.
> What nonsense. Everything that's Proven is Proven. Be it proven true; or proven false; or proven a Boolean. Or proven a Number. Or proven Halting.

No, that which is proven is proven true. The statement proven might be a
statement that some other statement is false, in which case that other
statement is shown to be false, or DISPROVEN.


>
>> Right, the program mentioned is know to Halt, and that can be proven by
>> just running it and seeing that it does halts.
> Which is exactly what Olcott's H does. Yet you disagreed with it.

No, Olcott's program aborts its simulation of the program before it gets
to the end before it gets to the end, because that is how it has been
programmed.

Run his program and see what it does.

>
>> I note you are taking answers out of context, showing you are being a
>> DECEPTIVE Skep Dick
> I am NOT taking the answers out of context. So it must be you who's being deceptive.

Then why is the statement I was answerering, the CONTEXT of the
statement, no longer there.

That shows you have taken it out of context, and thus proves you are a
liar (or just totally stupid).

>
>> No, the simulation Halt-decider aborted its simulation to give the
>> non-halting answer.
> Yes. Because it does proof-by-induction. It detected the program returning to the same state twice.
>
> You literally just said that you can prove things about infinite objects in finite time. But now ?!?!?

proof-by-induction

>
>> I didn't, and because the program isn't based on me, we don't get the problem that H runs into.
> Oh, so you didn't abort the program after N steps? You ran it for infinitely-many steps?

No, it reaches it final state in a finite number of steps.

Since his H DOES abort its simulation, because it INCORRECTLY thinks
that the program will run forever, and returns that answer, it makes the
actual program halting and halts in a finite number of steps.

It Halts BECAUSE H makes that mistake.

>
>
>> By Inspecting of P, P(P) will Halt if H(P,P) returns non-halting (in the
>> Turing Machine case, a final state of P is the exact state of the final
>> state of H that reports non-halting).
> What sort of "inspection" are YOU performing that you can't give us programmatically - in source code ?!?!

Can YOU provide the source code of the program you are using to make you
statements?

This just proves the error in your concept that all proofs are just
programs.

>
>> Since it is claimed that H(P,P) will "correctly" return Non-Halting, we
>> see that that can't be correct, as if H(P,P) returns non-halting P(P)
>> will Halt.
> What is it that you think you can "see" that H cannot "see" !?!?!

The problem is that "Programs" can't actually think, but just process.
There process is defined when the program is created. P is defined to
use that processing of H to make sure that H's processing can't give the
correct answer.

Since this P wasn't built on my processing, and in fact, MY processing
comes AFTER P is created, so it can't be, I can see, at least in this
case, the results of what P will do.

The concept of giving "will" to programs is incorrect.

>
>> We can then go father and show that if H(P,P) returns Halting, that P(P)
>> will not halt, as by constuction, the final state of H that reports
>> non-halting has been converted into an infinite loop, which will clearly
>> never halt.
> "We" ?!?! So we are, in fact doing a step-trace execution of H(P,P) ?!?!?!
>
> EXACTLY like Olcott is doing?!?

Except that since the input is based to confound me, I can get the right
answer.

Note, we are "step tracing" the INPUT to H(P,P) which is P(P), and
noting that the H that P calls makes a decision based on incorrect
rules, and we the see that it reaches the end.

>
>> Since by requirement, H to give a correct answer must do one of the two
>> above behaviors, it will ALWAYS be wrong.
> Holy shit dude, you keep spinning in circles.
>
> HOW DO YOU KNOW that H gave you an "incorrect" answer?
> HOW did you obtain the "correct" one

I have told you but you are obviously too stupid to understand.

I ran P(P) and it halted, this it is proven to be a Halting Computation.

Since H says P(P) is non-halting, it is wrong,

And you are proven STUPID.

>
> Without the a priori knowledge of WHICH answer is "correct"; and WHICH answer is "incorrect" you can't possibly decide that H is correct; or incorrect.

Why do I need a priori knowledge? I can determine it after the fact, and
in fact, that is part of the logic of the proof. Since I know that for
ANY program H that can possible be thought of, there are only a finite
number of option classes it can result in, and for each of these
options, by the design of ths template H^, I can show that the answer
given by that H will be wrong, I can prove that no H can give the
correct answer.

>
> So WHERE did you get the knowledge from if not H?

By looking at the program that it is deciding on, which depends on what
H does.

>
>>>> For the original proof
>>> In what programming language are you going to present this "proof"?
>>
>> LOGIC.
> WHICH ONE?
>

The CORRECT ONE.

>>>> we can also prove that the H^ program WILL be non-halting if the H is shown to return Halting for H applied to H^ H^
>>> In what programming language are you going to present this "proof"?
>>>
>>
>> LOGIC.
> WHICH ONE?

Obviously not yours.

>
>>>> so we can actually PROVE that IF it gives an answer
>>> In what programming language can we PROVE this?
>>>
>>
>> LOGIC.
> WHICH ONE?
>
>
>> Right, so there exists SOME programs and statements that can not be
>> decided if they will Halt or are incorrect.
> Right! So is your assertion that H is "incorrect" one of those programs; or not?!?
>
> Is your assertion about the incorrectness of H correct or incorrect?

It has been PROVEN correct, i.e H must have been incorrect in its answer.

>
>>>> To disprove a machine from being a Halt Decider, since that requires
>>> In what programming language are you going to disprove this?
>>
>> LOGIC. Maybe you don't understand it, because it predates you.
> WHICH ONE?
>
> I keep asking you this because there are hundreds of different logics!
>
> Classical. Intuitionistic. Temporal. Linear. Many-sorted. Many-valued. Boolean. Ternary. Infinitary.
>
> Maybe you don't understand because you just don't understand anything?

I used the FORMAL LOGIC defined in Computation Theory, of course. What
else is ALLOWED for a statement in a Formal Logic?

Mr Flibble

unread,
Dec 3, 2022, 9:49:32 AM12/3/22
to
GET A BETTER HOBBY, MATE.

/Flibble

Skep Dick

unread,
Dec 3, 2022, 3:08:59 PM12/3/22
to
On Saturday, 3 December 2022 at 16:14:27 UTC+2, richar...@gmail.com wrote:
> No, I have a "PARTIAL Correctness-Decider", that can handle THIS
> particular case.
Where is it?

> Remember, the definition of a "Decider" is a machine that handles ALL
> cases. We don't need such a machine for this, just one that can handle
> THIS case.
Lucky you - I wasn't asking for a general-decider. I'm asking you for a particular-decider.
One for THIS particular case.

Where is it?

> And the problem is that one case can possible take infinite time, which
> isn't allowe.
This is so weird. Why are you talking in the abstract? I am asking you about THIS particular case so...

Can or does take infinite time?

> That has been explaied to you several times, but you seem to dense to
> understand that.
You are too dense to understand that I never asked you to explain it.

I am only asking you for the source code of your decider which has determined that Olcott's H is "incorrect".

> > Show me your correctness decider.
> I don't think you would understand the math needed for that sort of proof.
So is that an actual admission that you don't know whether "4" is the correct answer to "2+2"?

> Note also, that isn't the question that I was talking about, so my
> partial decider doesn't need to work on it
Sure. But your partial decider does need to work on the question "Is Olcott's H correct or incorrect?"

And since you've been asserting its "incorrectness"... where is the source code?

> > But I am not asking you to PROVE the answer ?!?! I am asking you to VERIFY whether a given answer is correct!
> And what is the difference between PROVING something and VERIFYING it?
Tremendous. A verification checks THAT X is the correct answer. ; A proof shows WHY X is the answer.

> Both are showing steps that demonstrate that the statement must be true.
So you don't actually understand the difference between claiming THAT 2+2 is 4 and claiming WHY 2+2 is 4. Wow!

> > HOW have you verified this?
> Because I have a valid proof of it.
Rinse repeat. You may or not have a proof of it, but how exactly have you verified the "validity" of your proof?

> If you don't believe in proofs, then you can't actually know anything.
I'll believe it when I see it.

Where is the proof?

> > HOW do YOU know whether a proof halts or not ? Given that you don't have a working halt-decider - HOW do you keep acquiring this knowledge?
> Because I reached the end of it and it became final.
In which runtime did you execute your proof?

> >
> >> You seem to be having a comprehension issue.
> > Not me... It's definitely you.
> Nope. Its you. You are even showing that you don't understand the
> difference between proving one case and solving the general.
See! It's **definitely** you. I am only talking about a single case here - the case at hand.

> > OK. HOW do you show that?
> As I said, run it and see that it reaches a final state.
OK. So where is the proof that you ran? Show it to us.

> For someone who claims that proofs are programs, no understanding that
> the can actually be run to see they reach a final state seems utterly
> stupid.
Of course I understand that. I also understand that since you are the one who claims "incorrectness" you must have already run the proof which told you that Olcott's H is incorrect.

Where is the proof?

> > HOW do you know that the final state is reached?
> Because it DID when I ran it.
Great! Show us the proof that you ran.

> Reality IS a proof.
That's a religious claim.

> I gave you a proof that wasn't a program (but perhaps could be converted into a program)
You didn't "give me a proof that wasn't a program", you didn't give me any proof.

> have demonstated that you statement is FALSE, and you are ignorant.
You've done no such thing. Maybe in your head... A space nobody gives a shit about.

> > And far more importantly - I am asking you to explain HOW you've come to know that you knowledge is "correct"
> I've done it, but it seems to be beyound your understanding.
No, you haven't .You keep talking but you've provided no proof.

> > What if you have "proven" that a program halts, but your proof is wrong?
> I used only demonstartably correct steps, so the proof is valid.
How do you know that you steps are "correct"? Maybe you are mistaken.

> IF you want to challange my proof, show the incorrect step I used.
Sure! Where is the proof you want me to examine?

> You seem to have a fundamental problem with knowing what Truth is.
Ooooh. You think you know what Truth is?

> This is one of the problems of thinking of Proofs as Programs when you
> start to try to reason about Programs. Proofs, when built by the rules,
> are necessarily correct, just like a program will always produce the
> answer that that program produces.
I have no idea why you are using the word "correct" here.

Yes. A program produces the output that it produces.
Yes. A program follows rules.
Yes. A program can apply any rule at any time.
Yes. A program will produce the answer the programmer made it produce.

What I am still not clear about is why you think that answer is "correct".

> > I asked you whether the "correctness" of a halt-decider is decidable.
> And, as I have explianed, often yes, but there are cases where it can't
> be, thus, in it is not decidable in general.
I didn't ask you about the general case? I am asking you about **this** particular case.

Given the source code for Olcott's H, and the source code for P; and the output of H(P,P).

Produce the decider C (for correctness) such that C(H, P, result_of_H) determines whether the result of H is "correct".

> You seem to have a problem understanding that undecidable in general
> still allows the proposition to be able to be decided for many specific
> cases.
You really seem to have a problem with particulars.

> That is a funny thing about unknowability. We know that some things are
> unknowable, but in many cases we can't prove that a particual something
> is unknowable, becuase by its nature, if we knew we couldn't prove its
> answer, we would know the answer.
There you go again about generalities. In the particular case of this particular context given Olcott's particular decider and particular result - you've called a bunch of things "knowable" and "unknowable".

> Halting is a property like that. If we KNEW that the halting status of a
> given machine/input combination was proved to be "Unknowable", then we
> would know that it must be non-halting
🤣🤣🤣🤣🤣🤣🤣 maybe you want to read that again.

If you proved halting to be unknowable then you would know that the unknowable halting status is non-halting.

🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣

I don't know how to say it more plainly. You are not smart.

> Thus if we could somehow proof that we can't do that, it means by
> definition, the machine must never stop, so ALL unknowable Halting
> problems must be non-halting
🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣

I don't know how to say it more plainly. You are not smart.

> >> If the program WILL Halt, then by running it, we will see that and PROVE
> >> that it halts.
> > But that's exactly what Olcott's simulating halt-decider does!!!!
> Nope, and that is his flaw. He runs it for a while, until it meets a
> condition that he THINKS (incorrectly) shows non-halting behavior, then
> he stops.
The condition Olcott's decider uses is **precisely* YOUR condition for an inductive proof.
He sees it doesn't halt in N steps.
He sees it doesn't halt in N+1 steps.
By detecting the recursive call he inductively concludes that it doesn't halt. Ever.

You are so stupid you don't even understand that by disagreeing with Olcott's H you are disagreeing with yourself.

> > How is it that when he does it his answer is "incorrect".
> > But when you do it your answer will be "correct".
> because his program, by its structure, gives up and gets the wrong answer.
Obviously it "gives up"! Your inductive proof also "gives up"! ALL inductive proofs "give up"!

Literally, you are only proving N and N+1.
You are NOT proving N+2, and N+3, and N+4.... ad infinitum.

Are you now saying that you use an inductive proof to prove that P doesn't halt?
It's pretty weird - because you are disagreeing with yourself.

> If he wrote is program diferently, to not give up, then that program
> fails by not answering at all, becuase it then gets a DIFFERENT input
> based on this new machine.
Translation: If he DIDN'T use an inductive proof.

This is really weird. You said you are using an inductive proof. And you said it's "correct".

> This new input actually needs a decider that recognize the infinite
> behavior pattern that now exists in the program.
This is really weird! You said you are using an inductive proof to prove properties of infinite sets in finite time.

But you also said it's "incorrect" to "give up" ?!?!?

You really are disagreeing with yourself!

> > What are you using as a correctness-decider ?!?
> I show that the program halts by just running it.
But you said the assertion "P halts" was incorrect ?!?!

> >> Note, there are patterns that are provably non-halting, for instance,
> >> any Turing Machine that returns to an exact state (including the
> >> contents and placement of the tape) MUST continue on the same path it
> >> did last time, and thus we can prove by induction that it will never halt.
> > But that's PRECISELY what Olcott's halt-decider does?!?!?!
> >
> > It observes the stack trace. Sees that the state machine calls the same function with the same parameters TWICE and aborts because it has detected an infinite loop.
> Which isn't an actual non-halting pattern. it ignores the behavior of
> the copy of itself, and thus gets the wrong answer.
So you agree that YOUR strategy (which is EXACTLY THE SAME as Olcott's strategy) doesn't work?!?!?

> > YOU are the one who keeps calling that "incorrect" but here you are now advocating for it ?!?!?
> Because I an not using that same patttern. You are just showing your
> ignorance in thinking I am.
The way you described you are using EXACTLY THE SAME pattern!

You are using proof by induction. Which means you are going to extrapolate an infinite conclusion from finite observations!

So why are you disagreeing with Olcott if you are doing exactly the same thing as him?

> Then READ the proof I quoted.
You haven't quoted any proofs. Certainly nothing I can run on my own computer.

> > Which decider did you use?
> VALID LOGIC.
Which decider did you use to decide that your logic is "valid" ?!?!

> > Without a correctness-decider we could be dealing with the case where "H answers Halting, and that's correct" OR the case where "H answers Halting, and that's incorrect"
> >
> > HOW DO YOU KNOW which case you are in ?!?!?
> You might not. But you do SOMETIMES, which is often good enough.
Why are you speaking in general terms when we are dealing with a concrete case ?!?!

In particular: either you know or you don't know. There is not "might" ?!?!

> You seem to have a failure to understand the difference between a case
> and in general.
No, I don't! The failure in understanding all yours.

> >> So, you don't understand how induction can be used to prove something in
> >> a finite number of steps about an infinite set?
> > Oh, I think I understand just fine!
> >
> > Inductive/recursive proofs don't halt.
> > Co-inductive/co-recursive proofs halt.
> >
> No, at least the definitions I work with, and "Inductive Proof" has two
> steps.
>
> 1) Prove that the thing is true for a starting case N.
>
> 2) Prove that if it is true for case n, for every n >= N, that it is
> true for case n+1.
> Then, but the induction proof, it has been proved true for ALL n >= N

So you are going to "give up" after only one step ?!?!? Didn't you just say that's "incorrect"?

🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣
🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣
🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣🤣

Olcott's proof is inductive.

He shows a function call at Time t=0 (N)
He shows a duplicate function call at Time t=1 (N+1)
This proves that the function loops/recurses for ALL n >= N
You said that's "incorrect". But now that's "correct".

Why are you disagreeing with yourself?


> >> I am not writing "Programs", I am talking about PROOF,
> > PROOFS ARE PROGRAMS. Two different words for the exact same Mathematical object.
> Nope, you misusing the terms, showing your ignorance.
Accusation in a mirror.

I think it's become pretty clear who the ignorant idiot in this conversation is.


> > So you are talking about the same thing using two different names.
> >
> >> Because D isn't built to contradict me.
> > D is built to contradict its appointed halt-decider.
> >
> > If YOU are the appointed halt decider (and not H) then D is built to contradict YOU (and not H).
> Right, but it wasn't.
> > If D doesn't contradict you - then you are not the halt-decider for D.
> I am not the APPOINTED Halt Decider that it is proving incorrect.
Then obviously you will ALWAYS get the wrong answer!!!

If D only contradicts H, but it doesn't contradict YOU then D is non-deterministic!!!

Nobody gives a shit what D does from your perspective.
We want to know what D does from H's perspective.

> I can still be able to decide on D. D has no magical power that keeps
> otehr deciders from being able to decide it, it specificaly makes it so
> that its appointed decider will be wrong about it.
So you are openly admitting that you are wrong about D ?

> You seem to have your definitions mixed up.
You seem to have your "you" mixed up. You should have said "I seem to have my definitions mixed up".

You really are incompetent at identity. Equality. Same thing.

> > Proofs. Programs. Logic. Same thing.
> Nope, as proven by logic.
See! You are even confused when to say 'Nope' and when to say 'I agree'.

> > If you have any broader and more comprehensive notion/conceptions of "proof" - by all means. Share it with us.
> A proof is just a sequence of know true statements, combined by known
> true operations, that result in showing that desired statement is true.
You are describing a program....

> >> I didn't say I was using a program, I used a PROOF, using the knowledge
> >> of the construction of D.
> > Proofs ARE programs. Different words for the same construct!
> Nope, shows you don't understand the meaning of the words.
Then why did you just describe a proof as "sequence of know true statements, combined by known true operations"

That's a program, you know.

> Thats YOU, who doesn't know the DIFFERENCE between a program and a proof.
Of course I know the difference. I know that there is no difference.

> That just shows that programs are not proofs. BY DEFINITION, since a
> program can say that 2+2=5 is True, and we know that it is not, then
> programs are not proofs.
You are contradicting yourself. You said that applying the rules to the inputs produces the result that it produces!

If we apply the rules of +(p,q) to the inputs p=2; q=2 and those rules produce the answer 5 then what are you disagreeing with ?!?!

> Yep, that is your problem, you are working in a logic system that has no
> knowledge, and thus can't actually determine anything.
See! You are mixing up your "you" again! YOUR logic system has no knowledge either.

Logic contains no knowledge. Knowledge is an input to logic.

> >> When I can actually prove them. Everything actually Proven is True.
> > What nonsense. Everything that's Proven is Proven. Be it proven true; or proven false; or proven a Boolean. Or proven a Number. Or proven Halting.
> No, that which is proven is proven true.
That's a conceptual error. Why are conflating provability and truth?

>The statement proven might be a statement that some other statement is false, in which case that other statement is shown to be false, or DISPROVEN.
I don't know how else to say it to you... You are not smart. And I am starting to suspect that you may actually be quite stupid.

We prove that 2+2 is 4.
We don't prove that 2+2 is true.

> > Which is exactly what Olcott's H does. Yet you disagreed with it.
> No, Olcott's program aborts its simulation of the program before it gets
> to the end before it gets to the end, because that is how it has been
> programmed.
Obviously! Because it does a proof by induction! You abort after N and N+1!

Are you disagreeing with yourself again? Are you now saying that we have to do N+2, and N+3, and N+4... ad infinitum?

> Run his program and see what it does.
I did. It does a proof by induction.

It proves that the function gets called with some parameters at time N
It proves that the function gets called with the same parameters at time N+1
This inductively proves a loop.

The only possible reason you could be disagreeing with Olcott if you believed that his inductive proof is insufficient. But you are peddling an inductive proof yourself.

So why are you disagreeing?

> > I am NOT taking the answers out of context. So it must be you who's being deceptive.
> Then why is the statement I was answerering, the CONTEXT of the
> statement, no longer there.
Because I deleted the instance of it in this particular reply. But the CONTEXT is still there because the entire history of the conversation is still there.

> That shows you have taken it out of context, and thus proves you are a
> liar (or just totally stupid).
Q.E.D You are confusing your "you" again.

> > Oh, so you didn't abort the program after N steps? You ran it for infinitely-many steps?
> No, it reaches it final state in a finite number of steps.
Obviously! ALL proofs by induction do that! Because proofs by induction only perform TWO steps.

Proof for N.
Proof for N+1

Your intellectual dishonesty and double standards are really starting to shine.

You want your inductive proofs to be finite, but you want Olcott's inductive proofs to be infinite.

> Since his H DOES abort its simulation, because it INCORRECTLY thinks
> that the program will run forever
Why is the thinking "incorrect"?!?! It's proven by induction that the program will run forever.

>and returns that answer, it makes the actual program halting and halts in a finite number of steps.
Yes. Because it's proof by induction.

> It Halts BECAUSE H makes that mistake.
It Halts BECAUSE H completed its proof by induction.

Why is the proof by induction "mistaken"?!?

> > What sort of "inspection" are YOU performing that you can't give us programmatically - in source code ?!?!
> Can YOU provide the source code of the program you are using to make you
> statements?
Of course I can. But they would be useless to you - you don't have access to my runtime.

> This just proves the error in your concept that all proofs are just programs.
Looks like your "proof" is wrong.

> > What is it that you think you can "see" that H cannot "see" !?!?!
> The problem is that "Programs" can't actually think, but just process.
Thinking. Processing information.

Potato/potatoh.

> There process is defined when the program is created. P is defined to
> use that processing of H to make sure that H's processing can't give the
> correct answer.
It seems you have yourself a conflict of definitions.

P is defined to prevent H from getting the correct answer.
H is defined to always get the correct answer.

Which definition is "right"? Hint: Whichever definition you choose as authoritative.

> The concept of giving "will" to programs is incorrect.
That sure seems like a double standard..

Why is the concept of giving "will" to minds correct; but the concept of giving "will" to programs incorrect.

Sure seems to me you think your mind is special.

> > EXACTLY like Olcott is doing?!?
> Except that since the input is based to confound me, I can get the right
> answer.
Hahahahaha. So you do think you are special! You can get the right answer but H can't.

Why is it then that you can't explain to your computer how to get the right answer also?
If you know how - program your computer to do exactly the same thing you are doing.

> Note, we are "step tracing" the INPUT to H(P,P) which is P(P), and
> noting that the H that P calls makes a decision based on incorrect
> rules, and we the see that it reaches the end.
So correct the rule. You know how, right?

> > HOW DO YOU KNOW that H gave you an "incorrect" answer?
> > HOW did you obtain the "correct" one
> I have told you but you are obviously too stupid to understand.
Yeah. I must be "too stupid" to understand how you keep making decisions that you can't explain to a computer.

> I ran P(P) and it halted, this it is proven to be a Halting Computation.
> Since H says P(P) is non-halting, it is wrong,
This is not valid critique. You simply waited longer.

Why did you keep waiting for P to halt when an inductive proof told you that P won't halt?!?

> And you are proven STUPID.
Yes, you are. Your inductive proof told you that P won't halt, but you kept waiting anyway.

Seems to me you don't believe your own proofs.

> > Without the a priori knowledge of WHICH answer is "correct"; and WHICH answer is "incorrect" you can't possibly decide that H is correct; or incorrect.
> Why do I need a priori knowledge? I can determine it after the fact, and in fact, that is part of the logic of the proof.
What do you mean by "after the fact" when you speak of a non-terminating program?!?!?

It sure sounds like you are looking past the end of infinity somehow.

> > So WHERE did you get the knowledge from if not H?
> By looking at the program that it is deciding on, which depends on what H does.
I don't understand. Both you and H have access to EXACTLY THE SAME information!

You have access to P and H's source code.
H has access to P and its own source code.

What is it that you can "see" in the source code that H cannot ?!?

> >> LOGIC.
> > WHICH ONE?
> >
> The CORRECT ONE.
So you've been committing the petitio principii fallacy all along?

Because you still haven't produced a method/process for deciding what makes a logic "correct".

> >> LOGIC.
> > WHICH ONE?
> Obviously not yours.
It's weird how you can't give a particular answer. Isn't it?

Skep Dick

unread,
Dec 3, 2022, 3:31:17 PM12/3/22
to
On Saturday, 3 December 2022 at 16:14:27 UTC+2, richar...@gmail.com wrote:
> > I asked you whether 4 is the correct answer to 2+2.
> >
> > Show me your correctness decider.
> I don't think you would understand the math needed for that sort of proof.
While we are at it... Here is the proof that I "wouldn't understand". In Agda.

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _∎)

data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

_ : 2 + 2 ≡ 4
_ =
begin
2 + 2
≡⟨⟩ -- is shorthand for
(suc (suc zero)) + (suc (suc zero))
≡⟨⟩ -- inductive case
suc ((suc zero) + (suc (suc zero)))
≡⟨⟩ -- base case
suc (suc (suc (suc zero)))
≡⟨⟩ -- is longhand for
4

olcott

unread,
Dec 3, 2022, 3:36:13 PM12/3/22
to
Or more directly:
Successor(Successor(0)) + Successor(Successor(0)) =
Successor(Successor(Successor(Successor(0))))

Richard Damon

unread,
Dec 3, 2022, 3:36:34 PM12/3/22
to
On 12/3/22 3:08 PM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 16:14:27 UTC+2, richar...@gmail.com wrote:
>> No, I have a "PARTIAL Correctness-Decider", that can handle THIS
>> particular case.
> Where is it?

I listed it. You obviously can't read "logic" I see.

Your INCORRECT insistance that a proof must be a program means (it
seems) that ALL the rest of your points are incorrect.

Sorry, you are showing your self to be TOO DUMB, perhaps intentionally,
so bye.

Skep Dick

unread,
Dec 3, 2022, 3:49:25 PM12/3/22
to
On Saturday, 3 December 2022 at 22:36:34 UTC+2, richar...@gmail.com wrote:
> On 12/3/22 3:08 PM, Skep Dick wrote:
> I listed it. You obviously can't read "logic" I see.
I've seen no proof; or logic (same thing, really).

All I've seen is you rambling in English.

> Your INCORRECT insistance that a proof must be a program means (it
> seems) that ALL the rest of your points are incorrect.
You are incorrect about me being incorrect.

Welcome to The Simulation.

> Sorry, you are showing your self to be TOO DUMB, perhaps intentionally,
> so bye.
And you are still projecting.

Richard Damon

unread,
Dec 3, 2022, 3:56:00 PM12/3/22
to
but you never showed that suc
((suc zero) + (suc (suc zero)))
is
suc (suc (suc (suc zero)))

So all you did was do a change of representation and then assumed that
2+2 = 4

You are just assuming that your TOOL knows how to do it.

olcott

unread,
Dec 3, 2022, 4:01:01 PM12/3/22
to
He has a masters in EE from MIT so he is not stupid.
When someone with those credentials makes such a "stupid"
mistake and we rule our {stupid} what does that leave?

Richard Damon

unread,
Dec 3, 2022, 4:03:30 PM12/3/22
to
On 12/3/22 3:49 PM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 22:36:34 UTC+2, richar...@gmail.com wrote:
>> On 12/3/22 3:08 PM, Skep Dick wrote:
>> I listed it. You obviously can't read "logic" I see.
> I've seen no proof; or logic (same thing, really).
>
> All I've seen is you rambling in English.
>

Yes, Proofs are often written in a Formal Version of Natural Language,
like English.

>> Your INCORRECT insistance that a proof must be a program means (it
>> seems) that ALL the rest of your points are incorrect.
> You are incorrect about me being incorrect.
>
> Welcome to The Simulation.
>
>> Sorry, you are showing your self to be TOO DUMB, perhaps intentionally,
>> so bye.
> And you are still projecting.

And you are still being a DICK, and WRONG.

Skep Dick

unread,
Dec 3, 2022, 4:15:22 PM12/3/22
to
On Saturday, 3 December 2022 at 22:56:00 UTC+2, richar...@gmail.com wrote:
> So all you did was do a change of representation and then assumed that
> 2+2 = 4
Huh? You fucking idiot!

You know the first axiom of logic? Identity.
You know that second axiom of logic? Excluded middle.

Either 2+2 is identical to 4 OR 2+2 is NOT identical to 4.

I just proved WHICH disjunct is true.

olcott

unread,
Dec 3, 2022, 4:26:11 PM12/3/22
to
2+2 is a numerically equivalent encoding of 4.

Skep Dick

unread,
Dec 3, 2022, 4:31:27 PM12/3/22
to
On Saturday, 3 December 2022 at 23:03:30 UTC+2, richar...@gmail.com wrote:
> Yes, Proofs are often written in a Formal Version of Natural Language,
> like English.
You seem ignorant of formal semantics: https://en.wikipedia.org/wiki/Formal_semantics_(natural_language)

The structure of your English "proof" always reduces to a formal proof.

A program.

> And you are still being a DICK, and WRONG.
You know what I think bothers you most? I think it's the logical connective...

Your brain really wanted me to be a dick OR be right.
Your brain wasn't ready for me being a dick AND being right.

Skep Dick

unread,
Dec 3, 2022, 4:34:30 PM12/3/22
to
On Saturday, 3 December 2022 at 23:26:11 UTC+2, olcott wrote:
> 2+2 is a numerically equivalent encoding of 4.
But that's just a proposition.

You are proposing that there is an equivalence relation between 4 and 2+2.
You are proposing THAT 2+2=4.

Prove it.


Richard Damon

unread,
Dec 3, 2022, 4:38:46 PM12/3/22
to
No, you did neither.

A PROPER proof is

We want to Show 2+2 = 4

Representation 2 = S(S(0))

So we have 2+2 = S(S(0)) + S(S(0))

Axiom: S(a) + b = S(a+b)
a = S(0), b = S(S(0)) so we have

2+2 = S( S(0) + S(S(0)))

doing it again with
a = 0, b = S(S(0)) we get

2+2 = S( S(0 + S(S(0)))

Axiom: 0 + x = x, we get

2+2 = S( S( S(S(0))))

Which is 4 by representation.

so 2+2 = 4

You missed all the steps in the middle which do the actual PROOF.



olcott

unread,
Dec 3, 2022, 4:46:27 PM12/3/22
to
On 12/3/2022 3:15 PM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 22:56:00 UTC+2, richar...@gmail.com wrote:
>> So all you did was do a change of representation and then assumed that
>> 2+2 = 4
> Huh? You fucking idiot!
>
> You know the first axiom of logic? Identity.
> You know that second axiom of logic? Excluded middle.
>
> Either 2+2 is identical to 4 OR 2+2 is NOT identical to 4.
>

NEITHER: 2+2 is a numerically equivalent encoding of 4.

Skep Dick

unread,
Dec 3, 2022, 4:49:48 PM12/3/22
to
On Saturday, 3 December 2022 at 23:38:46 UTC+2, richar...@gmail.com wrote:
> A PROPER proof is
>
> We want to Show 2+2 = 4
>
> Representation 2 = S(S(0))
Sorry. You'll have to define =, S and 0.

Like I did.

Skep Dick

unread,
Dec 3, 2022, 4:53:33 PM12/3/22
to
On Saturday, 3 December 2022 at 23:46:27 UTC+2, olcott wrote:
> > Either 2+2 is identical to 4 OR 2+2 is NOT identical to 4.
> >
> NEITHER: 2+2 is a numerically equivalent encoding of 4.
Idiot. The symbol "=" represents an equivalence relation.

When you substitute "is a numerically equivalent encoding of" for "=" into "2+2 is a numerically equivalent encoding of 4"
you get EXACTLY 2+2=4

olcott

unread,
Dec 3, 2022, 5:06:14 PM12/3/22
to
On 12/3/2022 3:53 PM, Skep Dick wrote:
> On Saturday, 3 December 2022 at 23:46:27 UTC+2, olcott wrote:
>>> Either 2+2 is identical to 4 OR 2+2 is NOT identical to 4.
>>>
>> NEITHER: 2+2 is a numerically equivalent encoding of 4.
> Idiot. The symbol "=" represents an equivalence relation.
>

Hence not the {identical to} relation.
string_length("2+2") != string_length("4") thus not identical

> When you substitute "is a numerically equivalent encoding of" for "=" into "2+2 is a numerically equivalent encoding of 4"
> you get EXACTLY 2+2=4

Skep Dick

unread,
Dec 3, 2022, 5:36:41 PM12/3/22
to
On Sunday, 4 December 2022 at 00:06:14 UTC+2, olcott wrote:
> Hence not the {identical to} relation.
> string_length("2+2") != string_length("4") thus not identical
Idiot. Do you actually understand the difference between syntax and semantics?

The symbolic expression 2+2 and the symbolic expression 4 point to the exact same semantic object. They are identical. De-reference the pointers first.

identity is equivalent to equivalence. Univalence axiom... (A = B) ≃ (A ≃ B)

Richard Damon

unread,
Dec 3, 2022, 5:37:07 PM12/3/22
to
I figured you could understandthe meaning of the terms from the
predefioned terms of the theory.

At least in my number theory classes, 0, =, and 'S' as a symbol for the
successor function were assumed symbols.

Maybe I overestimated your intelegence.

Or maybe it shows the problem with assuming proofs actually need to be
writtten as programs.
It is loading more messages.
0 new messages