Olcott's theory

[Mr Flibble]

I agree with Olcott that a halt decider can NOT be part of that which
is being decided (see [Strachey 1965]) which, if Olcott is correct,
falsifies a collection of proofs (which I don't have the time to
examine) which rely on that mistake. The mistake Olcott seems to be
making is inferring that just because those proofs are invalid then that
somehow means that the halting problem itself is not undecidable.

/Flibble

[olcott]

[An impossible program] C. Strachey
The Computer Journal, Volume 7, Issue 4, January 1965, Page 313,
https://doi.org/10.1093/comjnl/7.4.313

https://academic.oup.com/comjnl/article/7/4/313/354243

No I never made that mistake, My goal since 2004 has always been to
simply prove that the proofs are incorrect. Here is my original 2004
claim that everyone has disagreed with in more than 15,000 messages
since 2004:

[Halting Problem Final Conclusion]
comp.theory Peter Olcott Sep 5, 2004, 11:21:57 AM
The Liar Paradox can be shown to be nothing more than
a incorrectly formed statement because of its pathological
self-reference. The Halting Problem can only exist because
of this same sort of pathological self-reference.
https://groups.google.com/g/comp.theory/c/RO9Z9eCabeE/m/Ka8-xS2rdEEJ

--
Copyright 2021 Pete Olcott

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

[Mr Flibble]

On Sat, 10 Jul 2021 12:08:02 -0500
olcott <No...@NoWhere.com> wrote:

> The Halting Problem can only exist because
> of this same sort of pathological self-reference.

^ that is your mistake: the halting problem still exists even if a
collection of proofs have a mistake.

Does [Turing 1937] rely on a decider being part of that which is
being decided? Wikipedia suggests not:

"Turing's proof departs from calculation by recursive functions and
introduces the notion of computation by machine."

/Flibble

[olcott]

*I agree that I have not solved the halting problem*
At most I have only proved that the conventional proofs of the
undecidability of the halting problem that rely on the Strachey form,
are incorrect. This seems to include all textbook proofs.

[An impossible program] C. Strachey
The Computer Journal, Volume 7, Issue 4, January 1965, Page 313,
https://doi.org/10.1093/comjnl/7.4.313

Now seems to be a good time to finally look at the Turing proof.
https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf
I am not sure if the above linked copy has the later published correction.

If the Turing proof is isomorphic to the Strachey form, I don't know
what it left to prove that the halting problem is undecidable.

Goldbach's Conjecture is merely undecided and thus not undecidable.
https://en.wikipedia.org/wiki/Goldbach%27s_conjecture

Busy Beaver only seems intractable not undecidable.
https://en.wikipedia.org/wiki/Busy_beaver

[Mr Flibble]

On Sat, 10 Jul 2021 13:06:35 -0500
olcott <No...@NoWhere.com> wrote:

> On 7/10/2021 12:12 PM, Mr Flibble wrote:
> > On Sat, 10 Jul 2021 12:08:02 -0500
> > olcott <No...@NoWhere.com> wrote:
> >
> >> The Halting Problem can only exist because
> >> of this same sort of pathological self-reference.
> >
> > ^ that is your mistake: the halting problem still exists even if a
> > collection of proofs have a mistake.
> >
> > Does [Turing 1937] rely on a decider being part of that which is
> > being decided? Wikipedia suggests not:
> >
> > "Turing's proof departs from calculation by recursive functions and
> > introduces the notion of computation by machine."
> >
> > /Flibble
> >
>
> *I agree that I have not solved the halting problem*
> At most I have only proved that the conventional proofs of the
> undecidability of the halting problem that rely on the Strachey form,
> are incorrect. This seems to include all textbook proofs.

You need to reign in the ego, mate, Strachey deserves the credit not
you unless you are claiming that you have independently reached the same
conclusion as Strachey without being aware of Strachey until recently?

/Flibble

[olcott]

All of the textbooks cite the Strachey form as proof that the halting
problem is undecidable. Ben, Mike and Kaz agree that the Strachey form
proves that the halting problem is undecidable.

rec routine P
§L:if T[P] go to L
Return §

If T[P] = True the routine P will loop, and it will
only terminate if T[P] = False. In each case T[P] has
exactly the wrong value, and this contradiction shows
that the function T cannot exist.

When Strachey says:
"this contradiction shows that the function T cannot exist."

He is saying that he just proved that a universal halt decider {function
T} does not exist.

[Mr Flibble]

On Sat, 10 Jul 2021 13:32:40 -0500

No he isn't; he is saying that a decider can not be part of what is
being decided which is quite different. If you are correct about all
the textbooks being wrong then the mistake there is the authors of the
textbooks not correctly understanding the implications of the
contradiction Strachey is highlighting which, as I said earlier, has no
bearing on the decidability of the halting problem itself.

/Flibble

[olcott]

So when Strachey says:
"this contradiction shows that the function T cannot exist."

Strachey does not mean
{this contradiction shows that the function T cannot exist.}

> If you are correct about all
> the textbooks being wrong then the mistake there is the authors of the
> textbooks not correctly understanding the implications of the
> contradiction Strachey is highlighting which, as I said earlier, has no
> bearing on the decidability of the halting problem itself.
>
> /Flibble
>

[Mr Flibble]

On Sat, 10 Jul 2021 13:45:38 -0500

He means T cannot decide on P if T is called from within P; i.e. the
"pathological self reference" you keep going on about.

/Flibble

[olcott]

Yes and he and everyone else here besides you and I believes that this

proves that the halting problem is undecidable.

[Mr Flibble]

On Sat, 10 Jul 2021 14:09:07 -0500

When I read Strachey's letter I didn't get the impression that that was
his conclusion; merely that T cannot decide on P if called from within
P .. i.e. the "Impossible Program".

/Flibble

[Peter]

