Richard Damon <Richard@Damon-Family.org> writes:

> On 10/24/21 6:27 PM, olcott wrote:
>> On 10/24/2021 10:23 AM, Ben Bacarisse wrote:
>>> olcott <NoOne@NoWhere.com> writes:

>>>> The words above are like say that when we know that we have a black
>>>> cat then we know that we have a cat, and yet you still disagree.
>>>
>>> We know there are black cats.  We know they are all cats.  We know there
>>> are no halt deciders using a few trivial steps that you pretend to not
>>> (or perhaps really don't) understand.
>>>
>> Of course when you say there are no halt decider you do not mean that
>> they are no halt deciders you mean that there are no universal halt
>> deciders. It would be better if you say exactly what you mean and
>> mean exactly what you say.
>
> He means there are no even partial halt deciders that get the H^
> computation correctly.

No, I meant what I said that there are no halt deciders. The term "halt
decider" (except, perhaps, in some weird contexts) always means a
universal one.

PO is ether lying about using Ĥ to mean what Linz does, or lying about
how it is specified. Linz's Ĥ is derived from a universal decider H.

> Yours doesn't...

I would rather not talk about "yours" (i.e. PO's thingy -- whatever that
is) until he admits he's not using Ĥ to talk about Linz's class of TMs
called Ĥ. But that would mean he has to define what he's talking about
(the famous "pathological" inputs) and that's eluded him for more than a
decade.

I think he gets given far too much licence. If he writes Ĥ and claims
that it might exist because it comes from a partial halt decider, he
should be called out for that.

--
Ben.

On 10/25/2021 7:22 PM, Ben Bacarisse wrote:
> Richard Damon <Richard@Damon-Family.org> writes:
>
>> On 10/24/21 6:27 PM, olcott wrote:
>>> On 10/24/2021 10:23 AM, Ben Bacarisse wrote:
>>>> olcott <NoOne@NoWhere.com> writes:
>
>>>>> The words above are like say that when we know that we have a black
>>>>> cat then we know that we have a cat, and yet you still disagree.
>>>>
>>>> We know there are black cats.  We know they are all cats.  We know there
>>>> are no halt deciders using a few trivial steps that you pretend to not
>>>> (or perhaps really don't) understand.
>>>>
>>> Of course when you say there are no halt decider you do not mean that
>>> they are no halt deciders you mean that there are no universal halt
>>> deciders. It would be better if you say exactly what you mean and
>>> mean exactly what you say.
>>
>> He means there are no even partial halt deciders that get the H^
>> computation correctly.
>
> No, I meant what I said that there are no halt deciders. The term "halt
> decider" (except, perhaps, in some weird contexts) always means a
> universal one.
>
> PO is ether lying about using Ĥ to mean what Linz does, or lying about
> how it is specified. Linz's Ĥ is derived from a universal decider H.
>

Linz's "proof" that no universal halt decider exists is entirely based
on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.

>> Yours doesn't...
>
> I would rather not talk about "yours" (i.e. PO's thingy -- whatever that
> is) until he admits he's not using Ĥ to talk about Linz's class of TMs
> called Ĥ. But that would mean he has to define what he's talking about
> (the famous "pathological" inputs) and that's eluded him for more than a
> decade.
>
> I think he gets given far too much licence. If he writes Ĥ and claims
> that it might exist because it comes from a partial halt decider, he
> should be called out for that.
>

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 10/25/21 8:36 PM, olcott wrote:
> On 10/25/2021 7:22 PM, Ben Bacarisse wrote:
>> Richard Damon <Richard@Damon-Family.org> writes:
>>
>>> On 10/24/21 6:27 PM, olcott wrote:
>>>> On 10/24/2021 10:23 AM, Ben Bacarisse wrote:
>>>>> olcott <NoOne@NoWhere.com> writes:
>>
>>>>>> The words above are like say that when we know that we have a black
>>>>>> cat then we know that we have a cat, and yet you still disagree.
>>>>>
>>>>> We know there are black cats.  We know they are all cats.  We know
>>>>> there
>>>>> are no halt deciders using a few trivial steps that you pretend to not
>>>>> (or perhaps really don't) understand.
>>>>>
>>>> Of course when you say there are no halt decider you do not mean that
>>>> they are no halt deciders you mean that there are no universal halt
>>>> deciders. It would be better if you say exactly what you mean and
>>>> mean exactly what you say.
>>>
>>> He means there are no even partial halt deciders that get the H^
>>> computation correctly.
>>
>> No, I meant what I said that there are no halt deciders.  The term "halt
>> decider" (except, perhaps, in some weird contexts) always means a
>> universal one.
>>
>> PO is ether lying about using Ĥ to mean what Linz does, or lying about
>> how it is specified.  Linz's Ĥ is derived from a universal decider H.
>>
>
> Linz's "proof" that no universal halt decider exists is entirely based
> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.

And your H doesn't decide correctly, so Linz is still right.

Since your H says H(<H^>,<H^>) is non-halting, Linz's H^(<H^>) is
Halting, so H is wrong.

It doesn't matter that H's simulation never got to that point, the
actual computation that the input is a representation of does, and THAT
is what matters. This is an inevitable result if H is actually the
Computation that is required of it.

>
>
>>> Yours doesn't...
>>
>> I would rather not talk about "yours" (i.e. PO's thingy -- whatever that
>> is) until he admits he's not using Ĥ to talk about Linz's class of TMs
>> called Ĥ.  But that would mean he has to define what he's talking about
>> (the famous "pathological" inputs) and that's eluded him for more than a
>> decade.
>>
>> I think he gets given far too much licence.  If he writes Ĥ and claims
>> that it might exist because it comes from a partial halt decider, he
>> should be called out for that.
>>
>
>

olcott <NoOne@NoWhere.com> writes:

> Linz's "proof" that no universal halt decider exists is entirely based
> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.

It's a proof, not a "proof". It only becomes a "proof" when someone
finds a mistake in it. And it does not rely on his beliefs. That's not
the word to use when talking about simple logic like this:

If a TM, H, existed such that

Hq0 <M> s ⊦* Hqy if M applied to s halts, and
Hq0 <M> s ⊦* Hqn if M applied to s does not halt,

we could construct from it an H' such that

H'q0 <M> s ⊦* oo if M applied to s halts, and
H'q0 <M> s ⊦* H'qn if M applied to s does not halt.

And from that we could construct an Ĥ such that

Ĥq0 <M> ⊦* Ĥqx <M> <M> ⊦* oo if M applied to <M> halts, and
Ĥq0 <M> ⊦* Ĥqx <M> <M> ⊦* Ĥqn if M applied to <M> does not halt.

Setting M to Ĥ, so <M> becomes <Ĥ>, we see that the existence of H (as
Linz defines it) logically entails that a TM Ĥ that does this

Ĥq0 <Ĥ> ⊦* Ĥqx <Ĥ> <Ĥ> ⊦* oo if Ĥ applied to <Ĥ> halts, and
Ĥq0 <Ĥ> ⊦* Ĥqx <Ĥ> <Ĥ> ⊦* Ĥqn if Ĥ applied to <Ĥ> does not halt.

would also have to exist. But, as Linz says, "this is clearly
nonsense".

To call such trivial sequence of deductions a belief is just rhetorical
spin.

--
Ben.

On 10/26/2021 9:28 AM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> Linz's "proof" that no universal halt decider exists is entirely based
>> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>
> It's a proof, not a "proof". It only becomes a "proof" when someone
> finds a mistake in it. And it does not rely on his beliefs. That's not
> the word to use when talking about simple logic like this:
>

Because this is necessarily true (only a fool would disagree)

Simulating Halt Decider Theorem (Olcott 2021):
Whenever simulating halt decider H correctly determines that input P
never reaches its final state (whether or not its simulation of P is
aborted) then H correctly decides that P never halts.

As soon as I show that Ĥq0 <Ĥ> <Ĥ> meets the above theorem then Linz has
been refuted. Only a fool would disagree.

> If a TM, H, existed such that
>
> Hq0 <M> s ⊦* Hqy if M applied to s halts, and
> Hq0 <M> s ⊦* Hqn if M applied to s does not halt,
>
> we could construct from it an H' such that
>
> H'q0 <M> s ⊦* oo if M applied to s halts, and
> H'q0 <M> s ⊦* H'qn if M applied to s does not halt.
>
> And from that we could construct an Ĥ such that
>
> Ĥq0 <M> ⊦* Ĥqx <M> <M> ⊦* oo if M applied to <M> halts, and
> Ĥq0 <M> ⊦* Ĥqx <M> <M> ⊦* Ĥqn if M applied to <M> does not halt.
>
> Setting M to Ĥ, so <M> becomes <Ĥ>, we see that the existence of H (as
> Linz defines it) logically entails that a TM Ĥ that does this
>
> Ĥq0 <Ĥ> ⊦* Ĥqx <Ĥ> <Ĥ> ⊦* oo if Ĥ applied to <Ĥ> halts, and
> Ĥq0 <Ĥ> ⊦* Ĥqx <Ĥ> <Ĥ> ⊦* Ĥqn if Ĥ applied to <Ĥ> does not halt.
>
> would also have to exist. But, as Linz says, "this is clearly
> nonsense".
>
> To call such trivial sequence of deductions a belief is just rhetorical
> spin.
>

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On Tuesday, 26 October 2021 at 15:47:36 UTC+1, olcott wrote:
> On 10/26/2021 9:28 AM, Ben Bacarisse wrote:
> > olcott <No...@NoWhere.com> writes:
> >
> >> Linz's "proof" that no universal halt decider exists is entirely based
> >> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
> >
> > It's a proof, not a "proof". It only becomes a "proof" when someone
> > finds a mistake in it. And it does not rely on his beliefs. That's not
> > the word to use when talking about simple logic like this:
> >
> Because this is necessarily true (only a fool would disagree)
>
> Simulating Halt Decider Theorem (Olcott 2021):
> Whenever simulating halt decider H correctly determines that input P
> never reaches its final state (whether or not its simulation of P is
> aborted) then H correctly decides that P never halts.
>
Well that hasn't been thought through. Assuming simulating halt decider H
to be a Turing machine, if H's simulation of P is not halted, H never terminates,
so, using Turing's model, you never see the result of the decision.
(In Turing's model, intermediate states of the tape whilst the machine is
running can't be treated as results. What looks like a result might be scratch
space. You have to wait until the machine has halted to read the result).

On 10/26/2021 10:58 AM, Malcolm McLean wrote:
> On Tuesday, 26 October 2021 at 15:47:36 UTC+1, olcott wrote:
>> On 10/26/2021 9:28 AM, Ben Bacarisse wrote:
>>> olcott <No...@NoWhere.com> writes:
>>>
>>>> Linz's "proof" that no universal halt decider exists is entirely based
>>>> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>>>
>>> It's a proof, not a "proof". It only becomes a "proof" when someone
>>> finds a mistake in it. And it does not rely on his beliefs. That's not
>>> the word to use when talking about simple logic like this:
>>>
>> Because this is necessarily true (only a fool would disagree)
>>
>> Simulating Halt Decider Theorem (Olcott 2021):
>> Whenever simulating halt decider H correctly determines that input P
>> never reaches its final state (whether or not its simulation of P is
>> aborted) then H correctly decides that P never halts.
>>
> Well that hasn't been thought through. Assuming simulating halt decider H
> to be a Turing machine, if H's simulation of P is not halted, H never terminates,
> so, using Turing's model, you never see the result of the decision.

>> Simulating Halt Decider Theorem (Olcott 2021):
>> Whenever simulating halt decider H correctly determines that input P
WOULD
>> never
REACH
its final state (whether or not its simulation of P is
>> aborted) then H correctly decides that P never halts.

> (In Turing's model, intermediate states of the tape whilst the machine is
> running can't be treated as results. What looks like a result might be scratch
> space. You have to wait until the machine has halted to read the result).
>

void Infinite_Loop()
{ HERE: goto HERE;
}

_Infinite_Loop()
[00000ab0](01) 55 push ebp
[00000ab1](02) 8bec mov ebp,esp
[00000ab3](02) ebfe jmp 00000ab3
[00000ab5](01) 5d pop ebp
[00000ab6](01) c3 ret
Size in bytes:(0007) [00000ab6]

I provide this as a simplest example.
It doesn't take a PhD to understand that the simulation of
_Infinite_Loop() never reaches machine address 0xab6.

// Simplified Linz Ĥ (Linz:1990:319)
// Strachey(1965) CPL translated to C
01 void P(u32 x)
02 {
03 if (H(x, x))
04 HERE: goto HERE;
05 }

The above code can be analyzed using a similar axiomatic basis to
determine that no simulation of the input to H(P,P) ever gets past line 03.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

olcott <NoOne@NoWhere.com> writes:

> On 10/26/2021 9:28 AM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> Linz's "proof" that no universal halt decider exists is entirely based
>>> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>> It's a proof, not a "proof". It only becomes a "proof" when someone
>> finds a mistake in it. And it does not rely on his beliefs. That's not
>> the word to use when talking about simple logic like this:
>
> Because this is necessarily true (only a fool would disagree)
>
> Simulating Halt Decider Theorem (Olcott 2021):
> Whenever simulating halt decider H correctly determines that input P
> never reaches its final state (whether or not its simulation of P is
> aborted) then H correctly decides that P never halts.

What is H? What is P? What is a correct decision? What does it mean
to say an input does or does not halt? Linz's proof does not leave any
of these things unspecified. He defines what H should do in all cases.
He does not introduce new symbols like P without definition. (The last
time you used P it as a scrap of C code, not an input string to a
Turning machine.)

> As soon as I show that Ĥq0 <Ĥ> <Ĥ> meets the above theorem then Linz
> has been refuted. Only a fool would disagree.

No. You need to point out where Linz goes wrong, not pontificate about
an ill-defined "theorem".

>> If a TM, H, existed such that
>> Hq0 <M> s ⊦* Hqy if M applied to s halts, and
>> Hq0 <M> s ⊦* Hqn if M applied to s does not halt,
>> we could construct from it an H' such that
>> H'q0 <M> s ⊦* oo if M applied to s halts, and
>> H'q0 <M> s ⊦* H'qn if M applied to s does not halt.
>> And from that we could construct an Ĥ such that
>> Ĥq0 <M> ⊦* Ĥqx <M> <M> ⊦* oo if M applied to <M> halts, and
>> Ĥq0 <M> ⊦* Ĥqx <M> <M> ⊦* Ĥqn if M applied to <M> does not halt.
>> Setting M to Ĥ, so <M> becomes <Ĥ>, we see that the existence of H (as
>> Linz defines it) logically entails that a TM Ĥ that does this
>> Ĥq0 <Ĥ> ⊦* Ĥqx <Ĥ> <Ĥ> ⊦* oo if Ĥ applied to <Ĥ> halts, and
>> Ĥq0 <Ĥ> ⊦* Ĥqx <Ĥ> <Ĥ> ⊦* Ĥqn if Ĥ applied to <Ĥ> does not halt.
>> would also have to exist. But, as Linz says, "this is clearly
>> nonsense".

And there was you chance to point out where Linz goes wrong. Why did
you not take it? Because there is no error in the logic and you know
it.

--
Ben.

olcott <NoOne@NoWhere.com> writes:

> Within the specific context of the details of the proof ⟨Ĥ⟩ ⟨Ĥ⟩ is
> defined as an input that H gets wrong thus when I show that H decides
> ⟨Ĥ⟩ ⟨Ĥ⟩ correctly Linz has been refuted.

All you do is assert that H decides ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.

> Are you willing to admit that if it is shown that H correctly decides
> the halt status of ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted or are you going
> to dishonestly dodge this key point?

I keep trying not to dodge it but you keep ignoring my answer. No proof
is invalided by other truths. You might render all of mathematics
inconsistent, but previously valid chains of reasoning remains valid.
You made it plain that don't accept what a proof is when you stated that
if A,B,C ⊦ X, then ~A,A,B,C ⊬ X. As far as I know you have never
retracted this incorrect statement.

As it happens, you can't show that Linz's H is correct about the input
⟨Ĥ⟩ ⟨Ĥ⟩, so the point is moot, but I have been trying to get you to note
my answer to this hypothetical question for years, but you keep
pretending not to notice.

--
Ben.

On 10/26/2021 6:19 PM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> On 10/26/2021 9:28 AM, Ben Bacarisse wrote:
>>> olcott <NoOne@NoWhere.com> writes:
>>>
>>>> Linz's "proof" that no universal halt decider exists is entirely based
>>>> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>>> It's a proof, not a "proof". It only becomes a "proof" when someone
>>> finds a mistake in it. And it does not rely on his beliefs. That's not
>>> the word to use when talking about simple logic like this:
>>
>> Because this is necessarily true (only a fool would disagree)
>>
>> Simulating Halt Decider Theorem (Olcott 2021):
>> Whenever simulating halt decider H correctly determines that input P
>> never reaches its final state (whether or not its simulation of P is
>> aborted) then H correctly decides that P never halts.
>
> What is H?
a simulating halt decider

> What is P?
input to Simulating Halt Decider

What is a correct decision?

Reports whether or not simulated input reaches its final state

> What does it mean
> to say an input does or does not halt?

the simulation of the input never reaches its final state
(whether or not its simulation of P is aborted)

> Linz's proof does not leave any
> of these things unspecified. He defines what H should do in all cases.
> He does not introduce new symbols like P without definition. (The last
> time you used P it as a scrap of C code, not an input string to a
> Turning machine.)
>
>> As soon as I show that Ĥq0 <Ĥ> <Ĥ> meets the above theorem then Linz
>> has been refuted. Only a fool would disagree.
>
> No. You need to point out where Linz goes wrong, not pontificate about
> an ill-defined "theorem".

Linz is wrong is his final conclusion at the top of page 320.
https://www.liarparadox.org/Peter_Linz_HP(Pages_315-320).pdf

q0 ⟨Ĥ⟩ ⊢* Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥqn

The input to Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ specifies infinitely nested simulation thus Ĥq0
correctly transitions to Ĥqn.

The mistake that Linz makes is that he is wrongly assuming that Ĥq0 is
deciding whether or not itself halts.

Ĥq0 is NOT deciding whether or not itself halts.
Ĥq0 is deciding whether or its input: ⟨Ĥ⟩ ⟨Ĥ⟩ halts.

He confused himself by not provided the full specification for Ĥ.
He abbreviated it to be concise.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 10/26/2021 6:47 PM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> Within the specific context of the details of the proof ⟨Ĥ⟩ ⟨Ĥ⟩ is
>> defined as an input that H gets wrong thus when I show that H decides
>> ⟨Ĥ⟩ ⟨Ĥ⟩ correctly Linz has been refuted.
>
> All you do is assert that H decides ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>
>> Are you willing to admit that if it is shown that H correctly decides
>> the halt status of ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted or are you going
>> to dishonestly dodge this key point?
>
> I keep trying not to dodge it but you keep ignoring my answer. No proof
> is invalided by other truths. You might render all of mathematics
> inconsistent, but previously valid chains of reasoning remains valid.
> You made it plain that don't accept what a proof is when you stated that
> if A,B,C ⊦ X, then ~A,A,B,C ⊬ X. As far as I know you have never
> retracted this incorrect statement.
>
> As it happens, you can't show that Linz's H is correct about the input
> ⟨Ĥ⟩ ⟨Ĥ⟩, so the point is moot, but I have been trying to get you to note
> my answer to this hypothetical question for years, but you keep
> pretending not to notice.
>

I ask you a YES / NO question and you dodge. I did not ask you to
analyze the question you don't understand it well enough to do this
correctly.

That you keep dodging questions like this proves that you desperately
want to avoid any mutual understanding and only care about rebuttal even
at the cost of truth.

THIS IS A FREAKING MANDATORY PREREQUISITE:
Are you willing to admit that if it is shown that H correctly decides
the halt status of ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted or are you going
to dishonestly dodge this key point?

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 10/26/21 8:14 PM, olcott wrote:
> On 10/26/2021 6:47 PM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> Within the specific context of the details of the proof ⟨Ĥ⟩ ⟨Ĥ⟩ is
>>> defined as an input that H gets wrong thus when I show that H decides
>>> ⟨Ĥ⟩ ⟨Ĥ⟩ correctly Linz has been refuted.
>>
>> All you do is assert that H decides ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>>
>>> Are you willing to admit that if it is shown that H correctly decides
>>> the halt status of ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted or are you going
>>> to dishonestly dodge this key point?
>>
>> I keep trying not to dodge it but you keep ignoring my answer.  No proof
>> is invalided by other truths.  You might render all of mathematics
>> inconsistent, but previously valid chains of reasoning remains valid.
>> You made it plain that don't accept what a proof is when you stated that
>> if A,B,C ⊦ X, then ~A,A,B,C ⊬ X.  As far as I know you have never
>> retracted this incorrect statement.
>>
>> As it happens, you can't show that Linz's H is correct about the input
>> ⟨Ĥ⟩ ⟨Ĥ⟩, so the point is moot, but I have been trying to get you to note
>> my answer to this hypothetical question for years, but you keep
>> pretending not to notice.
>>
>
> I ask you a YES / NO question and you dodge. I did not ask you to
> analyze the question you don't understand it well enough to do this
> correctly.
>
> That you keep dodging questions like this proves that you desperately
> want to avoid any mutual understanding and only care about rebuttal even
> at the cost of truth.
>
> THIS IS A FREAKING MANDATORY PREREQUISITE:
> Are you willing to admit that if it is shown that H correctly decides
> the halt status of ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted or are you going
> to dishonestly dodge this key point?
>
>

Well, the problem is that <H^> <H^> is just a string, and strings don't
have behavior.

The Halting Problem is asking if UTM(<H^><H^>) will halt.

You are talking about the nonsense of will H abort is simulation of
<H^><H^> before it sees a halting state.

The nonsese of adding things like whether or not it aborts the
simulation is just blather, as for a given H, that is a fixed fact and
the fact that the machine being looked at contains a copy of H, you
can't change the 'global' definition of H and reason about the given input.

If you change your logic to whether or not THIS copy is changed to not
halt, then you would get something, except for that fact that this just
proves that your assertion is WRONG, as replacing that top level H with
a UTM (but keeping the copy in H^ to still be the original) shows that
it halts.

olcott <NoOne@NoWhere.com> writes:

> On 10/26/2021 6:47 PM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:

>> All you do is assert that H decides ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>>
>>> Are you willing to admit that if it is shown that H correctly decides
>>> the halt status of ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted or are you going
>>> to dishonestly dodge this key point?
>>
>> I keep trying not to dodge it but you keep ignoring my answer. No proof
>> is invalided by other truths. You might render all of mathematics
>> inconsistent, but previously valid chains of reasoning remains valid.
>>
>> You made it plain that don't accept what a proof is when you stated that
>> if A,B,C ⊦ X, then ~A,A,B,C ⊬ X. As far as I know you have never
>> retracted this incorrect statement.
>>
>> As it happens, you can't show that Linz's H is correct about the input
>> ⟨Ĥ⟩ ⟨Ĥ⟩, so the point is moot, but I have been trying to get you to note
>> my answer to this hypothetical question for years, but you keep
>> pretending not to notice.
>
> I ask you a YES / NO question and you dodge.

How could you miss the answer yet again? Clearly it's no: I don't
accept that if it is shown that H correctly decides the halt status of
⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted. How was "no proof is invalided by
other truths" not clearly a "no"? I had no idea you would need it
spelled out.

Anyway, I've spelled it out now: no. If you want to see why you are
wrong to think the answer might be yes, the explanation is all there.

--
Ben.

olcott <NoOne@NoWhere.com> writes:

> On 10/26/2021 6:19 PM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> On 10/26/2021 9:28 AM, Ben Bacarisse wrote:
>>>> olcott <NoOne@NoWhere.com> writes:
>>>>
>>>>> Linz's "proof" that no universal halt decider exists is entirely based
>>>>> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>>>> It's a proof, not a "proof". It only becomes a "proof" when someone
>>>> finds a mistake in it. And it does not rely on his beliefs. That's not
>>>> the word to use when talking about simple logic like this:
>>>
>>> Because this is necessarily true (only a fool would disagree)
>>>
>>> Simulating Halt Decider Theorem (Olcott 2021):
>>> Whenever simulating halt decider H correctly determines that input P
>>> never reaches its final state (whether or not its simulation of P is
>>> aborted) then H correctly decides that P never halts.
>> What is H?
> a simulating halt decider

This does not specify H. Is this the behaviour you want or expect H to
exhibit:

Hq0 <M> s ⊦* Hqy if M applied to s halts, and
Hq0 <M> s ⊦* Hqn if M applied to s does not halt?

I doubt it, but please either confirm that when you write H you mean a
TM with the above behaviour, or, if you are using H to mean a TM that
might deviate from this specification, please give the actual
specification. *And stop calling it H!*

>> What is P?
> input to Simulating Halt Decider
>
>> What is a correct decision?
>
> Reports whether or not simulated input reaches its final state
>
>> What does it mean
>> to say an input does or does not halt?
>
> the simulation of the input never reaches its final state
> (whether or not its simulation of P is aborted)

A proper simulation (by a UTM) matches the halting behaviour of the
encoded TM. I.e. this:

Hq0 <M> s ⊦* Hqy if UTM(<M>, s) reaches M's halt state, and
Hq0 <M> s ⊦* Hqn if UTM(<M>, s) does not reach M's halt state

is exactly the same as the much simpler description above so the mystery
word "abort" (TM don't "abort") is hiding those cases where you intend a
decider to be wrong about some inputs.

If there are no inputs your imagined TM gets wrong (i.e. what you call H
really is what Linz calls H) then your "theorem" is just a badly worded
statement about a non-existent class of Turing machines.

>> Linz's proof does not leave any
>> of these things unspecified. He defines what H should do in all cases.
>> He does not introduce new symbols like P without definition. (The last
>> time you used P it as a scrap of C code, not an input string to a
>> Turning machine.)
>>
>>> As soon as I show that Ĥq0 <Ĥ> <Ĥ> meets the above theorem then Linz
>>> has been refuted. Only a fool would disagree.
>> No. You need to point out where Linz goes wrong, not pontificate about
>> an ill-defined "theorem".
>
> Linz is wrong is his final conclusion at the top of page 320.
> https://www.liarparadox.org/Peter_Linz_HP(Pages_315-320).pdf

So the step you think is wrong is to determine what Ĥ applied to <Ĥ>
does by substituting specific values (Ĥ for M and <Ĥ> for <M>) into the
previous, correctly derived equation? That's an odd complaint. What's
wrong with the substitution?

> q0 ⟨Ĥ⟩ ⊢* Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥqn

Remember to add "if Ĥ applied to ⟨Ĥ⟩ does not halt". Without that
condition, you are not talking about the proof you are trying to
invalidate.

(Aside: this notation is a step backwards. Writing Ĥq0 when you don't
mean state q0 of Ĥ is just silly. You could call in Hq0 or H'q0 because
it is the state that corresponds to the initial states of both H and H',
but Ĥq0 is just an awful name.)

I cut the rest because it does not explain why you reject that final
substitution step. If you think it does, put it back in reply to my
question ("What's wrong with the substitution?") and I'll try to explain
it to you.

--
Ben.

On 10/27/2021 8:12 AM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> On 10/26/2021 6:47 PM, Ben Bacarisse wrote:
>>> olcott <NoOne@NoWhere.com> writes:
>
>>> All you do is assert that H decides ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>>>
>>>> Are you willing to admit that if it is shown that H correctly decides
>>>> the halt status of ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted or are you going
>>>> to dishonestly dodge this key point?
>>>
>>> I keep trying not to dodge it but you keep ignoring my answer. No proof
>>> is invalided by other truths. You might render all of mathematics
>>> inconsistent, but previously valid chains of reasoning remains valid.
>>>
>>> You made it plain that don't accept what a proof is when you stated that
>>> if A,B,C ⊦ X, then ~A,A,B,C ⊬ X. As far as I know you have never
>>> retracted this incorrect statement.
>>>
>>> As it happens, you can't show that Linz's H is correct about the input
>>> ⟨Ĥ⟩ ⟨Ĥ⟩, so the point is moot, but I have been trying to get you to note
>>> my answer to this hypothetical question for years, but you keep
>>> pretending not to notice.
>>
>> I ask you a YES / NO question and you dodge.
>
> How could you miss the answer yet again? Clearly it's no: I don't
> accept that if it is shown that H correctly decides the halt status of
> ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted.

So you reject the idea of a semantic tautology.
If X says Y is true and I prove that Y is false then X could still be
correct. No wonder we are having trouble communicating, you are simply
irrational.

> How was "no proof is invalided by
> other truths" not clearly a "no"? I had no idea you would need it
> spelled out.
>
> Anyway, I've spelled it out now: no. If you want to see why you are
> wrong to think the answer might be yes, the explanation is all there.
>

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 10/27/2021 8:15 AM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> On 10/26/2021 6:19 PM, Ben Bacarisse wrote:
>>> olcott <NoOne@NoWhere.com> writes:
>>>
>>>> On 10/26/2021 9:28 AM, Ben Bacarisse wrote:
>>>>> olcott <NoOne@NoWhere.com> writes:
>>>>>
>>>>>> Linz's "proof" that no universal halt decider exists is entirely based
>>>>>> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>>>>> It's a proof, not a "proof". It only becomes a "proof" when someone
>>>>> finds a mistake in it. And it does not rely on his beliefs. That's not
>>>>> the word to use when talking about simple logic like this:
>>>>
>>>> Because this is necessarily true (only a fool would disagree)
>>>>
>>>> Simulating Halt Decider Theorem (Olcott 2021):
>>>> Whenever simulating halt decider H correctly determines that input P
>>>> never reaches its final state (whether or not its simulation of P is
>>>> aborted) then H correctly decides that P never halts.
>>> What is H?
>> a simulating halt decider
>
> This does not specify H. Is this the behaviour you want or expect H to
> exhibit:
>
> Hq0 <M> s ⊦* Hqy if M applied to s halts, and
> Hq0 <M> s ⊦* Hqn if M applied to s does not halt?
>
> I doubt it, but please either confirm that when you write H you mean a
> TM with the above behaviour, or, if you are using H to mean a TM that
> might deviate from this specification, please give the actual
> specification. *And stop calling it H!*
>
>>> What is P?
>> input to Simulating Halt Decider
>>
>>> What is a correct decision?
>>
>> Reports whether or not simulated input reaches its final state
>>
>>> What does it mean
>>> to say an input does or does not halt?
>>
>> the simulation of the input never reaches its final state
>> (whether or not its simulation of P is aborted)
>
> A proper simulation (by a UTM) matches the halting behaviour of the
> encoded TM. I.e. this:
>
> Hq0 <M> s ⊦* Hqy if UTM(<M>, s) reaches M's halt state, and
> Hq0 <M> s ⊦* Hqn if UTM(<M>, s) does not reach M's halt state
>
> is exactly the same as the much simpler description above so the mystery
> word "abort" (TM don't "abort") is hiding those cases where you intend a
> decider to be wrong about some inputs.
>
> If there are no inputs your imagined TM gets wrong (i.e. what you call H
> really is what Linz calls H) then your "theorem" is just a badly worded
> statement about a non-existent class of Turing machines.
>
>>> Linz's proof does not leave any
>>> of these things unspecified. He defines what H should do in all cases.
>>> He does not introduce new symbols like P without definition. (The last
>>> time you used P it as a scrap of C code, not an input string to a
>>> Turning machine.)
>>>
>>>> As soon as I show that Ĥq0 <Ĥ> <Ĥ> meets the above theorem then Linz
>>>> has been refuted. Only a fool would disagree.
>>> No. You need to point out where Linz goes wrong, not pontificate about
>>> an ill-defined "theorem".
>>
>> Linz is wrong is his final conclusion at the top of page 320.
>> https://www.liarparadox.org/Peter_Linz_HP(Pages_315-320).pdf
>
> So the step you think is wrong is to determine what Ĥ applied to <Ĥ>
> does by substituting specific values (Ĥ for M and <Ĥ> for <M>) into the
> previous, correctly derived equation? That's an odd complaint. What's
> wrong with the substitution?
>
>> q0 ⟨Ĥ⟩ ⊢* Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥqn
>
> Remember to add "if Ĥ applied to ⟨Ĥ⟩ does not halt". Without that
> condition, you are not talking about the proof you are trying to
> invalidate.
>
> (Aside: this notation is a step backwards. Writing Ĥq0 when you don't
> mean state q0 of Ĥ is just silly. You could call in Hq0 or H'q0 because
> it is the state that corresponds to the initial states of both H and H',
> but Ĥq0 is just an awful name.)
>
> I cut the rest because it does not explain why you reject that final
> substitution step. If you think it does, put it back in reply to my
> question ("What's wrong with the substitution?") and I'll try to explain
> it to you.
>

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
If the UTM simulation of the input to Ĥqx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach its
final state (whether or not this simulation is aborted) then it is
necessarily true that Ĥqx transitions to Ĥ.qn correctly.

The mistake that Linz makes on the top of page 320 is that he wrongly
assumes that Ĥ.qx is deciding the halt status of itself.

As long as halt decider H has correctly decided the halt status of its
input P then the halt status of P was correctly decided by H and nothing
in the universe can possibly contradict this.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

olcott <NoOne@NoWhere.com> writes:

> On 10/27/2021 8:12 AM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> On 10/26/2021 6:47 PM, Ben Bacarisse wrote:
>>>> olcott <NoOne@NoWhere.com> writes:
>>
>>>> All you do is assert that H decides ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>>>>
>>>>> Are you willing to admit that if it is shown that H correctly decides
>>>>> the halt status of ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted or are you going
>>>>> to dishonestly dodge this key point?
>>>>
>>>> I keep trying not to dodge it but you keep ignoring my answer. No proof
>>>> is invalided by other truths. You might render all of mathematics
>>>> inconsistent, but previously valid chains of reasoning remains valid.
>>>>
>>>> You made it plain that don't accept what a proof is when you stated that
>>>> if A,B,C ⊦ X, then ~A,A,B,C ⊬ X. As far as I know you have never
>>>> retracted this incorrect statement.
>>>>
>>>> As it happens, you can't show that Linz's H is correct about the input
>>>> ⟨Ĥ⟩ ⟨Ĥ⟩, so the point is moot, but I have been trying to get you to note
>>>> my answer to this hypothetical question for years, but you keep
>>>> pretending not to notice.
>>>
>>> I ask you a YES / NO question and you dodge.
>> How could you miss the answer yet again? Clearly it's no: I don't
>> accept that if it is shown that H correctly decides the halt status of
>> ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted.
>
> So you reject the idea of a semantic tautology.

No. I reject what you said, not any further extension of it that you
care to propose. Proofs are logical entailments, and as such are not
invalidated by any others. To invalidate the poof you have struggled
with for decades, you need to show an error in it (ut you can't because
it's valid). If, in the unlikely event you prove something that
contradicts it, you will have shown an inconsistency. The original
proof remains valid (though pointless).

> If X says Y is true and I prove that Y is false then X could still be
> correct. No wonder we are having trouble communicating, you are simply
> irrational.

No, the explanation lies in the fact that you don't know that you have
said three different things, only one of which I reject. Here is what I
reject, re-phrased for this last scenario: if X proves Y and you prove
~Y, X's proof would still be valid, but the whole deductive system would
have been shown to be inconsistent.

You don't know what other people (logicians, mathematicians, educated
lay people) mean when that talk about proofs. You still claim that if
A,B,C ⊦ X, then ~A,A,B,C ⊬ X. The problem communicating comes from not
having a shared understanding of the basic terms.

--
Ben.

olcott <NoOne@NoWhere.com> writes:

> On 10/27/2021 8:15 AM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> On 10/26/2021 6:19 PM, Ben Bacarisse wrote:
>>>> olcott <NoOne@NoWhere.com> writes:
>>>>
>>>>> On 10/26/2021 9:28 AM, Ben Bacarisse wrote:
>>>>>> olcott <NoOne@NoWhere.com> writes:
>>>>>>
>>>>>>> Linz's "proof" that no universal halt decider exists is entirely based
>>>>>>> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>>>>>> It's a proof, not a "proof". It only becomes a "proof" when someone
>>>>>> finds a mistake in it. And it does not rely on his beliefs. That's not
>>>>>> the word to use when talking about simple logic like this:
>>>>>
>>>>> Because this is necessarily true (only a fool would disagree)
>>>>>
>>>>> Simulating Halt Decider Theorem (Olcott 2021):
>>>>> Whenever simulating halt decider H correctly determines that input P
>>>>> never reaches its final state (whether or not its simulation of P is
>>>>> aborted) then H correctly decides that P never halts.
>>>> What is H?
>>> a simulating halt decider
>> This does not specify H. Is this the behaviour you want or expect H to
>> exhibit:
>> Hq0 <M> s ⊦* Hqy if M applied to s halts, and
>> Hq0 <M> s ⊦* Hqn if M applied to s does not halt?
>> I doubt it, but please either confirm that when you write H you mean a
>> TM with the above behaviour, or, if you are using H to mean a TM that
>> might deviate from this specification, please give the actual
>> specification. *And stop calling it H!*

So you won't say? Why not?

>>>> What is P?
>>> input to Simulating Halt Decider
>>>
>>>> What is a correct decision?
>>>
>>> Reports whether or not simulated input reaches its final state
>>>
>>>> What does it mean
>>>> to say an input does or does not halt?
>>>
>>> the simulation of the input never reaches its final state
>>> (whether or not its simulation of P is aborted)
>>
>> A proper simulation (by a UTM) matches the halting behaviour of the
>> encoded TM. I.e. this:
>> Hq0 <M> s ⊦* Hqy if UTM(<M>, s) reaches M's halt state, and
>> Hq0 <M> s ⊦* Hqn if UTM(<M>, s) does not reach M's halt state
>> is exactly the same as the much simpler description above so the mystery
>> word "abort" (TM don't "abort") is hiding those cases where you intend a
>> decider to be wrong about some inputs.
>>
>> If there are no inputs your imagined TM gets wrong (i.e. what you call H
>> really is what Linz calls H) then your "theorem" is just a badly worded
>> statement about a non-existent class of Turing machines.

So you won't say? Why not?

>> I cut the rest because it does not explain why you reject that final
>> substitution step. If you think it does, put it back in reply to my
>> question ("What's wrong with the substitution?") and I'll try to explain
>> it to you.
>
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>
> If the UTM simulation of the input to Ĥqx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach
> its final state (whether or not this simulation is aborted) then it is
> necessarily true that Ĥqx transitions to Ĥ.qn correctly.
>
> The mistake that Linz makes on the top of page 320 is that he wrongly
> assumes that Ĥ.qx is deciding the halt status of itself.
>
> As long as halt decider H has correctly decided the halt status of its
> input P then the halt status of P was correctly decided by H and
> nothing in the universe can possibly contradict this.

When Linz writes

Ĥ.q0 ⟨M⟩ ⊢* Ĥ.qx ⟨M⟩ ⟨M⟩ ⊢* oo if M applied to ⟨M⟩ halts
Ĥ.q0 ⟨M⟩ ⊢* Ĥ.qx ⟨M⟩ ⟨M⟩ ⊢* Ĥ.qn if M applied to ⟨M⟩ does not halt

the variable M stands for any Turing machine. Nothing in the argument
limits what Turing machines M might stand for. This generality flows
from the start of the proof to the end. H is defined by what it does
with any encoded M, so H' is also defined by what it does with any
encoded M. Consequently Ĥ's behaviour also applies to any encoded M:

Either Ĥ does not halt when given the encoding of any TM that halts when
given its own encoding, or Ĥ halts when given the encoding of any TM
that does not halt when given its own encoding.

Can you see why what you wrote does not explain your objection? I
accept that you don't like what results from substituting Ĥ for M in
that last step, but nothing you write has anything to do with why you
think it's not a validly logical thing to do.

(As usual, you are wrong about some of the things you say in your
explanation, but none of those misconceptions have anything to do with
why you think you can't substitute Ĥ for M. It would just be a waste of
time to try to correct them, especially as you have refused to do so on
more than one occasion.)

--
Ben.

On 10/27/21 9:51 AM, olcott wrote:
> On 10/27/2021 8:12 AM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> On 10/26/2021 6:47 PM, Ben Bacarisse wrote:
>>>> olcott <NoOne@NoWhere.com> writes:
>>
>>>> All you do is assert that H decides ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>>>>
>>>>> Are you willing to admit that if it is shown that H correctly decides
>>>>> the halt status of ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted or are you going
>>>>> to dishonestly dodge this key point?
>>>>
>>>> I keep trying not to dodge it but you keep ignoring my answer.  No
>>>> proof
>>>> is invalided by other truths.  You might render all of mathematics
>>>> inconsistent, but previously valid chains of reasoning remains valid.
>>>>
>>>> You made it plain that don't accept what a proof is when you stated
>>>> that
>>>> if A,B,C ⊦ X, then ~A,A,B,C ⊬ X.  As far as I know you have never
>>>> retracted this incorrect statement.
>>>>
>>>> As it happens, you can't show that Linz's H is correct about the input
>>>> ⟨Ĥ⟩ ⟨Ĥ⟩, so the point is moot, but I have been trying to get you to
>>>> note
>>>> my answer to this hypothetical question for years, but you keep
>>>> pretending not to notice.
>>>
>>> I ask you a YES / NO question and you dodge.
>>
>> How could you miss the answer yet again?  Clearly it's no: I don't
>> accept that if it is shown that H correctly decides the halt status of
>> ⟨Ĥ⟩ ⟨Ĥ⟩ that Linz has been refuted.
>
> So you reject the idea of a semantic tautology.
> If X says Y is true and I prove that Y is false then X could still be
> correct. No wonder we are having trouble communicating, you are simply
> irrational.
>

Perhaps in smaller words so you can understand.

IF we have one proof that says X.

And we then come up with another proof that says Not X.

That second proof does NOT 'disprove' the first proof.

What it does is point out that either there is a flaw in ONE of the
proofs, or the logical system is invalid.

Linz's proof does rigerously show that by the logic, there exists no H
that that can correctly predict that halting status of all possible
inputs by showing an input that he logically proves can such an h can
not answer.

Even if you show an H that you claim solves that input, that in no way
'disproves' Linz proof. All it shows is that one of the two proofs,
either Linz's or yours has a logical flaw, or that the logic system used
is flawed as it has gone inconsistent.

You do NOT disprove a proof by showing a counter example. You can
disprove an UNPROVEN theorem or supposition by showing a counter
example, but this does NOT apply to a proven statement.

To disprove a proof, you have to point out an actual logical flaw in the
proof, that is show that some logical operation performed is not a valid
logical operation or that some input proposition taken as true is incorrect.

You have not done this, so you can NOT have 'disproven Linz'. At best
you have shown the logic system to be inconsistent, but in truth, the
errors in your proof have been pointed out, so all you have really
proven is that you don't know how to make a proper logical proof.

>>  How was "no proof is invalided by
>> other truths" not clearly a "no"?  I had no idea you would need it
>> spelled out.
>>
>> Anyway, I've spelled it out now: no.  If you want to see why you are
>> wrong to think the answer might be yes, the explanation is all there.
>>
>
>

On 10/27/21 10:21 AM, olcott wrote:
> On 10/27/2021 8:15 AM, Ben Bacarisse wrote:
>> olcott <NoOne@NoWhere.com> writes:
>>
>>> On 10/26/2021 6:19 PM, Ben Bacarisse wrote:
>>>> olcott <NoOne@NoWhere.com> writes:
>>>>
>>>>> On 10/26/2021 9:28 AM, Ben Bacarisse wrote:
>>>>>> olcott <NoOne@NoWhere.com> writes:
>>>>>>
>>>>>>> Linz's "proof" that no universal halt decider exists is entirely
>>>>>>> based
>>>>>>> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>>>>>> It's a proof, not a "proof".  It only becomes a "proof" when someone
>>>>>> finds a mistake in it.  And it does not rely on his beliefs.
>>>>>> That's not
>>>>>> the word to use when talking about simple logic like this:
>>>>>
>>>>> Because this is necessarily true (only a fool would disagree)
>>>>>
>>>>> Simulating Halt Decider Theorem (Olcott 2021):
>>>>> Whenever simulating halt decider H correctly determines that input P
>>>>> never reaches its final state (whether or not its simulation of P is
>>>>> aborted) then H correctly decides that P never halts.
>>>> What is H?
>>> a simulating halt decider
>>
>> This does not specify H.  Is this the behaviour you want or expect H to
>> exhibit:
>>
>>    Hq0 <M> s ⊦* Hqy    if M applied to s halts, and
>>    Hq0 <M> s ⊦* Hqn    if M applied to s does not halt?
>>
>> I doubt it, but please either confirm that when you write H you mean a
>> TM with the above behaviour, or, if you are using H to mean a TM that
>> might deviate from this specification, please give the actual
>> specification.  *And stop calling it H!*
>>
>>>> What is P?
>>> input to Simulating Halt Decider
>>>
>>>> What is a correct decision?
>>>
>>> Reports whether or not simulated input reaches its final state
>>>
>>>> What does it mean
>>>> to say an input does or does not halt?
>>>
>>> the simulation of the input never reaches its final state
>>> (whether or not its simulation of P is aborted)
>>
>> A proper simulation (by a UTM) matches the halting behaviour of the
>> encoded TM.  I.e. this:
>>
>>    Hq0 <M> s ⊦* Hqy    if UTM(<M>, s) reaches M's halt state, and
>>    Hq0 <M> s ⊦* Hqn    if UTM(<M>, s) does not reach M's halt state
>>
>> is exactly the same as the much simpler description above so the mystery
>> word "abort" (TM don't "abort") is hiding those cases where you intend a
>> decider to be wrong about some inputs.
>>
>> If there are no inputs your imagined TM gets wrong (i.e. what you call H
>> really is what Linz calls H) then your "theorem" is just a badly worded
>> statement about a non-existent class of Turing machines.
>>
>>>> Linz's proof does not leave any
>>>> of these things unspecified.  He defines what H should do in all cases.
>>>> He does not introduce new symbols like P without definition.  (The last
>>>> time you used P it as a scrap of C code, not an input string to a
>>>> Turning machine.)
>>>>
>>>>> As soon as I show that Ĥq0 <Ĥ> <Ĥ> meets the above theorem then Linz
>>>>> has been refuted. Only a fool would disagree.
>>>> No.  You need to point out where Linz goes wrong, not pontificate about
>>>> an ill-defined "theorem".
>>>
>>> Linz is wrong is his final conclusion at the top of page 320.
>>> https://www.liarparadox.org/Peter_Linz_HP(Pages_315-320).pdf
>>
>> So the step you think is wrong is to determine what Ĥ applied to <Ĥ>
>> does by substituting specific values (Ĥ for M and <Ĥ> for <M>) into the
>> previous, correctly derived equation?  That's an odd complaint.  What's
>> wrong with the substitution?
>>
>>> q0 ⟨Ĥ⟩ ⊢* Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥqn
>>
>> Remember to add "if Ĥ applied to ⟨Ĥ⟩ does not halt".  Without that
>> condition, you are not talking about the proof you are trying to
>> invalidate.
>>
>> (Aside: this notation is a step backwards.  Writing Ĥq0 when you don't
>> mean state q0 of Ĥ is just silly.  You could call in Hq0 or H'q0 because
>> it is the state that corresponds to the initial states of both H and H',
>> but Ĥq0 is just an awful name.)
>>
>> I cut the rest because it does not explain why you reject that final
>> substitution step.  If you think it does, put it back in reply to my
>> question ("What's wrong with the substitution?") and I'll try to explain
>> it to you.
>>
>
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
> If the UTM simulation of the input to Ĥqx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach its
> final state (whether or not this simulation is aborted) then it is
> necessarily true that Ĥqx transitions to Ĥ.qn correctly.

Finally, you use the right words. We Know that UTM(<H^> <H^>) will act
exactly like H^<H^>).

We have that:
q0 ⟨Ĥ⟩ ⊢* Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥqn

Where the above initial q0 is that starting state of H^, so this is
showing the behavior of H^ (<H^>) which we see ends up at H^qn which is
defined as a terminal state for H^, so this PROVES that H^ applied to
<H^> is a Halting Computation.
>
> The mistake that Linz makes on the top of page 320 is that he wrongly
> assumes that Ĥ.qx is deciding the halt status of itself.

Since H^.qx is where we placed a copy of the code of H, we know by
definition that the behavior from H^.qx will be identical to the
behavior of the machine H. Since you have stipulated that H(<H^><H^>)
will say halting, that means that H.q0 <H^> <H^> goes to H.qn and thus
H^q0 <H^><H^> also goes to H^qn, which as we noted above halts.

>
> As long as halt decider H has correctly decided the halt status of its
> input P then the halt status of P was correctly decided by H and nothing
> in the universe can possibly contradict this.
>

Except that H has said that H^(<H^>) will never halt, when it does, so H
did NOT correct decide the Halting status of the input <H^> <H^>.

The problem is that it made its decision based on UNSOUND logic, by
assuming that the copy of H that it sees inside H^ would NOT abort its
simulation, but, since H is a Computation, we know that this copy of H
inside H^ will behave exactly like the copy of H doing the decision,
since they both have the exact same input.

Since the deciding H will abort its simulation, so will the copy in the
simulation, but the point in time when that will happen will be after
the point in time when the simulating H 'gives up', makes the wrong
decision, and aborts it simulation, so it will never see that happen.

When we simulate that exact same input with a UTM, as your stated
condition above says, THAT will continue to see that simulated H also
abort is simulation and return the non-halting answer (making exactly
the same error as the original H).

On 10/27/2021 6:46 PM, Richard Damon wrote:
>
> On 10/27/21 10:21 AM, olcott wrote:
>> On 10/27/2021 8:15 AM, Ben Bacarisse wrote:
>>> olcott <NoOne@NoWhere.com> writes:
>>>
>>>> On 10/26/2021 6:19 PM, Ben Bacarisse wrote:
>>>>> olcott <NoOne@NoWhere.com> writes:
>>>>>
>>>>>> On 10/26/2021 9:28 AM, Ben Bacarisse wrote:
>>>>>>> olcott <NoOne@NoWhere.com> writes:
>>>>>>>
>>>>>>>> Linz's "proof" that no universal halt decider exists is entirely
>>>>>>>> based
>>>>>>>> on his belief that H cannot decide ⟨Ĥ⟩ ⟨Ĥ⟩ correctly.
>>>>>>> It's a proof, not a "proof".  It only becomes a "proof" when someone
>>>>>>> finds a mistake in it.  And it does not rely on his beliefs.
>>>>>>> That's not
>>>>>>> the word to use when talking about simple logic like this:
>>>>>>
>>>>>> Because this is necessarily true (only a fool would disagree)
>>>>>>
>>>>>> Simulating Halt Decider Theorem (Olcott 2021):
>>>>>> Whenever simulating halt decider H correctly determines that input P
>>>>>> never reaches its final state (whether or not its simulation of P is
>>>>>> aborted) then H correctly decides that P never halts.
>>>>> What is H?
>>>> a simulating halt decider
>>>
>>> This does not specify H.  Is this the behaviour you want or expect H to
>>> exhibit:
>>>
>>>    Hq0 <M> s ⊦* Hqy    if M applied to s halts, and
>>>    Hq0 <M> s ⊦* Hqn    if M applied to s does not halt?
>>>
>>> I doubt it, but please either confirm that when you write H you mean a
>>> TM with the above behaviour, or, if you are using H to mean a TM that
>>> might deviate from this specification, please give the actual
>>> specification.  *And stop calling it H!*
>>>
>>>>> What is P?
>>>> input to Simulating Halt Decider
>>>>
>>>>> What is a correct decision?
>>>>
>>>> Reports whether or not simulated input reaches its final state
>>>>
>>>>> What does it mean
>>>>> to say an input does or does not halt?
>>>>
>>>> the simulation of the input never reaches its final state
>>>> (whether or not its simulation of P is aborted)
>>>
>>> A proper simulation (by a UTM) matches the halting behaviour of the
>>> encoded TM.  I.e. this:
>>>
>>>    Hq0 <M> s ⊦* Hqy    if UTM(<M>, s) reaches M's halt state, and
>>>    Hq0 <M> s ⊦* Hqn    if UTM(<M>, s) does not reach M's halt state
>>>
>>> is exactly the same as the much simpler description above so the mystery
>>> word "abort" (TM don't "abort") is hiding those cases where you intend a
>>> decider to be wrong about some inputs.
>>>
>>> If there are no inputs your imagined TM gets wrong (i.e. what you call H
>>> really is what Linz calls H) then your "theorem" is just a badly worded
>>> statement about a non-existent class of Turing machines.
>>>
>>>>> Linz's proof does not leave any
>>>>> of these things unspecified.  He defines what H should do in all
>>>>> cases.
>>>>> He does not introduce new symbols like P without definition.  (The
>>>>> last
>>>>> time you used P it as a scrap of C code, not an input string to a
>>>>> Turning machine.)
>>>>>
>>>>>> As soon as I show that Ĥq0 <Ĥ> <Ĥ> meets the above theorem then Linz
>>>>>> has been refuted. Only a fool would disagree.
>>>>> No.  You need to point out where Linz goes wrong, not pontificate
>>>>> about
>>>>> an ill-defined "theorem".
>>>>
>>>> Linz is wrong is his final conclusion at the top of page 320.
>>>> https://www.liarparadox.org/Peter_Linz_HP(Pages_315-320).pdf
>>>
>>> So the step you think is wrong is to determine what Ĥ applied to <Ĥ>
>>> does by substituting specific values (Ĥ for M and <Ĥ> for <M>) into the
>>> previous, correctly derived equation?  That's an odd complaint.  What's
>>> wrong with the substitution?
>>>
>>>> q0 ⟨Ĥ⟩ ⊢* Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥqn
>>>
>>> Remember to add "if Ĥ applied to ⟨Ĥ⟩ does not halt".  Without that
>>> condition, you are not talking about the proof you are trying to
>>> invalidate.
>>>
>>> (Aside: this notation is a step backwards.  Writing Ĥq0 when you don't
>>> mean state q0 of Ĥ is just silly.  You could call in Hq0 or H'q0 because
>>> it is the state that corresponds to the initial states of both H and H',
>>> but Ĥq0 is just an awful name.)
>>>
>>> I cut the rest because it does not explain why you reject that final
>>> substitution step.  If you think it does, put it back in reply to my
>>> question ("What's wrong with the substitution?") and I'll try to explain
>>> it to you.
>>>
>>
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>> If the UTM simulation of the input to Ĥqx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach
>> its final state (whether or not this simulation is aborted) then it is
>> necessarily true that Ĥqx transitions to Ĥ.qn correctly.
>
> Finally, you use the right words. We Know that UTM(<H^> <H^>) will act
> exactly like H^<H^>).
>
> We have that:
> q0 ⟨Ĥ⟩ ⊢* Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥqn
>
> Where the above initial q0 is that starting state of H^, so this is
> showing the behavior of H^ (<H^>) which we see ends up at H^qn which is
> defined as a terminal state for H^, so this PROVES that H^ applied to
> <H^> is a Halting Computation.
That Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ halts is not the question.
The simulation of ⟨Ĥ⟩ ⟨Ĥ⟩ by Ĥq0 never halts is the answer.

If the halt decider correctly decides the halt status of its input then
it is correct no matter what else:

If when we directly execute Ĥ applied to ⟨Ĥ⟩ and it:
(a) Halts.
(b) Destroys the whole universe.
(c) Converts all fascists to true Christianity.
(d) Circumnavigates the globe.
(e) Cures cancer.
(f) Raises the dead.

It has still correctly decided the halt status of its input.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 10/27/21 9:39 PM, olcott wrote:
> On 10/27/2021 6:46 PM, Richard Damon wrote:
>>
>> On 10/27/21 10:21 AM, olcott wrote:
>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>>> If the UTM simulation of the input to Ĥqx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach
>>> its final state (whether or not this simulation is aborted) then it
>>> is necessarily true that Ĥqx transitions to Ĥ.qn correctly.

^^^^^^^^^^^^^^^^^ NOTE WHAT YOU SAID HERE ^^^^^^^^^^^^^^^^^^^^^^^^

>>
>> Finally, you use the right words. We Know that UTM(<H^> <H^>) will act
>> exactly like H^<H^>).
>>
>> We have that:
>> q0 ⟨Ĥ⟩ ⊢* Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥqn
>>
>> Where the above initial q0 is that starting state of H^, so this is
>> showing the behavior of H^ (<H^>) which we see ends up at H^qn which
>> is defined as a terminal state for H^, so this PROVES that H^ applied
>> to <H^> is a Halting Computation.
> That Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ halts is not the question.
> The simulation of ⟨Ĥ⟩ ⟨Ĥ⟩ by Ĥq0 never halts is the answer.

No, as you said earlier, it is what the input to H (or H^q0) would do if
it was made the input to a UTM, NOT your 'non-utm' partial simulation H.

The right answer to the Halting Problem is ALWAYS about the actual
machine who has been converted into a representation to give to the
decider, never about what happens in the decider.

>
> If the halt decider correctly decides the halt status of its input then
> it is correct no matter what else:

But it DOESN'T decide correctly. So, yes, if it decided correctly, it is
correct, but it it decides incorrectly, it is incorrect.

>
> If when we directly execute Ĥ applied to ⟨Ĥ⟩ and it:
> (a) Halts.
> (b) Destroys the whole universe.
> (c) Converts all fascists to true Christianity.
> (d) Circumnavigates the globe.
> (e) Cures cancer.
> (f) Raises the dead.
>
> It has still correctly decided the halt status of its input.
>

Why does the thing DEFINED to be the source of the right answer not
matter, but something that isn't defined that we do?

You are just showing how ignorant of the problem you are.

Occationally, you 'goof' and give the right words, which shows you may
actually know the truth, and are just a pathological liar, doomed
forever to have to live with your lies.

On 10/27/2021 8:55 PM, Richard Damon wrote:
> On 10/27/21 9:39 PM, olcott wrote:
>> On 10/27/2021 6:46 PM, Richard Damon wrote:
>>>
>>> On 10/27/21 10:21 AM, olcott wrote:
>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>>>> If the UTM simulation of the input to Ĥqx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach
>>>> its final state (whether or not this simulation is aborted) then it
>>>> is necessarily true that Ĥqx transitions to Ĥ.qn correctly.
>
> ^^^^^^^^^^^^^^^^^ NOTE WHAT YOU SAID HERE ^^^^^^^^^^^^^^^^^^^^^^^^
>
>>>
>>> Finally, you use the right words. We Know that UTM(<H^> <H^>) will
>>> act exactly like H^<H^>).
>>>
>>> We have that:
>>> q0 ⟨Ĥ⟩ ⊢* Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥqn
>>>
>>> Where the above initial q0 is that starting state of H^, so this is
>>> showing the behavior of H^ (<H^>) which we see ends up at H^qn which
>>> is defined as a terminal state for H^, so this PROVES that H^ applied
>>> to <H^> is a Halting Computation.
>> That Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ halts is not the question.
>> The simulation of ⟨Ĥ⟩ ⟨Ĥ⟩ by Ĥq0 never halts is the answer.
>
> No, as you said earlier, it is what the input to H (or H^q0) would do if
> it was made the input to a UTM, NOT your 'non-utm' partial simulation H.
>
> The right answer to the Halting Problem is ALWAYS about the actual
> machine who has been converted into a representation to give to the
> decider, never about what happens in the decider.

So then you are saying that when the halt decider does correctly decide
that its input never halts that it can still be wrong?

That is irrational.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 10/27/21 10:18 PM, olcott wrote:
> On 10/27/2021 8:55 PM, Richard Damon wrote:
>> On 10/27/21 9:39 PM, olcott wrote:
>>> On 10/27/2021 6:46 PM, Richard Damon wrote:
>>>>
>>>> On 10/27/21 10:21 AM, olcott wrote:
>>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>>>>> If the UTM simulation of the input to Ĥqx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach
>>>>> its final state (whether or not this simulation is aborted) then it
>>>>> is necessarily true that Ĥqx transitions to Ĥ.qn correctly.
>>

^^^^^^^^^^^^^^^^ NOTE WHAT YOU SAID HERE ^^^^^^^^^^^^^^^^^^^^^^^^

>>
>>>>
>>>> Finally, you use the right words. We Know that UTM(<H^> <H^>) will
>>>> act exactly like H^<H^>).
>>>>
>>>> We have that:
>>>> q0 ⟨Ĥ⟩ ⊢* Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥqn
>>>>
>>>> Where the above initial q0 is that starting state of H^, so this is
>>>> showing the behavior of H^ (<H^>) which we see ends up at H^qn which
>>>> is defined as a terminal state for H^, so this PROVES that H^
>>>> applied to <H^> is a Halting Computation.
>>> That Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ halts is not the question.
>>> The simulation of ⟨Ĥ⟩ ⟨Ĥ⟩ by Ĥq0 never halts is the answer.
>>
>> No, as you said earlier, it is what the input to H (or H^q0) would do
>> if it was made the input to a UTM, NOT your 'non-utm' partial
>> simulation H.
>>
>> The right answer to the Halting Problem is ALWAYS about the actual
>> machine who has been converted into a representation to give to the
>> decider, never about what happens in the decider.
>
> So then you are saying that when the halt decider does correctly decide
> that its input never halts that it can still be wrong?
>
> That is irrational.
>

No, if it WAS right about the RIGHT question, it would be right.

THe problem is you look at the wrong question, because you think that a
simulator that stops is simulation is somehow the 'same' as a simulator
that never stops it simulation until it actually finishes.

As you said in the paragraph I pointed out above, what matters is what a
UTM does with that input. and a real UTM doesn't stop until its
simulation reaches an end, and when we do that, the computation halts.

(Note, that is NOT changing H to be a UTM, that is changing JUST the top
level machien with the UTM, leaving the code for the input, which
INCLUDES its copy of H, the original one, that does abort its
simulation, incorrectly)

You either have the wrong answer to the right question or a maybe right
answer to the wrong questions, but these two wrongs don't make a right,
you are just wrong.

YOU are irrational.

FAIL.

On 2021-10-27 20:18, olcott wrote:
> On 10/27/2021 8:55 PM, Richard Damon wrote:
>> On 10/27/21 9:39 PM, olcott wrote:
>>> On 10/27/2021 6:46 PM, Richard Damon wrote:
>>>>
>>>> On 10/27/21 10:21 AM, olcott wrote:
>>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>>>>> If the UTM simulation of the input to Ĥqx ⟨Ĥ⟩ ⟨Ĥ⟩ would never reach
>>>>> its final state (whether or not this simulation is aborted) then it
>>>>> is necessarily true that Ĥqx transitions to Ĥ.qn correctly.
>>
>> ^^^^^^^^^^^^^^^^^ NOTE WHAT YOU SAID HERE ^^^^^^^^^^^^^^^^^^^^^^^^
>>
>>>>
>>>> Finally, you use the right words. We Know that UTM(<H^> <H^>) will
>>>> act exactly like H^<H^>).
>>>>
>>>> We have that:
>>>> q0 ⟨Ĥ⟩ ⊢* Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥqn
>>>>
>>>> Where the above initial q0 is that starting state of H^, so this is
>>>> showing the behavior of H^ (<H^>) which we see ends up at H^qn which
>>>> is defined as a terminal state for H^, so this PROVES that H^
>>>> applied to <H^> is a Halting Computation.
>>> That Ĥq0 ⟨Ĥ⟩ ⟨Ĥ⟩ halts is not the question.
>>> The simulation of ⟨Ĥ⟩ ⟨Ĥ⟩ by Ĥq0 never halts is the answer.
>>
>> No, as you said earlier, it is what the input to H (or H^q0) would do
>> if it was made the input to a UTM, NOT your 'non-utm' partial
>> simulation H.
>>
>> The right answer to the Halting Problem is ALWAYS about the actual
>> machine who has been converted into a representation to give to the
>> decider, never about what happens in the decider.
>
> So then you are saying that when the halt decider does correctly decide
> that its input never halts that it can still be wrong?
>
> That is irrational.

You've got that completely ass-backwards. You're the one arguing that
when your decider gets the wrong answer as defined by the problem it is
somehow still deciding 'correctly'.

*THAT's* irrational.

André

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.