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 ?!?!

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...

On Fri, 02 Dec 2022 22:20:08 -0800, Skep Dick wrote:

> 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...

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

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?

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.

On Sat, 03 Dec 2022 09:14:21 -0500, Richard Damon wrote:

> 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?
>
>
>>>>> 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.
>>

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.

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

On 12/3/2022 2:31 PM, Skep Dick wrote:
> 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

Or more directly:
Successor(Successor(0)) + Successor(Successor(0)) =
Successor(Successor(Successor(Successor(0))))

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

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.

>
>> 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?

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.

On 12/3/22 3:31 PM, Skep Dick wrote:
> 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

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.

On 12/3/2022 2: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?
>
>> 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.
>

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.

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.

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.
>
> I just proved WHICH disjunct is true.

2+2 is a numerically equivalent encoding of 4.

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

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.

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.

On 12/3/22 4: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.
>
> I just proved WHICH disjunct is true.

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.

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.

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

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.

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

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

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

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)

On 12/3/22 4:49 PM, Skep Dick wrote:
> 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.
>

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.