There is more than one proof. I was taught, not the the halting problem
for TMs is unsolvable, but that the halting problem for register
machines is unsolvable. The reason being, I suppose, that the course
was taught by one of the inventors of the register machine. [There are
a variety of register machines, this one had an unlimited number of
registers and the instructions
add 1 to register R,
subtract 1 from register R (so long as it doesn't hold 0),
if R doesn't hold 0 go to instruction i.
See Shepherdson & Sturgis, 'Computability of recursive functions',
/JACM/, vol 10, no 2, 1963, pp217-255.]

>
> Goldbach's Conjecture is merely undecided and thus not undecidable.
> https://en.wikipedia.org/wiki/Goldbach%27s_conjecture
>
> Busy Beaver only seems intractable not undecidable.
> https://en.wikipedia.org/wiki/Busy_beaver
>
>
>


--

The world will little note, nor long remember what we say here
Abraham Lincoln at Gettysburg

[olcott]

None-the-less everyone else does get that impression.
All of the textbook halting problem undecidability proofs rely on the
Strachey form as their entire basis.

http://www.liarparadox.org/sipser_165.pdf

[Mr Flibble]

On Sat, 10 Jul 2021 14:32:10 -0500

Then you might be on to something but you need to stop implying the
halting problem itself is not undecidable in your posts as it doesn't
help your case (and is the reason I have been dismissive of your posts
in the past).

/Flibble

[olcott]

All of the proofs seem to boil down to this one idea:

An impossible program
C. Strachey
The Computer Journal, Volume 7, Issue 4, January 1965, Page 313,
https://doi.org/10.1093/comjnl/7.4.313

> add 1 to register R,
> subtract 1 from register R (so long as it doesn't hold 0),
> if R doesn't hold 0 go to instruction i.
> See Shepherdson & Sturgis, 'Computability of recursive functions',
> /JACM/, vol 10, no 2, 1963, pp217-255.]
>
>>
>> Goldbach's Conjecture is merely undecided and thus not undecidable.
>> https://en.wikipedia.org/wiki/Goldbach%27s_conjecture
>>
>> Busy Beaver only seems intractable not undecidable.
>> https://en.wikipedia.org/wiki/Busy_beaver
>>
>>
>>
>
>


--

[Chris M. Thomasson]

On 7/10/2021 12:35 PM, Mr Flibble wrote:
> On Sat, 10 Jul 2021 14:32:10 -0500
> olcott <No...@NoWhere.com> wrote:

[...]

>>>> Yes and he and everyone else here besides you and I believes that
>>>> this proves that the halting problem is undecidable.
>>>
>>> When I read Strachey's letter I didn't get the impression that that
>>> was his conclusion; merely that T cannot decide on P if called from
>>> within P .. i.e. the "Impossible Program".
>>>
>>> /Flibble
>>>
>>
>> None-the-less everyone else does get that impression.
>> All of the textbook halting problem undecidability proofs rely on the
>> Strachey form as their entire basis.
>>
>> http://www.liarparadox.org/sipser_165.pdf
>
> Then you might be on to something but you need to stop implying the
> halting problem itself is not undecidable in your posts as it doesn't
> help your case (and is the reason I have been dismissive of your posts
> in the past).

Great advise!

[olcott]

Like I already explained in much more words with many more key details,
if none of these conventional (Strachey based) undecidability proofs are
correct then that doesn't seem to leave any other proof of halting
undecidability:

Goldbach's Conjecture is merely undecided and thus not undecidable.
https://en.wikipedia.org/wiki/Goldbach%27s_conjecture

Busy Beaver only seems intractable thus not undecidable.
https://en.wikipedia.org/wiki/Busy_beaver

It is probably a good time for me to take a first look at the actual
Turing proof. I merely need to verify that it is isomorphic to the
Strachey form.

[Mr Flibble]

On Sat, 10 Jul 2021 16:12:12 -0500

You are still missing the point: even if [Turing 1937] has the same
mistake you still cannot prove that the halting problem itself is not
undecidable just because that particular proof is invalid.

/Flibble

[olcott]

None-the-less once the halting problem is no longer provably undecidable
computation loses its definite limits.

The key other aspect of this is that the Tarski undefinability theorem
can be understood to fail for the same reason that the halting theorem
fails.

This can have an explosive effect on AI research. Davidson's truth
conditional semantics can finally be anchored in a formal mathematical
notion of truth.

[Mr Flibble]

On Sat, 10 Jul 2021 16:46:28 -0500

No, a lack of a proof showing that the halting problem is undecidable
does NOT imply that the halting problem is not undecidable; that still
needs to be proven.

[snip]

/Flibble

[olcott]

It transforms what was previously thought to be known as a definite
limit to all computation into no known limit to computation. This is huge.

[Mr Flibble]

On Sat, 10 Jul 2021 16:58:13 -0500

Mr Flibble is very cross.

https://www.youtube.com/watch?v=AOE7qTAK87o

/Flibble

[olcott]

That was great.

[Chris M. Thomasson]

On 7/10/2021 3:00 PM, Mr Flibble wrote:
> On Sat, 10 Jul 2021 16:58:13 -0500
> olcott <No...@NoWhere.com> wrote:

[...]

>> It transforms what was previously thought to be known as a definite
>> limit to all computation into no known limit to computation. This is
>> huge.
>
> Mr Flibble is very cross.
>
> https://www.youtube.com/watch?v=AOE7qTAK87o

LOL!!! :^D

[Peter]

And you know that how? Have you read _all_ of the proofs?

>> add 1 to register R,
>> subtract 1 from register R (so long as it doesn't hold 0),
>> if R doesn't hold 0 go to instruction i.
>> See Shepherdson & Sturgis, 'Computability of recursive functions',
>> /JACM/, vol 10, no 2, 1963, pp217-255.]
>>
>>>
>>> Goldbach's Conjecture is merely undecided and thus not undecidable.
>>> https://en.wikipedia.org/wiki/Goldbach%27s_conjecture
>>>
>>> Busy Beaver only seems intractable not undecidable.
>>> https://en.wikipedia.org/wiki/Busy_beaver
>>>
>>>
>>>
>>
>>
>
>


--

[olcott]

All of the textbooks have this same proof.
As long as the Turing proof is based on the same idea I am set.

>>> add 1 to register R,
>>> subtract 1 from register R (so long as it doesn't hold 0),
>>> if R doesn't hold 0 go to instruction i.
>>> See Shepherdson & Sturgis, 'Computability of recursive functions',
>>> /JACM/, vol 10, no 2, 1963, pp217-255.]
>>>
>>>>
>>>> Goldbach's Conjecture is merely undecided and thus not undecidable.
>>>> https://en.wikipedia.org/wiki/Goldbach%27s_conjecture
>>>>
>>>> Busy Beaver only seems intractable not undecidable.
>>>> https://en.wikipedia.org/wiki/Busy_beaver
>>>>
>>>>
>>>>
>>>
>>>
>>
>>
>
>


--

[Ben Bacarisse]

olcott <No...@NoWhere.com> writes:

> All of the textbooks have this same proof.

You have not even read the proper proof given in the textbook that you
appear to have: "An Introduction to Formal Languages and Automata" by
Peter Linz.

> As long as the Turing proof is based on the same idea I am set.

Turing never published a proof of the halting theorem, though he
certainly knew it. His 1936 paper was not concerned with halting, but
with defining "commutable numbers".

I think it was Martin Davis who coined the term "halting problem", but
his use of the terms is not what you would recognise, and the proof is
entirely different.

I don't know who first published a proof of the form you are so obsessed
with. If anyone knows, I'd like to hear about it. Of course it comes
in many guises, for Turing machines and other models like register
machines (as I first encountered it), so maybe it was not originally
given for TMs at all?

--
Ben.

[wij]

I have composed an axiom that clarifies the issue. I am convinced no one
have ever said the same thing as General Undecidable Axioms says:
+----------------------------------------------------------------------------------+
| No TM U can decide the property of a TM P if that property can be defied by TM P. |
+----------------------------------------------------------------------------------+

https://groups.google.com/g/comp.theory/c/65ZaXe9Sabk
--
Copyright 2021 WIJ

[olcott]

On 7/10/2021 8:56 PM, Ben Bacarisse wrote:
> olcott <No...@NoWhere.com> writes:
>
>> All of the textbooks have this same proof.
>
> You have not even read the proper proof given in the textbook that you
> appear to have: "An Introduction to Formal Languages and Automata" by
> Peter Linz.
>
>> As long as the Turing proof is based on the same idea I am set.
>
> Turing never published a proof of the halting theorem, though he
> certainly knew it. His 1936 paper was not concerned with halting, but
> with defining "commutable numbers".
>

Yes numbers that live in New Jersey and go to work in New York city.
They commute to work.

> I think it was Martin Davis who coined the term "halting problem", but
> his use of the terms is not what you would recognise, and the proof is
> entirely different.
>
> I don't know who first published a proof of the form you are so obsessed
> with. If anyone knows, I'd like to hear about it. Of course it comes
> in many guises, for Turing machines and other models like register
> machines (as I first encountered it), so maybe it was not originally
> given for TMs at all?
>

This one is the the apparent forerunner to all of the pseudo-code proofs
and was written by the creator of the CPL programming language, the
ancestor to BCPL, B and C.

An impossible program C. Strachey
The Computer Journal, Volume 7, Issue 4, January 1965, Page 313,
https://doi.org/10.1093/comjnl/7.4.313

*Here are Strachey's (verbatim) own words*
Suppose T[R] is a Boolean function taking a routine
(or program) R with no formal or free variables as its
argument and that for all R, T[R] — True if R terminates
if run and that T[R] = False if R does not terminate.
Consider the routine P defined as follows

rec routine P
§L:if T[P] go to L
Return §

If T[P] = True the routine P will loop, and it will
only terminate if T[P] = False. In each case T[P] has
exactly the wrong value, and this contradiction shows
that the function T cannot exist.

Strachey is the creator of CPL ancestor to BCPL then B then C
His code above is written in his CPL programming language.

He was criticized in that his use of terminology is not precisely
correct by modern standards, yet apparently the essence of what he
conveyed is exactly correct.

I am happy to say that my C version works just fine:

// Simplified Linz Ĥ (Linz:1990:319)
void P(u32 x)
{
if (H(x, x))
HERE: goto HERE;
}

I will model my proof after Strachey instead of Linz, yet still
reference Linz.

_P()
[00000b66](01) 55 push ebp
[00000b67](02) 8bec mov ebp,esp
[00000b69](03) 8b4508 mov eax,[ebp+08]
[00000b6c](01) 50 push eax
[00000b6d](03) 8b4d08 mov ecx,[ebp+08]
[00000b70](01) 51 push ecx
[00000b71](05) e8f0fdffff call 00000966 // call H
[00000b76](03) 83c408 add esp,+08
[00000b79](02) 85c0 test eax,eax
[00000b7b](02) 7402 jz 00000b7f
[00000b7d](02) ebfe jmp 00000b7d
[00000b7f](01) 5d pop ebp
[00000b80](01) c3 ret
Size in bytes:(0027) [00000b80]

[Ben Bacarisse]

wij <wyn...@gmail.com> writes:

> I have composed an axiom that clarifies the issue. I am convinced no one
> have ever said the same thing as General Undecidable Axioms says:
> +----------------------------------------------------------------------------------+
> | No TM U can decide the property of a TM P if that property can be defied by TM P. |
> +----------------------------------------------------------------------------------+

I'm also pretty sure no one has ever said that. What does it mean? In
particular, what is a property of P that "can be defined by TM P"? May
this is your way of stating Rice's Theorem?

--
Ben.

[wij]

Examples are provided in
https://groups.google.com/g/comp.theory/c/65ZaXe9Sabk
It is an axiom, intuitive enough, proof is not really necessary.

--
Copyright 2021 WIJ

[Jeff Barnett]

Did they teach you that only two registers are necessary? That's the
most fun part of the result. Since the "two counter" machines have
exactly the same computation power as Turing machines, a no halt theory
for either extends to both. Automatic.

> See Shepherdson & Sturgis, 'Computability of recursive functions',
> /JACM/, vol 10, no 2, 1963, pp217-255.]
>
>>
>> Goldbach's Conjecture is merely undecided and thus not undecidable.
>> https://en.wikipedia.org/wiki/Goldbach%27s_conjecture
>>
>> Busy Beaver only seems intractable not undecidable.
>> https://en.wikipedia.org/wiki/Busy_beaver--

Jeff Barnett

[Jeff Barnett]

On 7/10/2021 7:56 PM, Ben Bacarisse wrote:
> olcott <No...@NoWhere.com> writes:
>
>> All of the textbooks have this same proof.
>
> You have not even read the proper proof given in the textbook that you
> appear to have: "An Introduction to Formal Languages and Automata" by
> Peter Linz.
>
>> As long as the Turing proof is based on the same idea I am set.
>
> Turing never published a proof of the halting theorem, though he
> certainly knew it. His 1936 paper was not concerned with halting, but
> with defining "commutable numbers".
>
> I think it was Martin Davis who coined the term "halting problem", but
> his use of the terms is not what you would recognise, and the proof is
> entirely different.

It was in the mid 1960s when Davis agreed to give a few of us 20
somethings a quick ad hoc class on this stuff. We got together an hour a
day for a few weeks. To my 50+ year old recollection, the
no-halting-machine proof he showed us was virtually identical to the one
in the Linz book.

> I don't know who first published a proof of the form you are so obsessed
> with. If anyone knows, I'd like to hear about it. Of course it comes
> in many guises, for Turing machines and other models like register
> machines (as I first encountered it), so maybe it was not originally
> given for TMs at all?--

Jeff Barnett

[Chris M. Thomasson]

On 7/10/2021 10:00 AM, Mr Flibble wrote:
> I agree with Olcott that a halt decider can NOT be part of that which
> is being decided (see [Strachey 1965]) which, if Olcott is correct,
> falsifies a collection of proofs (which I don't have the time to
> examine) which rely on that mistake. The mistake Olcott seems to be
> making is inferring that just because those proofs are invalid then that
> somehow means that the halting problem itself is not undecidable.


If he can tell me a complex multi-threaded program will halt or run
forever, for sure, I would be interested. No false results allowed.

I am thinking about something like this, with an abuse of using standard
race conditions in broken rmw's... Think if the logic of the program
used these race conditions from time to time to halt or not. Well, think
if a program flipped a coin and then decided not to halt or not based on
the result. It was all threaded and complex. ;^)

https://groups.google.com/g/comp.lang.c++/c/7u_rLgQe86k/m/XiqELOEECAAJ

If Peter can do that, WOW!!!

[Ben Bacarisse]

Jeff Barnett <j...@notatt.com> writes:

> On 7/10/2021 7:56 PM, Ben Bacarisse wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> All of the textbooks have this same proof.
>> You have not even read the proper proof given in the textbook that you
>> appear to have: "An Introduction to Formal Languages and Automata" by
>> Peter Linz.
>>
>>> As long as the Turing proof is based on the same idea I am set.
>> Turing never published a proof of the halting theorem, though he
>> certainly knew it. His 1936 paper was not concerned with halting, but
>> with defining "commutable numbers".
>> I think it was Martin Davis who coined the term "halting problem", but
>> his use of the terms is not what you would recognise, and the proof is
>> entirely different.
>
> It was in the mid 1960s when Davis agreed to give a few of us 20
> somethings a quick ad hoc class on this stuff. We got together an hour
> a day for a few weeks. To my 50+ year old recollection, the
> no-halting-machine proof he showed us was virtually identical to the
> one in the Linz book.

Where was this? Was anything published? Did you get the feeling he was
claiming the construction was his own invention?

My feeling is that the idea embodied in the "usual" construction was
just floating around as a rather obvious way to persuade those readers
who don't like the more formal proofs that textbooks tended to use.
This may be completely wrong, but since you were around at the time,
maybe you can shed some light on it.

--
Ben.

[Ben Bacarisse]

olcott <No...@NoWhere.com> writes:

> On 7/10/2021 8:56 PM, Ben Bacarisse wrote:
>> olcott <No...@NoWhere.com> writes:
>>
>>> All of the textbooks have this same proof.
>> You have not even read the proper proof given in the textbook that you
>> appear to have: "An Introduction to Formal Languages and Automata" by
>> Peter Linz.
>>
>>> As long as the Turing proof is based on the same idea I am set.
>> Turing never published a proof of the halting theorem, though he
>> certainly knew it. His 1936 paper was not concerned with halting, but
>> with defining "commutable numbers".
>
> Yes numbers that live in New Jersey and go to work in New York
> city. They commute to work.

Noted. This how you want discuss the matter is it? I can do it too.

> I am happy to say that my C version works just fine:

Not according to you. H(P,P) == 0 and P(P) halts.

> // Simplified Linz Ĥ (Linz:1990:319)
> void P(u32 x)
> {
> if (H(x, x))
> HERE: goto HERE;
> }

Still hiding H, I see.

--
Ben.

[Ben Bacarisse]

wij <wyn...@gmail.com> writes:

> On Sunday, 11 July 2021 at 10:34:36 UTC+8, Ben Bacarisse wrote:
>> wij <wyn...@gmail.com> writes:
>>
>> > I have composed an axiom that clarifies the issue. I am convinced no one
>> > have ever said the same thing as General Undecidable Axioms says:
>> > +----------------------------------------------------------------------------------+
>> > | No TM U can decide the property of a TM P if that property can be defied by TM P. |
>> > +----------------------------------------------------------------------------------+
>> I'm also pretty sure no one has ever said that. What does it mean? In
>> particular, what is a property of P that "can be defined by TM P"? May
>> this is your way of stating Rice's Theorem?
>>
>> --
>> Ben.

It's best not to quote sigs.

> Examples are provided in
> https://groups.google.com/g/comp.theory/c/65ZaXe9Sabk
> It is an axiom, intuitive enough, proof is not really necessary.

I was asking for an explanation of the words, but if you'd rather not
explain it here, I'm quite happy with that.

--
Ben.

[Peter]

You haven't read all the textbooks, and there are proofs in papers and
lectures. The mention of Martin Davis downstream led me to his book
/Computability and unsolvability/, McGraw-Hill 1958 (also recent Dover
republication). He proves the unsolvability of the halting problem by
noting that (exists y)T(x,x,y) is uncomputable (T being Kleene's T
predicate). You seem not to know what you are talking about.

> As long as the Turing proof is based on the same idea I am set.
>
>>>> add 1 to register R,
>>>> subtract 1 from register R (so long as it doesn't hold 0),
>>>> if R doesn't hold 0 go to instruction i.
>>>> See Shepherdson & Sturgis, 'Computability of recursive functions',
>>>> /JACM/, vol 10, no 2, 1963, pp217-255.]
>>>>
>>>>>
>>>>> Goldbach's Conjecture is merely undecided and thus not undecidable.
>>>>> https://en.wikipedia.org/wiki/Goldbach%27s_conjecture
>>>>>
>>>>> Busy Beaver only seems intractable not undecidable.
>>>>> https://en.wikipedia.org/wiki/Busy_beaver
>>>>>
>>>>>
>>>>>
>>>>
>>>>
>>>
>>>
>>
>>
>
>


--

[Peter]

Yes. The lecturer was John Shepherdson at Bristol.

>> See Shepherdson & Sturgis, 'Computability of recursive functions',
>> /JACM/, vol 10, no 2, 1963, pp217-255.]
>>
>>>
>>> Goldbach's Conjecture is merely undecided and thus not undecidable.
>>> https://en.wikipedia.org/wiki/Goldbach%27s_conjecture
>>>
>>> Busy Beaver only seems intractable not undecidable.
>>> https://en.wikipedia.org/wiki/Busy_beaver--
> Jeff Barnett
>

[olcott]

As long as my refutation of the halting problem proofs is correct then
this may seem to translate the halting problem from known to be
undecidable to unknown to be undecidable.

At that point teams of software engineers could begin working on
problems such as yours.

[wij]

In one core one clock CPU, "a complex multi-threaded program" is no powerful than TM.
In multi-core CPU, "a complex multi-threaded program" is no powerful than several TM's,
probably still not powerful than a single TM, in term of computational power.

[olcott]

https://en.wikipedia.org/wiki/Kleene%27s_T_predicate

That Gödel numbering crap simply hides the pathological
self-reference(Olcott 2004) error behind so much complexity that it
can't be seen.

When we ask what Boolean value can a halt decider return to an input
that changes its behavior to contradict this value we cannot answer this
question because it is an incorrect type mismatch error question. The
answer is restricted to {true, false} thus excluding the correct answer
of “neither” making the question itself incorrect. The TM / input pairs
that “prove” the halting problem is undecidable have the same
pathological self-reference(Olcott 2004) error as the self-contradictory
liar paradox.

To eliminate this pathological feedback loop error we examine the
behavior of the input with a pure simulator that has no effect
what-so-ever on the behavior of the input. As correct science requires
the dependent variable (the halt status decision) must only have the
independent variable (the behavior of the input) and be isolated from
all other influences. Only when we do it this way do we get the correct
halt status decision for the input.

Until the behavior of its input proves that it will never halt every H
remains a pure simulator of this input. This single fact by itself
proves that the behavior of H has no effect what-so-ever on its halt
status decision. When H stops simulating its input the execution of the
input has been suspended, this does not count as halting.

>> As long as the Turing proof is based on the same idea I am set.
>>
>>>>> add 1 to register R,
>>>>> subtract 1 from register R (so long as it doesn't hold 0),
>>>>> if R doesn't hold 0 go to instruction i.
>>>>> See Shepherdson & Sturgis, 'Computability of recursive functions',
>>>>> /JACM/, vol 10, no 2, 1963, pp217-255.]
>>>>>
>>>>>>
>>>>>> Goldbach's Conjecture is merely undecided and thus not undecidable.
>>>>>> https://en.wikipedia.org/wiki/Goldbach%27s_conjecture
>>>>>>
>>>>>> Busy Beaver only seems intractable not undecidable.
>>>>>> https://en.wikipedia.org/wiki/Busy_beaver
>>>>>>
>>>>>>
>>>>>>
>>>>>
>>>>>
>>>>
>>>>
>>>
>>>
>>
>>
>
>


--

[olcott]

On 7/10/2021 12:00 PM, Mr Flibble wrote:
> I agree with Olcott that a halt decider can NOT be part of that which
> is being decided (see [Strachey 1965]) which, if Olcott is correct,
> falsifies a collection of proofs (which I don't have the time to
> examine) which rely on that mistake. The mistake Olcott seems to be
> making is inferring that just because those proofs are invalid then that
> somehow means that the halting problem itself is not undecidable.
>

> /Flibble

>

An impossible program
C. Strachey
The Computer Journal, Volume 7, Issue 4, January 1965, Page 313,
https://doi.org/10.1093/comjnl/7.4.313

When we ask what Boolean value can a halt decider return to an input
that changes its behavior to contradict this value we cannot answer this
question because it is an incorrect type mismatch error question. The
answer is restricted to {true, false} thus excluding the correct answer
of “neither” making the question itself incorrect. The TM / input pairs
that “prove” the halting problem is undecidable have the same
pathological self-reference(Olcott 2004) error as the self-contradictory
liar paradox.

To eliminate this pathological feedback loop error we examine the
behavior of the input with a pure simulator that has no effect
what-so-ever on the behavior of the input. As correct science requires
the dependent variable (the halt status decision) must only have the
independent variable (the behavior of the input) and be isolated from
all other influences. Only when we do it this way do we get the correct
halt status decision for the input.

Until the behavior of its input proves that it will never halt every H
remains a pure simulator of this input. This single fact by itself
proves that the behavior of H has no effect what-so-ever on its halt
status decision. When H stops simulating its input the execution of the
input has been suspended, this does not count as halting.

Halt Deciding Axiom: When the pure simulation of the machine description
⟨P⟩ of a machine P on its input I never halts we know that P(I) never
halts. This axiom is met by the following:

Simulating halt decider H is only answering the question:
Would the input halt on its input if H never stopped simulating it?
(a) An answer of "no" universally means that the input never halts.
(b) An answer of "yes" universally means that the input halts.

[Jeff Barnett]

On 7/11/2021 3:23 AM, Ben Bacarisse wrote:
> Jeff Barnett <j...@notatt.com> writes:
>
>> On 7/10/2021 7:56 PM, Ben Bacarisse wrote:
>>> olcott <No...@NoWhere.com> writes:
>>>
>>>> All of the textbooks have this same proof.
>>> You have not even read the proper proof given in the textbook that you
>>> appear to have: "An Introduction to Formal Languages and Automata" by
>>> Peter Linz.
>>>
>>>> As long as the Turing proof is based on the same idea I am set.
>>> Turing never published a proof of the halting theorem, though he
>>> certainly knew it. His 1936 paper was not concerned with halting, but
>>> with defining "commutable numbers".
>>> I think it was Martin Davis who coined the term "halting problem", but
>>> his use of the terms is not what you would recognise, and the proof is
>>> entirely different.
>>
>> It was in the mid 1960s when Davis agreed to give a few of us 20
>> somethings a quick ad hoc class on this stuff. We got together an hour
>> a day for a few weeks. To my 50+ year old recollection, the
>> no-halting-machine proof he showed us was virtually identical to the
>> one in the Linz book.
>
> Where was this? Was anything published? Did you get the feeling he was
> claiming the construction was his own invention?

There was a nationally chartered nonprofit, the System Development
Corporation, that was created from a chunk the RAND Corporation (RAND as
in Santa Monica California, not Sperry Rand) in the late 1950s. SDC
consisted of divisions of two sorts: those that experimented with
development of large defense systems such as the early warning stuff on
the DEW line in Canada to sense polar route attacks; other divisions
were two for research and technology (all computer science). By the time
I went there (early middle 1960s), the R&T divisions were major
recipients of one of the DARPA block grants.

SDC R&T did many things of interest to you, I think. For example:
Seymour Ginsburg, Gene Rose, and Shelia Greibach were doing work in
formal language theory. Seymour had a knack for identifying folks in the
field who were about to pop something significant and finding funds so
they could spend their sabbaticals at SDC so a ton of papers were
published from there in formal language theory. In a more pragmatic
vein, Erwin Book and Val Schorre developed early, industrial strength
meta compilers one of which was used in early JOVIAL development. JOVIAL
= Jules' Own Version of the International Algorithmic Language. Jules
was the head of the T in R&T and his daughter, they lived next door, was
my eldest`s first babysitter.

Other developments in R&T were an industrial weight time sharing system
that was working within a month of MIT's; early network experiments that
lead to BBN and SDC being the only two invited to submit proposals for
the original DARPA Net; I worked on something Called LISP 2 - supposed
to mature LISP and combine it with some ALGOL ideas (Marvin Minsky and
John McCarthy were official god fathers - Alan Perlis was step uncle);
and there was what I called our Philosophy initiative that sponsored
interesting visitors who stayed around for a while - Martin Davis and
Yehoshua Bar-Hillel were examples here - I think this sprung from an
interest in formal logic and automating theorem proving; early work in
computational linguistics including a project to read and internalize
the Golden Book Encyclopedia - they were still on the "Aardvark" entry
and a fairly large speech understanding effort in the 1970s.

My group consisted mostly college dropouts that were more concerned with
computers, mathematics. and science then school. About half were MIT
affiliated. We would visit Minsky and McCarthy every few months. We
would usually take a red eye to Boston, go to the top of Tech Square
were the "MAC Hackers" would meet us. The next day we would "play" with
Minsky, see Seymour Papert and others for diner and generally catch up
on what was going on in the world. That evening or the next we would
find a land rover left for us by one of my colleague`s parents and drive
through the night to New York were one of us was an NYU professor (not a
dropout). On those drives we took turns presenting seminars on logic and
general topics in CS. That was a good chunk of my "formal" education.

In any event when we found Davis among us we descended on him en masse
and demanded a class on everything he knew. He consented, partially, and
we got him for a few weeks and took a tour of a fascinating world. He
was quite into diagonal arguments; I think he thought they were pretty,
easy to teach, and easy to understand (I don't think he every met PO).
He followed good teaching practice and did not point out what was to his
credit though he did mention many others by name. I think he decided
that the group was motivated to learn and absorb the information and
that the best he could do for us was introduce us to reusable techniques
such as diagonalization and mini model theory (my terminology), and some
of the foundational results.

> My feeling is that the idea embodied in the "usual" construction was
> just floating around as a rather obvious way to persuade those readers
> who don't like the more formal proofs that textbooks tended to use.
> This may be completely wrong, but since you were around at the time,
> maybe you can shed some light on it.

I think he used whatever proof amused him at the moment, at least for
live people interactions. I think that as soon as Cantor's diagonal
proof was circulated, there was an instant recognition in the community
that this was a technique that could turn some god awful hard stuff into
something a lot more people could grasp. Of course I wasn't around in
the Cantor days but I think he thoroughly changed first guesses at how
to prove things. I think in some ways the introduction of diagonal
proofs was almost as important as defining equal size as 1-1
correspondence. One more thing, I don't think Davis had any love of
"textbook style proofs", rather I think he enjoyed pretty mathematics.

Sorry I rattled on for too long. However, that's how it came out and I
don't have a motivation or time to shorten it. I haven't eaten breakfast
yet and I'm hungry.
--
Jeff Barnett

[Peter]

Why are you ignoring the Davis proof that I referred to?

[olcott]

I have been saying that the halting problem counter-examples have the
same erroneous form as the liar paradox since 2004.

comp.theory Peter Olcott Sep 5, 2004, 11:21:57 AM
[Halting Problem Final Conclusion]
The Liar Paradox can be shown to be nothing more than
a incorrectly formed statement because of its pathological
self-reference. The Halting Problem can only exist because

of this same sort of pathological self-reference.

https://groups.google.com/g/comp.theory/c/RO9Z9eCabeE/m/Ka8-xS2rdEEJ

Flibble agrees that all of the proofs that depend on this pathological
self-reference are incorrect.

[Olcott's theory] Mr Flibble Jul 10, 2021, 12:00:56 PM

I agree with Olcott that a halt decider can NOT be part of that which
is being decided (see [Strachey 1965]) which, if Olcott is correct,
falsifies a collection of proofs (which I don't have the time to
examine) which rely on that mistake.

https://groups.google.com/g/comp.theory/c/6cEnndkkrKA/m/gRj0x9KOBgAJ

The incompleteness Theorem merely hides its pathological self-reference
behind the enormous complexity of Gödel numbering. When we recreate this
same proof in HOL without Gödel numbering, then we can see its
pathological self-reference error.

Because Kleene's T predicate uses the same Gödel numbering it is
reasonable to assume that it may have the same hidden pathological
self-reference error as the Gödel proof.
https://en.wikipedia.org/wiki/Kleene%27s_T_predicate

[Peter]

And I gave you a reference that your are choosing to ignore...

>
> comp.theory Peter Olcott  Sep 5, 2004, 11:21:57 AM
> [Halting Problem Final Conclusion]
> The Liar Paradox can be shown to be nothing more than
> a incorrectly formed statement because of its pathological
> self-reference. The Halting Problem can only exist because
> of this same sort of pathological self-reference.
> https://groups.google.com/g/comp.theory/c/RO9Z9eCabeE/m/Ka8-xS2rdEEJ
>
> Flibble agrees that all of the proofs that depend on this pathological
> self-reference are incorrect.
>
> [Olcott's theory] Mr Flibble  Jul 10, 2021, 12:00:56 PM
> I agree with Olcott that a halt decider can NOT be part of that which
> is being decided (see [Strachey 1965]) which, if Olcott is correct,
> falsifies a collection of proofs (which I don't have the time to
> examine) which rely on that mistake.
> https://groups.google.com/g/comp.theory/c/6cEnndkkrKA/m/gRj0x9KOBgAJ
>
> The incompleteness Theorem merely hides its pathological self-reference
> behind the enormous complexity of Gödel numbering. When we recreate this
> same proof in HOL without Gödel numbering, then we can see its
> pathological self-reference error.
>
> Because Kleene's T predicate uses the same Gödel numbering it is
> reasonable to assume that it may have the same hidden pathological
> self-reference error as the Gödel proof.
> https://en.wikipedia.org/wiki/Kleene%27s_T_predicate
>


--

[Chris M. Thomasson]

have you ever of embarrassingly parallel?

[Chris M. Thomasson]

Here is an example of an embarrassingly parallel computation:

https://www.shadertoy.com/view/MdcyRs

[olcott]

My book shelf is not all knowing.

If you can't provide a link then it should be your assumption that the
material is not available.

[wij]

It looks to me embarrassingly parallel is a new term for modern CPU/GPU.
If not particularly designed, they are still deterministic devices.
In fixed condition, the result of flipping a coin is always the same (if not too picky),
the same with CPU/GPU.
Your problem does not fit the computation problem, because on real computers
there are many input from outside the computer.

[Richard Damon]

On 7/10/21 12:00 PM, Mr Flibble wrote:
> I agree with Olcott that a halt decider can NOT be part of that which
> is being decided (see [Strachey 1965]) which, if Olcott is correct,
> falsifies a collection of proofs (which I don't have the time to
> examine) which rely on that mistake. The mistake Olcott seems to be
> making is inferring that just because those proofs are invalid then that
> somehow means that the halting problem itself is not undecidable.
>

> /Flibble
>

I believe you misunderstand that statement.

By definition, in Computation Theory all deciders are Turing Machines,
or there is a Turing Machine that is the computational equivalent of it
(Since we haven't invented a 'higher' form of computation that isn't
better than Turing Equivalent).

Since the decider is a Turing Machine, we can always make another Turing
Machine that has it as a part of it.

What he is saying is that IF the allowable set of inputs this machine
needs to decide on can include inputs that are built in this manner,
than the decision problem that decider is supposed to be able to decide
on can't be universally decided, and there will always be some input
that a given decider won't get right, which also means that there are
some inputs that we can't prove the right answer for.

The Halting Problem is just one example of this sort of problem.

He isn't saying that you can't build that input, but that if you can
then that is enough to prove that the problem can't be universally
decided, some inputs will be unprovable as to their answer to the problem.

[Malcolm McLean]

On Monday, 12 July 2021 at 00:52:54 UTC+1, wij wrote:
>
> It looks to me embarrassingly parallel is a new term for modern CPU/GPU.
>

It just means a problem where you have to compute many independent functions,
so it's very easy to parallelise. That includes most graphics programming where
you either have a function per pixel, or you have a lot of scene elements that
don't need results from other scene elements to process (e.g. transforming 3D
meshes from world space to camera space).

[Peter]

Cranks (for, crank you are) often confuse 'I don't understand X' with 'X
is erroneous'.

>>>
>>> When we ask what Boolean value can a halt decider return to an input
>>> that changes its behavior to contradict this value we cannot answer
>>> this question because it is an incorrect type mismatch error
>>> question. The answer is restricted to {true, false} thus excluding
>>> the correct answer of “neither” making the question itself incorrect.
>>> The TM / input pairs that “prove” the halting problem is undecidable
>>> have the same pathological self-reference(Olcott 2004) error as the
>>> self-contradictory liar paradox.
>>>
>>> To eliminate this pathological feedback loop error we examine the
>>> behavior of the input with a pure simulator that has no effect
>>> what-so-ever on the behavior of the input. As correct science
>>> requires the dependent variable (the halt status decision) must only
>>> have the independent variable (the behavior of the input) and be
>>> isolated from all other influences. Only when we do it this way do we
>>> get the correct halt status decision for the input.
>>>
>>> Until the behavior of its input proves that it will never halt every
>>> H remains a pure simulator of this input. This single fact by itself
>>> proves that the behavior of H has no effect what-so-ever on its halt
>>> status decision. When H stops simulating its input the execution of
>>> the input has been suspended, this does not count as halting.
>>>
>>
>> Why are you ignoring the Davis proof that I referred to?
>>
>
> My book shelf is not all knowing.
>
> If you can't provide a link

I provided a reference. Why don't you grow up?

> then it should be your assumption that the
> material is not available.
>
>


--

[Andy Walker]

On 10/07/2021 19:06, olcott wrote:
> At most I have only proved that the conventional proofs of the
> undecidability of the halting problem that rely on the Strachey form,
> are incorrect. This seems to include all textbook proofs.

As you know, Linz gives a quite different proof; and there are
several other proofs, inc one via "Busy Beaver" [see below].

[...]

> Goldbach's Conjecture is merely undecided and thus not undecidable.

"Thus" is a step too far. But note the reference to Goldbach
in the Wiki article on "Busy Beaver".

[...]

> Busy Beaver only seems intractable not undecidable.

It's undecidable whether an arbitrary TM is a BB; and the
BB function [ie, the "score" of a BB of given size] is uncomputable.
That's a stronger result than intractability. The proof that the
BB function is uncomputable is [reasonably] elementary, and does not
rely on the HP [or recursion]. If you had a "halting decider", then
you could find BBs by exhaustive [albeit intractable!] search and
thus compute the BB function; so there's yet another HP proof.

--
Andy Walker, Nottingham.
Andy's music pages: www.cuboid.me.uk/andy/Music
Composer of the day: www.cuboid.me.uk/andy/Music/Composers/Ascher

[Malcolm McLean]

On Monday, 12 July 2021 at 14:13:15 UTC+1, Andy Walker wrote:
> On 10/07/2021 19:06, olcott wrote:
> > At most I have only proved that the conventional proofs of the
> > undecidability of the halting problem that rely on the Strachey form,
> > are incorrect. This seems to include all textbook proofs.
> As you know, Linz gives a quite different proof; and there are
> several other proofs, inc one via "Busy Beaver" [see below].
>
> [...]
> > Goldbach's Conjecture is merely undecided and thus not undecidable.
> "Thus" is a step too far. But note the reference to Goldbach
> in the Wiki article on "Busy Beaver".
>
> [...]
> > Busy Beaver only seems intractable not undecidable.
> It's undecidable whether an arbitrary TM is a BB; and the
> BB function [ie, the "score" of a BB of given size] is uncomputable.
> That's a stronger result than intractability. The proof that the
> BB function is uncomputable is [reasonably] elementary, and does not
> rely on the HP [or recursion]. If you had a "halting decider", then
> you could find BBs by exhaustive [albeit intractable!] search and
> thus compute the BB function; so there's yet another HP proof.
>

If you have a busy beaver function and a simulating decider, the busy
beaver function tells you how many times you need to step the decider
before you can be certain it will never halt. So halting is decideable if
busy beaver is decideable.

[olcott]

Find a proof of Gödel that used HOL instead of Gödel numbering and you
will see what I mean. Ignore this request and you have not done your due
diligence.

>>>>
>>>> When we ask what Boolean value can a halt decider return to an input
>>>> that changes its behavior to contradict this value we cannot answer
>>>> this question because it is an incorrect type mismatch error
>>>> question. The answer is restricted to {true, false} thus excluding
>>>> the correct answer of “neither” making the question itself
>>>> incorrect. The TM / input pairs that “prove” the halting problem is
>>>> undecidable have the same pathological self-reference(Olcott 2004)
>>>> error as the self-contradictory liar paradox.
>>>>
>>>> To eliminate this pathological feedback loop error we examine the
>>>> behavior of the input with a pure simulator that has no effect
>>>> what-so-ever on the behavior of the input. As correct science
>>>> requires the dependent variable (the halt status decision) must only
>>>> have the independent variable (the behavior of the input) and be
>>>> isolated from all other influences. Only when we do it this way do
>>>> we get the correct halt status decision for the input.
>>>>
>>>> Until the behavior of its input proves that it will never halt every
>>>> H remains a pure simulator of this input. This single fact by itself
>>>> proves that the behavior of H has no effect what-so-ever on its halt
>>>> status decision. When H stops simulating its input the execution of
>>>> the input has been suspended, this does not count as halting.
>>>>
>>>
>>> Why are you ignoring the Davis proof that I referred to?
>>>
>>
>> My book shelf is not all knowing.
>>
>> If you can't provide a link
>
> I provided a reference.  Why don't you grow up?

You expected me to have that book on my book shelf, that is an
unreasonable expectation. I did eventually find a copy and the halting
problem proof on page 70 did not seem to use Kleene.

>
>> then it should be your assumption that the material is not available.
>>
>>
>
>


--

[olcott]

Flibble understands this:
What correct Boolean value can a TM return to an input that does the
opposite of whatever it decides? : neither, is excluded from the
solution set thus making the question itself incorrect.

What time is it (yes or no)? hours and minutes are excluded from the
solution set making the quesition itself incorrect.

[olcott]

On 7/12/2021 8:13 AM, Andy Walker wrote:
> On 10/07/2021 19:06, olcott wrote:
>> At most I have only proved that the conventional proofs of the
>> undecidability of the halting problem that rely on the Strachey form,
>> are incorrect. This seems to include all textbook proofs.
>
>     As you know, Linz gives a quite different proof;  and there are
> several other proofs, inc one via "Busy Beaver" [see below].
>
> [...]
>> Goldbach's Conjecture is merely undecided and thus not undecidable.
>
>     "Thus" is a step too far.  But note the reference to Goldbach
> in the Wiki article on "Busy Beaver".
>
> [...]
>> Busy Beaver only seems intractable not undecidable.
>
>     It's undecidable whether an arbitrary TM is a BB;  and the
> BB function [ie, the "score" of a BB of given size] is uncomputable.
> That's a stronger result than intractability.  The proof that the
> BB function is uncomputable is [reasonably] elementary, and does not
> rely on the HP [or recursion].  If you had a "halting decider", then
> you could find BBs by exhaustive [albeit intractable!] search and
> thus compute the BB function;  so there's yet another HP proof.
>

Flibble understands this:
What correct Boolean value can a TM return to an input that does the
opposite of whatever it decides? : neither, is excluded from the
solution set thus making the question itself incorrect.

What time is it (yes or no)? hours and minutes are excluded from the

solution set making the question itself incorrect.

[olcott]

[Peter]

I expected no such thing! (My guess is that the most sophisticated
stuff on your bookshelves are Dr Suess's works.) You claimed that the
only proofs of the unsolvability of the halting problem use what one may
call the Strachey strategy. I disproved your claim.

> , that is an
> unreasonable expectation.  I did eventually find a copy and the halting
> problem proof on page 70 did not seem to use Kleene.

Report back when you've _read_ it.

>
>>
>>> then it should be your assumption that the material is not available.
>>>
>>>
>>
>>
>
>


--

[olcott]

I found it on page 70 and it does not say what you said that it says.

>
>>
>>>
>>>> then it should be your assumption that the material is not available.
>>>>
>>>>
>>>
>>>
>>
>>
>
>


--

[David Brown]

You still don't understand this "proof by contradiction" concept, do you?

It is not the /question/ that is incorrect, it is the assumption that
such a TM exists that is incorrect.

[Jeff Barnett]

I'm pretty sure that isn't correct. It is true that for a decider that
relies completely on simulation. However, consider a vaguely similar
problem, determining time complexity of an algorithm. You don't do that
by simulation; rather you do an analytic analysis (sometimes placing and
proving invariant properties and complexity of simple language forms).
Similarly if you, as a computer scientist or mathematician, were to do a
halting analysis/proof for an algorithm you wouldn't pick up a pencil
and do a simulation.

You would find something provable about the algorithm as in this typical
example: the counter N has a finite nonnegative initial value; when
label L is reached, the program halts if N is zero; all paths from label
L when N is positive return to label L in finite time and N is reduced
in value but never negative; QED. Note that simulation is no part of
such an approach.

The problem with this approach is that you might not be able to show
that an L to L path is finite. Even using the semantic rules of the
program language used to code the algorithm to help, you may need to
solve members of a class of problems that are undecidable, e.g., solving
Diophantine equations as part of the proof. The good news with the
approach is that you might, with a single proof, prove halting for the
entire domain or be able to classify the subdomain where problems exist.

Given what we know about the halting problem (really know, not PO NO)
simulation is fairly useless. First if we want to know if P halts for a
PARTICULAR INPUT, just run the program. Why simulate? You are looking
for a particular result and you will either get luck or you will run out
of patience. Just running it is much faster than simulation so why
simulate? It's more likely that you actually want to know if a function
halts (completes) for all input in its domain. In this case, simulation
doesn't contribute any insight; you must do some sort of structural
analysis. Period.
--
Jeff Barnett

[Mike Terry]

It looks right, but you might be misunderstanding the point being made.

The claim is:

IF we had a BB function [meaning if BB function were computable]
THEN that would imply Halting is decidable, by virtue of constructing
a simple simulating based decider as outlined.

In more detail, the halting decider would:
a) count states s for input TM
b) run BB calculation for s, giving BB(s)
c) simulate input TM for BB(s) steps.
d) if simulation reached a halt state, the input computation
halts, otherwise it is non-halting.

(d) is from the definition of the BB function.

There was also a prior claim concerning BB "decideability", which was
taken as meaning "whether a given TM is in CLASS_BB" is decideable. A
TM in CLASS_BB is one that halts in the maximum number of steps possible
for a TM with that number of states. The claim there was:

IF CLASS_BB is decideable
THEN the BB FUNCTION (of the previous claim) would be computable

The logic for a TM computing BB function would be:
a) given input number s ...
b) enumerate the finite set of TM's with s states
c) test each one to see if it is in CLASS_BB. (At least one must be)
d) simulate that TM and count steps to halt. That is BB(s).

So "CLASS_BB decideable" ==> "BB function is computable" ==> "Halting
is decideable".

But Halting is NOT decideable, therefore we conclude:
a) BB function is NOT computable
b) CLASS_BB is NOT decideable


Mike.

[Mr Flibble]

On Mon, 12 Jul 2021 21:08:02 +0100
Mike Terry <news.dead.p...@darjeeling.plus.com> wrote:

> But Halting is NOT decideable, therefore we conclude:

Assertions made without evidence can be dismissed without evidence
[Hitchens]. Any proof predicated on a misunderstanding of [Strachey
1965] is in error. Which proof are you basing this assertion on?
[Turing 1937]?

/Flibble

[olcott]

We can say that the following expression is undecidable on the basis
that both true and false derive contradictions:
"This sentence is not true." That same sentence is used as the basis of
the Tarski undefinability theorem.

http://www.liarparadox.org/Tarski_247_248.pdf
http://www.liarparadox.org/Tarski_275_276.pdf



Although we have proven that it is undecidable on the basis of proof by
contradiction we are ignoring the key detail that the proof by
contradiction only succeeds because the expression of language is
self-contradictory, thus not a truth bearer and therefore erroneous.

>
> It is not the /question/ that is incorrect, it is the assumption that
> such a TM exists that is incorrect.
>
>
>> What time is it (yes or no)? hours and minutes are excluded from the
>> solution set making the question itself incorrect.
>>
>
>

[olcott]

On 7/12/2021 3:24 PM, Mr Flibble wrote:
> On Mon, 12 Jul 2021 21:08:02 +0100
> Mike Terry <news.dead.p...@darjeeling.plus.com> wrote:
>
>> But Halting is NOT decideable, therefore we conclude:
>
> Assertions made without evidence can be dismissed without evidence
> [Hitchens].

The ad ignorantiam logic error seems to be the key doctrine of atheism:
https://ses.edu/logical-fallacies-101-ad-ignorantiam/

Assertions made without evidence must be held as undecided until proof
or disproof arises.

> Any proof predicated on a misunderstanding of [Strachey
> 1965] is in error.

You are the only one that understands this.

> Which proof are you basing this assertion on?
> [Turing 1937]?
>
> /Flibble
>

[Andy Walker]

On 12/07/2021 21:08, Mike Terry wrote:
> On 12/07/2021 20:27, Jeff Barnett wrote:
>> On 7/12/2021 7:19 AM, Malcolm McLean wrote:

[I wrote:]

>>>> It's undecidable whether an arbitrary TM is a BB; and the
>>>> BB function [ie, the "score" of a BB of given size] is uncomputable.
>>>> That's a stronger result than intractability. The proof that the
>>>> BB function is uncomputable is [reasonably] elementary, and does not
>>>> rely on the HP [or recursion]. If you had a "halting decider", then
>>>> you could find BBs by exhaustive [albeit intractable!] search and
>>>> thus compute the BB function; so there's yet another HP proof.
>>> If you have a busy beaver function and a simulating decider, the busy
>>> beaver function tells you how many times you need to step the decider
>>> before you can be certain it will never halt. So halting is decideable if
>>> busy beaver is decideable.

Yes [-ish, see below], but more interesting is "HP /un/decidable
if BB /un/computable".

>> I'm pretty sure that isn't correct.

Well, it should be "if the BB function is /computable/", otherwise
it's more-or-less correct. The "less" part is because you need a slightly
different version of BB, but there's no important distinction.

> It looks right, but you might be misunderstanding the point being made.
> The claim is:
>   IF we had a BB function [meaning if BB function were computable]
>   THEN that would imply Halting is decidable, by virtue of constructing
>   a simple simulating based decider as outlined.

> In more detail, [...].

Yes.

> There was also a prior claim concerning BB "decideability", which was
> taken as meaning "whether a given TM is in CLASS_BB" is decideable.
> A TM in CLASS_BB is one that halts in the maximum number of steps

> possible for a TM with that number of states. [...]

> So "CLASS_BB decideable" ==> "BB function is computable" ==>
> "Halting is decideable".

Yes, but more importantly "BB function uncomputable" is known
separately and quite independently of the HP [there are simple proofs,
inc the original one by Rado and one given in the Wiki article on BBs
(which /also/ gives a proof depending on the blank tape HP, equivalent
to the standard HP)], so we deduce that "CLASS BB" is undecidable.

> But Halting is NOT decideable, therefore we conclude:
>   a)  BB function is NOT computable
>   b)  CLASS_BB is NOT decideable

Again, this is more important the other way round. A halt-
decider would be able to to be tweaked [as above] to compute the
BB function. But the BB function is uncomputable; so Halting is
not decidable. This proof is elementary, different from either
Linz proof, and non-recursive.

[Mike Terry]

There are several proofs that halting is not decideable. Take your
pick. The obvious choice given PO's claims over many years would be the
Linz proof, or similar. (The Linz proof is slightly sloppy in its
attention to detail, as it's not aimed at mathematicians, but that's
nothing that can't be routinely patched up.)

Mike.

[olcott]

You don't even seem to understand the vacuous rebuttals that others have
provided.

> First if we want to know if P halts for a
> PARTICULAR INPUT, just run the program. Why simulate?

To be able to directly "see" the behavior of inputs that never halt.
Non-halting behavior patterns can often be recognized.

> You are looking
> for a particular result and you will either get luck or you will run out
> of  patience. Just running it is much faster than simulation so why
> simulate? It's more likely that you actually want to know if a function
> halts (completes) for all input in its domain. In this case, simulation
> doesn't contribute any insight; you must do some sort of structural
> analysis. Period.

If you had some justifiable reason to know that the program halts there
is no need for a halt decider. A halt decider is like an extra
(automated testing) compiler step.

If we had good enough formal specifications that automated proof of
correctness systems could be use as their basis we would not need
programmers, The code could simply be automatically generated from these
specs.

[olcott]

The key question was:

If the conventional proofs have been refuted then what is left to show
that halting is undecidable ?

I said that BB is merely intractable thus by itself not proof that
halting is undecidable.

[olcott]

The key question is whether or not BB proves halting undecidability by
itself within the assumption that the conventional HP proofs have been
correctly refuted.

[olcott]

I refuted Linz as well. When the whole class of all conventional HP
proofs have been refuted, then does the halting problem become
decidability unknown?

[Ben Bacarisse]

Mr Flibble <fli...@reddwarf.jmc> writes:

> On Mon, 12 Jul 2021 21:08:02 +0100
> Mike Terry <news.dead.p...@darjeeling.plus.com> wrote:
>
>> But Halting is NOT decideable, therefore we conclude:
>
> Assertions made without evidence can be dismissed without evidence
> [Hitchens].

I suspect he knew (and appreciated) the irony of his making such an
assertion without any evidence.

> Any proof predicated on a misunderstanding of [Strachey
> 1965] is in error.

I don't think any proper proof is based on such code sketches. PO is
reduced to clumsy sentences and borrowed code sketches, but that's
because he has no access to any other models of computation. And he's
not proving anything either, despite his claims to the contrary.

> Which proof are you basing this assertion on?

I doubt anyone but a novice could answer that. Do I rely on the
argument using register machines, shown to me when I was an
undergraduate? I did when I was a novice. Do I rely on Davis? Linz's
actual proof (rather than the one PO has been confused by) as a
corollary to the proof that there exists a recursively enumerable
languaga that is not recursive is pretty simple. There are least three
others in book at arms length from me right now. I really could not say
I rely on any one of these.

Which do you rely on?

> [Turing 1937]?

As far as I know, Turing never published a proof of the halting theorem.
You can derive one from the results in that seminal paper, but that's
not quite the same thing.

--
Ben.

[Jeff Barnett]

What you say seems correct to me; BB and simulation together implement a
halt decider.

What I was actually trying to say was that simulation has little or no
part in building a (partial) halt decider. I assume without knowing that
you probably agree with that. The best tools for the job are analytic
tools that find plausible arguments or proofs. Recognizing, of course
that no one bundle of tools is going to automate the whole process.

It's interesting that the HP result actually shows that there can't be a
perfect automated proof methodology either. What's so interesting is
that analyzing automatically proving things is often cited as the
original motivation for the invention of the Touring model and some of
the other equivalent formulations.
--
Jeff Barnett

[Ben Bacarisse]

In fairness to Linz, he presents that proof for historical interest. His
"actual" proof comes one page after the last page that PO appears to
have read. It's a corollary of theorem 11.5 from the previous chapter
that establishes that there are recursively enumerable languages that
are not recursive.

--
Ben.

[wij]

Your claim relies on the correctness of HP even though you seem not to know it.
That according GUX https://groups.google.com/g/comp.theory/c/65ZaXe9Sabk HP is undecidable.

> thus making the question itself incorrect.
>
> What time is it (yes or no)? hours and minutes are excluded from the
> solution set making the quesition itself incorrect.

Pathological Logic...

[wij]

That according GUA https://groups.google.com/g/comp.theory/c/65ZaXe9Sabk HP is undecidable.

[olcott]

On 7/12/2021 5:40 PM, Ben Bacarisse wrote:
> Mr Flibble <fli...@reddwarf.jmc> writes:
>
>> On Mon, 12 Jul 2021 21:08:02 +0100
>> Mike Terry <news.dead.p...@darjeeling.plus.com> wrote:
>>
>>> But Halting is NOT decideable, therefore we conclude:
>>
>> Assertions made without evidence can be dismissed without evidence
>> [Hitchens].
>
> I suspect he knew (and appreciated) the irony of his making such an
> assertion without any evidence.
>
>> Any proof predicated on a misunderstanding of [Strachey
>> 1965] is in error.
>
> I don't think any proper proof is based on such code sketches. PO is
> reduced to clumsy sentences and borrowed code sketches, but that's
> because he has no access to any other models of computation. And he's
> not proving anything either, despite his claims to the contrary.
>
>> Which proof are you basing this assertion on?
>
> I doubt anyone but a novice could answer that. Do I rely on the
> argument using register machines, shown to me when I was an
> undergraduate? I did when I was a novice. Do I rely on Davis? Linz's
> actual proof (rather than the one PO has been confused by) as a
> corollary to the proof that there exists a recursively enumerable
> languaga that is not recursive is pretty simple. There are least three
> others in book at arms length from me right now. I really could not say
> I rely on any one of these.
>

At first glance its seems that Linz theorem 11.3 might be the same sort
of nonsense as the Tarski undefinability theorem that essentially
"proves" that some expressions of language are true and unprovable.

The Tarski proof is fundamentally anchored in the liar paradox:
http://www.liarparadox.org/Tarski_247_248.pdf

Even after thousands of years people still do not understand that self
contradictory expressions of language do not map to a Boolean value only
because they are erroneous.

the symbol 'Pr' which denotes the class of all provable sentences of the
theory under consideration ...

we can construct a sentence x of the science in question which satisfies
the following condition: it is not true that x ∉ Pr if and only if p
or in equivalent formulation: (1) x ∉ Pr if and only if p
where the symbol 'p' represents the whole sentence x

In other words this: ¬Pr(p) ↔ p was derived from this ¬Tr(p) ↔ p
where Pr means Provable() and Tr means True()

http://www.liarparadox.org/Tarski_275_276.pdf

> Which do you rely on?
>
>> [Turing 1937]?
>
> As far as I know, Turing never published a proof of the halting theorem.
> You can derive one from the results in that seminal paper, but that's
> not quite the same thing.
>


--

[Mike Terry]

Sure, no problem with that...

Mike.

[wij]

On Monday, 12 July 2021 at 22:10:17 UTC+8, olcott wrote:

Your claim relies on the correctness of HP even though you seem not to know it.

That according GUA https://groups.google.com/g/comp.theory/c/65ZaXe9Sabk HP is undecidable.

> thus making the question itself incorrect.
>
> What time is it (yes or no)? hours and minutes are excluded from the
> solution set making the quesition itself incorrect.

--

Copyright 2021 WIJ
If I can see further it is by standing on top of the tower of dwarfs.

[Mike Terry]

Yeah, the halting problem and computing the BB function are equivalent
problems as each reduces easily to the other. I've seen direct proofs
of BB being uncomputable, but don't instantly recall them, but I recall
them being quite straight forward. But somehow I think getting PO to
understand this and getting him to accept the consequences is not going
to happen. Even understanding that refuting one proof doesn't mean he
has refuted the HP result seems too subtle for PO.


Mike.

[wij]

On Sunday, 11 July 2021 at 17:34:53 UTC+8, Ben Bacarisse wrote:
> wij <wyn...@gmail.com> writes:
>
> > On Sunday, 11 July 2021 at 10:34:36 UTC+8, Ben Bacarisse wrote:
> >> wij <wyn...@gmail.com> writes:
> >>
> >> > I have composed an axiom that clarifies the issue. I am convinced no one
> >> > have ever said the same thing as General Undecidable Axioms says:
> >> > +----------------------------------------------------------------------------------+
> >> > | No TM U can decide the property of a TM P if that property can be defied by TM P. |
> >> > +----------------------------------------------------------------------------------+
> >> I'm also pretty sure no one has ever said that. What does it mean? In
> >> particular, what is a property of P that "can be defined by TM P"? May
> >> this is your way of stating Rice's Theorem?
> >>
> >> --
> >> Ben.
> It's best not to quote sigs.
> > Examples are provided in
> > https://groups.google.com/g/comp.theory/c/65ZaXe9Sabk
> > It is an axiom, intuitive enough, proof is not really necessary.
> I was asking for an explanation of the words, but if you'd rather not
> explain it here, I'm quite happy with that.
>
> --
> Ben.

Explanation is useless as you already see it. People just trims it in various
ways to their like (or dislike). Thanks to his tireless efforts, olcott has
successfully refuted all GUA like sub-proofs for me.

https://groups.google.com/g/comp.theory/c/65ZaXe9Sabk

[olcott]

This would seem to mean that as long as the class of conventional HP
proofs have been refuted that this same refutation could be transformed
to refute BB.

> I've seen direct proofs
> of BB being uncomputable, but don't instantly recall them, but I recall
> them being quite straight forward.  But somehow I think getting PO to
> understand this and getting him to accept the consequences is not going
> to happen.  Even understanding that refuting one proof doesn't mean he
> has refuted the HP result seems too subtle for PO.

When every "input does the opposite of whatever the halt decider
decides" proof has been refuted this includes all of the conventional
proofs.

Now we construct a new Turing machine D with H as a subroutine. This new
TM calls H to determine what M does when the input to M is its own
description (M). Once D has determined this information, it does the
opposite. http://www.liarparadox.org/sipser_165.pdf

>
>
> Mike.

[olcott]

The conventional HP proofs *only* show that they specify infinitely
nested simulation when their counter-examples are simulated.

[olcott]

Ultimately the HP is would only otherwise be undecidable for the exactly
same reason that the liar paradox is not true.

It has been 2000 years and the best minds in the world have still not
figured out that self-contradictory sentences are not true.
Tarski thinks that the liar paradox is true and unprovable.

"This sentence is not true" is not true and that does not make it true.

>> thus making the question itself incorrect.
>>
>> What time is it (yes or no)? hours and minutes are excluded from the
>> solution set making the quesition itself incorrect.
>
> Pathological Logic...
>

[wij]

So you admit that such a problem is undecidable.

General Undecidable Axiom.

[Richard Damon]

Does P(I) Halt IS a Truth Bearing Sentence, as P(I) will either Halt or
it won't. We may not be able to prove that answer, but that is one
fundamental property of the Higher level Logic that includes mathematics.

If you want to keep to the concept that something is only true if you
can prove it, then you must restrict yourself to only First Order Logic,
or you WILL eventually run into an inconsistency in your logic system.

Yes, if you make that restriction to your logic, you can use that
property, but you can not express the fullness of mathematics in your logic.

This is well established.

[Richard Damon]

On 7/12/21 4:23 PM, olcott wrote:
> On 7/12/2021 4:59 PM, Mike Terry wrote:
>> On 12/07/2021 21:24, Mr Flibble wrote:
>>> On Mon, 12 Jul 2021 21:08:02 +0100
>>> Mike Terry <news.dead.p...@darjeeling.plus.com> wrote:
>>>
>>>> But Halting is NOT decideable, therefore we conclude:
>>>
>>> Assertions made without evidence can be dismissed without evidence
>>> [Hitchens].  Any proof predicated on a misunderstanding of [Strachey
>>> 1965] is in error.  Which proof are you basing this assertion on?
>>> [Turing 1937]?
>>>
>>> /Flibble
>>>
>>
>> There are several proofs that halting is not decideable.  Take your
>> pick.  The obvious choice given PO's claims over many years would be
>> the Linz proof, or similar.  (The Linz proof is slightly sloppy in its
>> attention to detail, as it's not aimed at mathematicians, but that's
>> nothing that can't be routinely patched up.)
>>
>> Mike.
>
> I refuted Linz as well. When the whole class of all conventional HP
> proofs have been refuted, then does the halting problem become
> decidability unknown?
>

You have NOT refuted Linz as your claimed correct answer is not correct.
Since it is shown tha tH^(H^) when run as an independent machine does
reach its final HALT state, and thus it IS a Halting Turing Machine by
definition. Even YOU have admitted that H^(H^) will come to this Halt
and have provided traces that prove it.

You just want to change the definition so you can work on POOP.

[olcott]

When we ask what Boolean value can a halt decider return to an input
that changes its behavior to contradict this value we cannot answer this
question because it is an incorrect type mismatch error question.

The answer is restricted to {true, false} thus excluding the correct
answer of “neither” making the question itself incorrect.

The TM / input pairs that “prove” the halting problem is undecidable
have the same pathological self-reference(Olcott 2004) error as the
self-contradictory liar paradox.

[Andy Walker]

On 12/07/2021 23:21, olcott wrote:
> The key question is whether or not BB proves halting undecidability
> by itself within the assumption that the conventional HP proofs have
> been correctly refuted.

That much is trivial. It's just the contrapositive of the
result [given in more detail by MikeT a few posts back] that if we
have a halt decider then the BB function is computable.

--
Andy Walker, Nottingham.
Andy's music pages: www.cuboid.me.uk/andy/Music

Composer of the day: www.cuboid.me.uk/andy/Music/Composers/Dandrieu

[wij]

Nop, H is a total function, every input is valid.

> The answer is restricted to {true, false} thus excluding the correct
> answer of “neither” making the question itself incorrect.

The answer is restricted to {true,false} because it is fundamental of All functions.
So, computation theory needs only address decision functions.
The answer set can be extended to {true,false,neither}, but the result is the same
... "undecidable".

> The TM / input pairs that “prove” the halting problem is undecidable
> have the same pathological self-reference(Olcott 2004) error as the
> self-contradictory liar paradox.

HP is computational problem, liar paradox is not.
You need to DEFINE your pathological error to computational problem form.

[Richard Damon]

Again, you have the wrong question. The question is will P(I) come to a
halt or not in a finite number of steps.

ALL machines will either Halt or they will not, 'neither' is not a
possible answer.

The is a possibility of I don't know, because there do exist some
machines that we can not prove if they halt or not, but that is a
knowledge limit, not a limit on the answer, for those machines the
answer is STILL, one of Halting or Non-Halting.

The fact that when you ask this other question to design H, you get the
'neither' conclusion is proof that you can not make the
Turing Machine you are trying to make.

Note, we can't ask that actual Halting Question until we actually have
fixed the machine, and since the TEMPLATE ^ depends on the Halting
decider, until we actually design that decider, we can't ask about its
behavior.

You question, What should H return for H^(H^) is a question in the
design process for H, as once H is fully designed, that question doesn't
make sense because H's answer will be what it is designed to do. The
paradox you run into isn't a problem with the actual Halting Problem but
just shows that we can't make a machine that will correctly answer a
machine built from it by this template, which proves that the Halting
Problem is not universally decidable.

Perhaps you problem is that your mind just can;t keep these details in
order, as you argument actually just confirms the theory you are trying
to disprove.

[olcott]

Yes and in the same way for the same reason the question:
What time is it? is also undecidable.

When we ask what Boolean value can a halt decider return to an input
that changes its behavior to contradict this value we cannot answer this
question because it is an incorrect type mismatch error question.

The answer is restricted to {true, false} thus excluding the correct
answer of “neither” making the question itself incorrect.

The TM / input pairs that “prove” the halting problem is undecidable
have the same pathological self-reference(Olcott 2004) error as the
self-contradictory liar paradox.

The way that I handled the HP my partial halt decider aborts its input
before ever returning any value. This is essentially the same thing as
returning the correct value of "neither" thus bypassing the type
mismatch error.

[olcott]

It is the exactly model of the Sipser proof which was modeled after the
liar paradox.

What time is is (yes or no)? is undecidable for the same reason.

[olcott]

On 7/13/2021 5:49 AM, Andy Walker wrote:
> On 12/07/2021 23:21, olcott wrote:
>> The key question is whether or not BB proves halting undecidability
>> by itself within the assumption that the conventional HP proofs have
>> been correctly refuted.
>
>     That much is trivial.  It's just the contrapositive of the
> result [given in more detail by MikeT a few posts back] that if we
> have a halt decider then the BB function is computable.
>

Great! This might seem to indicate that at the point in time when it is
accepted that I have correctly refuted the conventional Halting Problem
proofs then the halting problem is transformed from undecidable to
decidability unknown.

[olcott]

If this is true then the question:
What time is it (yes or no)? is valid.
Because it is very obvious that the above question has a type mismatch
error then every input to a TM that has a type mismatch error is also an
incorrect question.

bool Add(int X, int Y); // Is 2 + 3 true or false?

>> The answer is restricted to {true, false} thus excluding the correct
>> answer of “neither” making the question itself incorrect.
>
> The answer is restricted to {true,false} because it is fundamental of All functions.
> So, computation theory needs only address decision functions.
> The answer set can be extended to {true,false,neither}, but the result is the same
> ... "undecidable".
>

Just like the above function has no correct return value because of a
type mismatch error any input having behavior that contradict the
decision of the halt decider is also incorrect.

It is the pathological self-reference(Olcott 2004) error that Flibble
agreed to as erroneous.

On 7/10/2021 12:00 PM, Mr Flibble wrote:
> I agree with Olcott that a halt decider can NOT be part of that which
> is being decided (see [Strachey 1965]) which, if Olcott is correct,
> falsifies a collection of proofs (which I don't have the time to
> examine) which rely on that mistake.

>> The TM / input pairs that “prove” the halting problem is undecidable
>> have the same pathological self-reference(Olcott 2004) error as the
>> self-contradictory liar paradox.
>
> HP is computational problem, liar paradox is not.
> You need to DEFINE your pathological error to computational problem form.
>

// Must return the actual sum as a Boolean
bool Add(int X, int Y)
{
return (bool)(X + Y);
};

int main()
{
Add(2,3);

}


> --
> Copyright 2021 WIJ
> "If I can see further it is by standing on top of the tower of dwarfs."
>

[wij]

Is "What time is it?" a computational problem?

> When we ask what Boolean value can a halt decider return to an input
> that changes its behavior to contradict this value we cannot answer this
> question because it is an incorrect type mismatch error question.

The answer is restricted to {true,false} because it is fundamental of All functions.
So, computation theory needs only address decision functions.
The answer set can be extended to {true,false,neither}, but the result is the same
... "undecidable".

> The answer is restricted to {true, false} thus excluding the correct
> answer of “neither” making the question itself incorrect.
>
> The TM / input pairs that “prove” the halting problem is undecidable
> have the same pathological self-reference(Olcott 2004) error as the
> self-contradictory liar paradox.

HP is computational problem, liar paradox is not.
You need to DEFINE your pathological error to computational problem form.

> The way that I handled the HP my partial halt decider aborts its input
> before ever returning any value. This is essentially the same thing as
> returning the correct value of "neither" thus bypassing the type
> mismatch error.

"neither" might be in the category of "false". Note that by adding "neither"
,the Law of excluded middle is violated, you changed the logic in some way.

[olcott]

That is not the actual question, you leave out the key context that
makes the question incorrect. Ben played this same dishonest dodge since
2006. When you strip off the context of the question you change it into
an entirely different question.

Here is the actual question:

When we ask what Boolean value can a halt decider return to an input
that changes its behavior to contradict this value we cannot answer this
question because it is an incorrect type mismatch error question.

The answer is restricted to {true, false} thus excluding the correct

answer of “neither” making the question itself incorrect.

If we ask a man that has never been married:
Have you stopped beating you wife?
This is an incorrect question.
Every polar question lacking a correct yes/no answer is incorrect.

Every TM/input to a decision problem lacking a correct Boolean return
value is an incorrect TM/input for this decision problem.

The TM / input pairs that “prove” the halting problem is undecidable
have the same pathological self-reference(Olcott 2004) error as the
self-contradictory liar paradox.

It has been at least 2000 years since the liar paradox was discovered
and academicians still do not understand the because self-contradictory
sentences do not map to a Boolean value they are not truth bearers.

> If you want to keep to the concept that something is only true if you
> can prove it, then you must restrict yourself to only First Order Logic,
> or you WILL eventually run into an inconsistency in your logic system.
>

Not at all. Not in the least.
When Gödel's 1931 incompleteness theorem is translated into HOL that has
its own provability predicate thus no need for the purely extraneous
complexity of Gödel numbers then it is very obvious that it is modeled
after the liar paradox.

Gödel himself said that the liar paradox could be used as his
incompleteness basis.

there is also a close relationship with the “liar”
antinomy,14

We are therefore confronted with a proposition which
asserts its own unprovability

14 Every epistemological antinomy can likewise be
used for a similar undecidability proof.

This is HOL with its in provability predicate:
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF

I have examples that show the propositions that assert their own
unprovability are only undecidable because there is an infinite cycle in
their directed graph.

The problem is that like the liar paradox that have a vacuous truth
object. This sentence is not true. This sentence is not provable. Have
no truth object that they are true or provable about.

"It is true that this sentence is a dump truck."
has a truth object thus enabling the sentence to be evaluated as false.

"This sentence is true"
"This sentence is false"
"This sentence is provable"

Have no truth object, thus specify an infinite cycle in the directed
graph of their resolution.

> Yes, if you make that restriction to your logic, you can use that
> property, but you can not express the fullness of mathematics in your logic.
>
> This is well established.
>

I reestablished it correctly this time.