On 2024-02-29 01:24:16 +0000, Andy Walker said:

> On 29/02/2024 00:37, Ben Bacarisse wrote:
>> Alan Mackenzie <acm@muc.de> writes:
>>> If you're going to be going with the contradiction argument that
>>> dominates this group, rather than saying you "construct" a counter
>>> example, say that you "select" it from the set of all programs, as
>>> though it already existed.
>> [...]
>> But I do like the idea when applied to the better "no TM decides
>> halting" proof. We can number all TMs, and then "select" at least one
>> input that TM number 1 get wrong. Then we can select at least one the
>> TM number 2 gets wrong and so on. For every actual TM, there really is
>> one we can find to show that it fails to decide halting.
>
> Is there not a problem in that the "selection" is not computable?
> TM#1 with input [whatever] can do one of four things: fail to halt; halt
> in some state other than "yes"/"no"; halt "yes"; or halt "no". But we
> don't [and cannot] know in general which of these applies. So we can't
> "really find" one it gets wrong, only show that one exists. I don't see
> that this is any easier for the student than "If you claim that TM is a
> halt decider, then here is a construction that shows your claim is false".

We can select it because it contains a particular algorithm to copy the
input, an exact copy of H, a trivial loop appended to every "yes"-
state of the copy of H, and nothing else. Just a simple comparison.

--
Mikko

On 29/02/2024 02:32, Mike Terry wrote:
> On 29/02/2024 01:24, Andy Walker wrote:
>> On 29/02/2024 00:37, Ben Bacarisse wrote:
>>> Alan Mackenzie <acm@muc.de> writes:
>>>> If you're going to be going with the contradiction argument that
>>>> dominates this group, rather than saying you "construct" a counter
>>>> example, say that you "select" it from the set of all programs, as
>>>> though it already existed.
>>> [...]
>>> But I do like the idea when applied to the better "no TM decides
>>> halting" proof.  We can number all TMs, and then "select" at least one
>>> input that TM number 1 get wrong.  Then we can select at least one the
>>> TM number 2 gets wrong and so on.  For every actual TM, there really is
>>> one we can find to show that it fails to decide halting.
>>      Is there not a problem in that the "selection" is not computable?
> If the numbering is directly tied to the TM representation, then the
> mapping from TM number to "counterexample input" is computable - it
> is just what Linz describes in his procedure to create H^ from H.
> The proof that H does indeed get the <H^><H^> input wrong is also the
> proof from Linz.

Yes, but if we don't know whether TM#1 always halts, then we don't
know what it does with <TM#1^><TM#1^>. If TM#1 is running, and we don't
know whether it is about to halt, then it hasn't exactly [yet] got this
case wrong [yet]. So the really, truly, deeply, "here is an input that
TM#1 gets wrong" hasn't [yet] been found. ...

[...]
> The student still needs to accept a proof along the lines:
> a)  one of situations 1,2,3 or 4 will always apply
>     [corresponding to possible H behaviour/ HD failure modes]
> b)  -  if situation 1 applies, TM#n isn't a HD
>     -  if situation 2 applies, TM#n isn't a HD
>     -  if situation 3 applies, TM#n isn't a HD
>     -  if situation 4 applies, TM#n isn't a HD
> c)  therefore TM#n isn't a HD.

... Yes, but we're still only part-way there. We now need to
add that we can do this for TM#1, TM#2, ..., TM#123456, ... and so for
all TMs. You, Ben, Alan and I, amongst others, find this convincing.
But Ben was asking about the best proof for students who find other
proofs too abstract. I don't see that this proof is any better for
such students. We have three proposed Linz-style proofs:

-- If H is a HD, then look at H^, ..., contradiction.
-- For all TMs, ... [your proof].
-- If TM is claimed to be a HD, then ... [your step (b)].

I think the third of those is [slightly] less difficult than the other
two, but I'm open to persuasion.

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

On 29/02/24 01:03, olcott wrote:

> H.q0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qy   // H applied to ⟨Ĥ⟩ ⟨Ĥ⟩ halts
> H.q0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qn   // H applied to ⟨Ĥ⟩ ⟨Ĥ⟩ does not halt
>
> Because H is required to always halt we can know that
> Ĥ.Hq0 applied to ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to Ĥ.Hqy or Ĥ.Hqn
> thus H merely needs to report on that.
>
> // Ĥ.q0 ⟨Ĥ⟩ copies its input then transitions to Ĥ.Hq0
> // Ĥ.Hq0 is the first state of The Linz hypothetical halt decider
> // H transitions to Ĥ.Hqy for halts and Ĥ.Hqn for does not halt
> // ∞ means an infinite loop has been appended to the Ĥ.Hqy state
> //
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy  ∞ // Ĥ applied to ⟨Ĥ⟩ halts
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn    // Ĥ applied to ⟨Ĥ⟩ does not halt
>
> When Ĥ is applied to ⟨Ĥ⟩ it contradicts whatever value that Ĥ.H
> returns making Ĥ self-contradictory.
>

was there a purpose to posting this nonsense again? You might be
automatically spam-filtered if you keep posting the same post so many times.

On 29/02/24 01:58, No one knows wrote:
> On 2/28/2024 6:37 PM, Ben Bacarisse wrote:
>> But I do like the idea when applied to the better "no TM decides
>> halting" proof.  We can number all TMs, and then "select" at least one
>> input that TM number 1 get wrong.  Then we can select at least one the
>> TM number 2 gets wrong and so on.  For every actual TM, there really is
>> one we can find to show that it fails to decide halting.
>>
>
> That proof seems to no longer work, yet the alternative
> one that you referenced may now be relevant.
>
> When we look at the actual Linz proof
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn   // Ĥ applied to ⟨Ĥ⟩ does not halt
>
> H ⟨Ĥ⟩ ⟨Ĥ⟩ can see that Ĥ.H transitions to Ĥ.Hqn on the basis
> that Ĥ.H sees that Ĥ.Hqy is the wrong answer.

Through Giganews! Well, that establishes that Olcott pays for piracy,
since we all know that's what Giganews is for.

Why don't you write down a TM that you think always gets halting right,
and I will show you a TM that it gets wrong.

On 29/02/24 02:24, Andy Walker wrote:
> On 29/02/2024 00:37, Ben Bacarisse wrote:
>> Alan Mackenzie <acm@muc.de> writes:
>>> If you're going to be going with the contradiction argument that
>>> dominates this group, rather than saying you "construct" a counter
>>> example, say that you "select" it from the set of all programs, as
>>> though it already existed.
>> [...]
>> But I do like the idea when applied to the better "no TM decides
>> halting" proof.  We can number all TMs, and then "select" at least one
>> input that TM number 1 get wrong.  Then we can select at least one the
>> TM number 2 gets wrong and so on.  For every actual TM, there really is
>> one we can find to show that it fails to decide halting.
>
>     Is there not a problem in that the "selection" is not computable?
> TM#1 with input [whatever] can do one of four things:  fail to halt; halt
> in some state other than "yes"/"no";  halt "yes";  or halt "no".  But we
> don't [and cannot] know in general which of these applies.  So we can't
> "really find" one it gets wrong, only show that one exists.  I don't see
> that this is any easier for the student than "If you claim that TM is a
> halt decider, then here is a construction that shows your claim is false".
>

The selection is easily computable, by the usual method.

In case you are unaware of the usual proof: If M is the Turing machine
that you think computes halting, select a machine equivalent to:

void f(input) {
if(M(input, input)) {
loop forever
}
}

and then compute M(f,f).

If M(f,f) doesn't halt or halts in a state other than yes/no, it has
already failed to compute halting. If it halts in yes, the correct
answer was no; if it halts in no, the correct answer was yes.

On 29/02/24 02:57, olcott wrote:
> On 2/28/2024 7:24 PM, Andy Walker wrote:
>> On 29/02/2024 00:37, Ben Bacarisse wrote:
>>> Alan Mackenzie <acm@muc.de> writes:
>>>> If you're going to be going with the contradiction argument that
>>>> dominates this group, rather than saying you "construct" a counter
>>>> example, say that you "select" it from the set of all programs, as
>>>> though it already existed.
>>> [...]
>>> But I do like the idea when applied to the better "no TM decides
>>> halting" proof.  We can number all TMs, and then "select" at least one
>>> input that TM number 1 get wrong.  Then we can select at least one the
>>> TM number 2 gets wrong and so on.  For every actual TM, there really is
>>> one we can find to show that it fails to decide halting.
>>
>>      Is there not a problem in that the "selection" is not computable?
>> TM#1 with input [whatever] can do one of four things:  fail to halt; halt
>> in some state other than "yes"/"no";  halt "yes";  or halt "no".  But we
>> don't [and cannot] know in general which of these applies.
>
>> So we can't
>> "really find" one it gets wrong, only show that one exists.
>
> Excellent point. Diagonalization is not very informative.

That's incorrect. Diagonalization in this case is constructive - given
any Turing machine, we can easily find an input which it fails. In some
cases it might be uncomputable to know exactly how it fails (whether it
loops forever or eventually halts in the wrong state) but we know it's
one of those two. In many cases it IS computable to know exactly how it
fails.

Your x86utm H fails because it isn't equivalent to any Turing machine
due to the hidden state which you try to keep secret so we'll think it
is. If converted to a Turing machine without hidden state, it's
computable to know that it loops infinitely.

>
>> I don't see
>> that this is any easier for the student than "If you claim that TM is a
>> halt decider, then here is a construction that shows your claim is
>> false".
>>
>

On 29/02/24 03:42, No one knows wrote:
> On 2/28/2024 8:32 PM, Mike Terry wrote:
>> On 29/02/2024 01:24, Andy Walker wrote:
>>> On 29/02/2024 00:37, Ben Bacarisse wrote:
>>>> Alan Mackenzie <acm@muc.de> writes:
>>>>> If you're going to be going with the contradiction argument that
>>>>> dominates this group, rather than saying you "construct" a counter
>>>>> example, say that you "select" it from the set of all programs, as
>>>>> though it already existed.
>>>> [...]
>>>> But I do like the idea when applied to the better "no TM decides
>>>> halting" proof.  We can number all TMs, and then "select" at least one
>>>> input that TM number 1 get wrong.  Then we can select at least one the
>>>> TM number 2 gets wrong and so on.  For every actual TM, there really is
>>>> one we can find to show that it fails to decide halting.
>>>
>>>      Is there not a problem in that the "selection" is not computable?
>>
>> If the numbering is directly tied to the TM representation, then the
>> mapping from TM number to "counterexample input" is computable - it is
>> just what Linz describes in his procedure to create H^ from H.  The
>> proof that H does indeed get the <H^><H^> input wrong is also the
>> proof from Linz.
>
> *When we look at the actual Linz proof*
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn   // Ĥ applied to ⟨Ĥ⟩ does not halt
>
> H ⟨Ĥ⟩ ⟨Ĥ⟩ can see that Ĥ.H transitions to Ĥ.Hqn on the basis
> that Ĥ.H sees that Ĥ.Hqy is the wrong answer.
>

You did not read what Mike wrote.

On 29/02/2024 10:42, immibis wrote:
[...]
> The selection is easily computable, by the usual method.

H^ is computable from H, but that doesn't solve the pedagogic
problem of avoiding proof-by-contradiction and other abstractions.
Further, it doesn't show an example that TM#1 and TM#2 [given below]
get wrong.

> In case you are unaware of the usual proof:

I first taught it over 50 years ago, and it has been discussed
"ad nauseam" in this group. I think I'm as aware of it as anyone here,
modulo whatever I've forgotten over those years.

> If M is the Turing
> machine that you think computes halting,

"Please, Sir, what if I /don't/ think M computes halting?"

> select a machine equivalent
> to: [...]
> and then compute M(f,f).
> If M(f,f) doesn't halt or halts in a state other than yes/no, it has
> already failed to compute halting.

"Please, Sir, how can we know M(f,f) doesn't halt?"

> If it halts in yes, the correct
> answer was no; if it halts in no, the correct answer was yes.

Yes, and most people here accept that [tidied up a bit] as a
valid proof. But Ben's claim in <87v868ksuy.fsf@bsb.me.uk> was that
there was a selection method that caused TM#n to give the wrong answer
and ISTM that Mike's elaboration of that is at least as abstract as
some other proofs. I don't know whether it's even possible to find a
proof that is acceptable to students who don't understand abstraction
at least as far as proof-by-contradiction [luckily, my audiences have
always been mathematicians or close approximations thereto].

To fix ideas slightly, let us suppose that [using pseudo-code
in place of TMs]

TM#1 is 'L: goto L'
TM#2 is 'print ("Don't know")'
TM#3 is 'print (if {A} then "halts"
elif {B} then "doesn't halt"
else "Don't know")'
where '{A}' and '{B}' are Boolean procedures
TM#4 is 'if {Goldbach_Conjecture} then {...}'
TM#5 is some UTM emulating your 'f'

[Note that TM#3 and TM#5 may actually be quite useful.] What specific
input do these TMs get wrong? How do you know, in a way that would
convince a reasonably bright student who doesn't understand abstraction?
FTAOD, I am not claiming that these are HDs, or that TM#1 and TM#2 get
anything right.
--
Andy Walker, Nottingham.
Andy's music pages: www.cuboid.me.uk/andy/Music
Composer of the day: www.cuboid.me.uk/andy/Music/Composers/Hummel

On 2/29/2024 3:59 AM, Mikko wrote:
> On 2024-02-28 23:52:18 +0000, Alan Mackenzie said:
>
>> Ben Bacarisse <ben.usenet@bsb.me.uk> wrote:
>>> In chapter 12 of "An Introduction to Formal Languages and Automata" Linz
>>> presents the classical proof of the halting theorem only out of
>>> historical interest.  He has, to all intents and purposes, already
>>> proved the theorem in the preceding chapter having proved
>>
>>> 11.3 There exists a recursively enumerable language whose
>>> complement is not recursively enumerable.
>>
>>> 11.4 If a language L and its complement L' are both recursively
>>> enumerable, then both languages are recursive. If L is
>>> recursive, then L' is also recursive, and consequently both are
>>> recursively enumerable.
>>
>>> 11.5 There exists a recursively enumerable languaga that is not
>>> recursive; that is, the family of recursive languages is a proper
>>> subset of the family of recursively enumerable languages.
>>
>>> This is a much stronger result than the halting theorem since the
>>> halting theorem follows directly as a corollary to it.  But it could be
>>> argued that it's a bit of a round about way to do it.
>>
>>> Conversely, the classical proof by contradiction seems to lead a lot of
>>> non-mathematical students astray.  I think they tend to assume that if
>>> you can specify it, you can implement it, and /assuming/ that there is a
>>> program that does something just makes that worse!  This is why I once
>>> tried setting Post's correspondence problem as a background exercise,
>>> just as if it were any other programming problem.
>>
>>> If you were teaching this material, how would you approach the halting
>>> theorem?  Would you give a more intuitive proof or stick with a formal
>>> one?  What model would you use?  I was taught it using Minsky machines,
>>> and that has the advantage (for lectures) that it's very visual with
>>> lots of diagrams.  That's almost impossible to present on Usenet, but
>>> then I'm not suggesting you actually post your favourite proof, only
>>> that you describe it.
>>
>> I may be a bit late on this thread, but I have an idea.
>>
>> If you're going to be going with the contradiction argument that
>> dominates this group, rather than saying you "construct" a counter
>> example, say that you "select" it from the set of all programs, as
>> though it already existed.
>>
>> That might help emphasize that the purported halt decider would have to
>> work with _all_ programs.
>
> Unlikely to work here. In a book it might be a good idea to emphasize
> that every constructible Turing machine exists, including all that are
> not yet constructed. And more generally, every constructible mathematical
> object exists.
>

We simply assume (as always) that it must work with all finite strings.

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

On 2/29/2024 4:11 AM, Mikko wrote:
> On 2024-02-29 01:24:16 +0000, Andy Walker said:
>
>> On 29/02/2024 00:37, Ben Bacarisse wrote:
>>> Alan Mackenzie <acm@muc.de> writes:
>>>> If you're going to be going with the contradiction argument that
>>>> dominates this group, rather than saying you "construct" a counter
>>>> example, say that you "select" it from the set of all programs, as
>>>> though it already existed.
>>> [...]
>>> But I do like the idea when applied to the better "no TM decides
>>> halting" proof.  We can number all TMs, and then "select" at least one
>>> input that TM number 1 get wrong.  Then we can select at least one the
>>> TM number 2 gets wrong and so on.  For every actual TM, there really is
>>> one we can find to show that it fails to decide halting.
>>
>>     Is there not a problem in that the "selection" is not computable?
>> TM#1 with input [whatever] can do one of four things:  fail to halt; halt
>> in some state other than "yes"/"no";  halt "yes";  or halt "no".  But we
>> don't [and cannot] know in general which of these applies.  So we can't
>> "really find" one it gets wrong, only show that one exists.  I don't see
>> that this is any easier for the student than "If you claim that TM is a
>> halt decider, then here is a construction that shows your claim is
>> false".
>
> We can select it because it contains a particular algorithm to copy the
> input, an exact copy of H, a trivial loop appended to every "yes"-
> state of the copy of H, and nothing else. Just a simple comparison.
>

We can specify an infinite set of Turing Machines by the Linz template:
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn // Ĥ applied to ⟨Ĥ⟩ does not halt

We can see that none of these machines can possibly return a Boolean
value corresponding to the actual behavior of Ĥ applied to ⟨Ĥ⟩

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

On 2/28/2024 8:32 PM, Mike Terry wrote:
> On 29/02/2024 01:24, Andy Walker wrote:
>> On 29/02/2024 00:37, Ben Bacarisse wrote:
>>> Alan Mackenzie <acm@muc.de> writes:
>>>> If you're going to be going with the contradiction argument that
>>>> dominates this group, rather than saying you "construct" a counter
>>>> example, say that you "select" it from the set of all programs, as
>>>> though it already existed.
>>> [...]
>>> But I do like the idea when applied to the better "no TM decides
>>> halting" proof.  We can number all TMs, and then "select" at least one
>>> input that TM number 1 get wrong.  Then we can select at least one the
>>> TM number 2 gets wrong and so on.  For every actual TM, there really is
>>> one we can find to show that it fails to decide halting.
>>
>>      Is there not a problem in that the "selection" is not computable?
>
> If the numbering is directly tied to the TM representation, then the
> mapping from TM number to "counterexample input" is computable - it is
> just what Linz describes in his procedure to create H^ from H.  The
> proof that H does indeed get the <H^><H^> input wrong is also the proof
> from Linz.

Linz never applies H to ⟨Ĥ⟩ ⟨Ĥ⟩ he only applies Ĥ to ⟨Ĥ⟩

Now Ĥ is a Turing machine, so that it will have some description in
Σ*, say ⟨Ĥ⟩. This string, in addition to being the description of Ĥ can
also be used as input string. We can therefore legitimately ask what
would happen if Ĥ is applied to ⟨Ĥ⟩.

When Ĥ is applied to ⟨Ĥ⟩
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞
if Ĥ applied to ⟨Ĥ⟩ halts, and

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn
if Ĥ applied to ⟨Ĥ⟩ does not halt.
https://www.liarparadox.org/Linz_Proof.pdf

Linz falsely assumes that Ĥ in a separate memory space can
somehow thwart H in a different memory space. Since we
already know that H transitions to H.qy or H.qn, H merely
needs to simulate ⟨Ĥ⟩ applied to ⟨Ĥ⟩ to see which one it
transitions to.

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

On 2/29/2024 4:27 AM, Andy Walker wrote:
> On 29/02/2024 02:32, Mike Terry wrote:
>> On 29/02/2024 01:24, Andy Walker wrote:
>>> On 29/02/2024 00:37, Ben Bacarisse wrote:
>>>> Alan Mackenzie <acm@muc.de> writes:
>>>>> If you're going to be going with the contradiction argument that
>>>>> dominates this group, rather than saying you "construct" a counter
>>>>> example, say that you "select" it from the set of all programs, as
>>>>> though it already existed.
>>>> [...]
>>>> But I do like the idea when applied to the better "no TM decides
>>>> halting" proof.  We can number all TMs, and then "select" at least one
>>>> input that TM number 1 get wrong.  Then we can select at least one the
>>>> TM number 2 gets wrong and so on.  For every actual TM, there really is
>>>> one we can find to show that it fails to decide halting.
>>>      Is there not a problem in that the "selection" is not computable?
>> If the numbering is directly tied to the TM representation, then the
>> mapping from TM number to "counterexample input" is computable - it
>> is just what Linz describes in his procedure to create H^ from H.
>> The proof that H does indeed get the <H^><H^> input wrong is also the
>> proof from Linz.
>
>     Yes, but if we don't know whether TM#1 always halts, then we don't
> know what it does with <TM#1^><TM#1^>.  If TM#1 is running, and we don't
> know whether it is about to halt, then it hasn't exactly [yet] got this
> case wrong [yet].  So the really, truly, deeply, "here is an input that
> TM#1 gets wrong" hasn't [yet] been found.  ...
>
> [...]
>> The student still needs to accept a proof along the lines:
>> a)  one of situations 1,2,3 or 4 will always apply
>>      [corresponding to possible H behaviour/ HD failure modes]
>> b)  -  if situation 1 applies, TM#n isn't a HD
>>      -  if situation 2 applies, TM#n isn't a HD
>>      -  if situation 3 applies, TM#n isn't a HD
>>      -  if situation 4 applies, TM#n isn't a HD
>> c)  therefore TM#n isn't a HD.
>
>     ... Yes, but we're still only part-way there.  We now need to
> add that we can do this for TM#1, TM#2, ..., TM#123456, ... and so for
> all TMs.  You, Ben, Alan and I, amongst others, find this convincing.
> But Ben was asking about the best proof for students who find other
> proofs too abstract.  I don't see that this proof is any better for
> such students.  We have three proposed Linz-style proofs:
>
>   -- If H is a HD, then look at H^, ..., contradiction.
>   -- For all TMs, ... [your proof].
>   -- If TM is claimed to be a HD, then ... [your step (b)].
>
> I think the third of those is [slightly] less difficult than the other
> two, but I'm open to persuasion.
>

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn // Ĥ applied to ⟨Ĥ⟩ does not halt

H ⟨Ĥ⟩ ⟨Ĥ⟩ (in a separate memory space) merely needs to report on
the actual behavior of Ĥ ⟨Ĥ⟩. We already know that Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ must
transition to Ĥ.Hqy or Ĥ.Hqn, H merely needs to see which one.

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

On 2/29/2024 4:42 AM, immibis wrote:
> On 29/02/24 02:24, Andy Walker wrote:
>> On 29/02/2024 00:37, Ben Bacarisse wrote:
>>> Alan Mackenzie <acm@muc.de> writes:
>>>> If you're going to be going with the contradiction argument that
>>>> dominates this group, rather than saying you "construct" a counter
>>>> example, say that you "select" it from the set of all programs, as
>>>> though it already existed.
>>> [...]
>>> But I do like the idea when applied to the better "no TM decides
>>> halting" proof.  We can number all TMs, and then "select" at least one
>>> input that TM number 1 get wrong.  Then we can select at least one the
>>> TM number 2 gets wrong and so on.  For every actual TM, there really is
>>> one we can find to show that it fails to decide halting.
>>
>>      Is there not a problem in that the "selection" is not computable?
>> TM#1 with input [whatever] can do one of four things:  fail to halt; halt
>> in some state other than "yes"/"no";  halt "yes";  or halt "no".  But we
>> don't [and cannot] know in general which of these applies.  So we can't
>> "really find" one it gets wrong, only show that one exists.  I don't see
>> that this is any easier for the student than "If you claim that TM is a
>> halt decider, then here is a construction that shows your claim is
>> false".
>>
>
> The selection is easily computable, by the usual method.
>
> In case you are unaware of the usual proof: If M is the Turing machine
> that you think computes halting, select a machine equivalent to:
>
>     void f(input) {
>       if(M(input, input)) {
>         loop forever
>       }
>     }
>
> and then compute M(f,f).
>
> If M(f,f) doesn't halt or halts in a state other than yes/no, it has
> already failed to compute halting. If it halts in yes, the correct
> answer was no; if it halts in no, the correct answer was yes.

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn // Ĥ applied to ⟨Ĥ⟩ does not halt

H ⟨Ĥ⟩ ⟨Ĥ⟩ (in a separate memory space) merely needs to report on
the actual behavior of Ĥ ⟨Ĥ⟩. We already know that Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ must
transition to Ĥ.Hqy or Ĥ.Hqn, H merely needs to see which one.

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

On 2/29/2024 7:29 AM, Andy Walker wrote:
> On 29/02/2024 10:42, immibis wrote:
> [...]
>> The selection is easily computable, by the usual method.
>
>     H^ is computable from H, but that doesn't solve the pedagogic
> problem of avoiding proof-by-contradiction and other abstractions.
> Further, it doesn't show an example that TM#1 and TM#2 [given below]
> get wrong.
>
>> In case you are unaware of the usual proof:
>
>     I first taught it over 50 years ago, and it has been discussed
> "ad nauseam" in this group.  I think I'm as aware of it as anyone here,
> modulo whatever I've forgotten over those years.
>
>>                           If M is the Turing
>> machine that you think computes halting,
>
>     "Please, Sir, what if I /don't/ think M computes halting?"
>
>>                        select a machine equivalent
>> to: [...]
>> and then compute M(f,f).
>> If M(f,f) doesn't halt or halts in a state other than yes/no, it has
>> already failed to compute halting.
>
>     "Please, Sir, how can we know M(f,f) doesn't halt?"
>
>>                      If it halts in yes, the correct
>> answer was no; if it halts in no, the correct answer was yes.
>
>     Yes, and most people here accept that [tidied up a bit] as a
> valid proof.  But Ben's claim in <87v868ksuy.fsf@bsb.me.uk> was that
> there was a selection method that caused TM#n to give the wrong answer
> and ISTM that Mike's elaboration of that is at least as abstract as
> some other proofs.  I don't know whether it's even possible to find a
> proof that is acceptable to students who don't understand abstraction
> at least as far as proof-by-contradiction [luckily, my audiences have
> always been mathematicians or close approximations thereto].
>
>     To fix ideas slightly, let us suppose that [using pseudo-code
> in place of TMs]
>
>   TM#1 is 'L: goto L'
>   TM#2 is 'print ("Don't know")'
>   TM#3 is 'print (if {A} then "halts"
>                 elif {B} then "doesn't halt"
>                 else "Don't know")'
>     where '{A}' and '{B}' are Boolean procedures
>   TM#4 is 'if {Goldbach_Conjecture} then {...}'
>   TM#5 is some UTM emulating your 'f'
>
> [Note that TM#3 and TM#5 may actually be quite useful.]  What specific
> input do these TMs get wrong?  How do you know, in a way that would
> convince a reasonably bright student who doesn't understand abstraction?
> FTAOD, I am not claiming that these are HDs, or that TM#1 and TM#2 get
> anything right.

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn // Ĥ applied to ⟨Ĥ⟩ does not halt

H ⟨Ĥ⟩ ⟨Ĥ⟩ (in a separate memory space) merely needs to report on
the actual behavior of Ĥ ⟨Ĥ⟩. We already know that Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ must
transition to Ĥ.Hqy or Ĥ.Hqn, H merely needs to see which one.

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

On 2/29/2024 4:38 AM, immibis wrote:
> On 29/02/24 01:03, olcott wrote:
>
>> H.q0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qy   // H applied to ⟨Ĥ⟩ ⟨Ĥ⟩ halts
>> H.q0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qn   // H applied to ⟨Ĥ⟩ ⟨Ĥ⟩ does not halt
>>
>> Because H is required to always halt we can know that
>> Ĥ.Hq0 applied to ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to Ĥ.Hqy or Ĥ.Hqn
>> thus H merely needs to report on that.
>>
>> // Ĥ.q0 ⟨Ĥ⟩ copies its input then transitions to Ĥ.Hq0
>> // Ĥ.Hq0 is the first state of The Linz hypothetical halt decider
>> // H transitions to Ĥ.Hqy for halts and Ĥ.Hqn for does not halt
>> // ∞ means an infinite loop has been appended to the Ĥ.Hqy state
>> //
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy  ∞ // Ĥ applied to ⟨Ĥ⟩ halts
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn    // Ĥ applied to ⟨Ĥ⟩ does not halt
>>
>> When Ĥ is applied to ⟨Ĥ⟩ it contradicts whatever value that Ĥ.H
>> returns making Ĥ self-contradictory.
>>
>
> was there a purpose to posting this nonsense again? You might be
> automatically spam-filtered if you keep posting the same post so many
> times.

All of the rebuttals have been incorrect.

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

On 2/29/2024 4:45 AM, immibis wrote:
> On 29/02/24 02:57, olcott wrote:
>> On 2/28/2024 7:24 PM, Andy Walker wrote:
>>> On 29/02/2024 00:37, Ben Bacarisse wrote:
>>>> Alan Mackenzie <acm@muc.de> writes:
>>>>> If you're going to be going with the contradiction argument that
>>>>> dominates this group, rather than saying you "construct" a counter
>>>>> example, say that you "select" it from the set of all programs, as
>>>>> though it already existed.
>>>> [...]
>>>> But I do like the idea when applied to the better "no TM decides
>>>> halting" proof.  We can number all TMs, and then "select" at least one
>>>> input that TM number 1 get wrong.  Then we can select at least one the
>>>> TM number 2 gets wrong and so on.  For every actual TM, there really is
>>>> one we can find to show that it fails to decide halting.
>>>
>>>      Is there not a problem in that the "selection" is not computable?
>>> TM#1 with input [whatever] can do one of four things:  fail to halt;
>>> halt
>>> in some state other than "yes"/"no";  halt "yes";  or halt "no".  But we
>>> don't [and cannot] know in general which of these applies.
>>
>>> So we can't
>>> "really find" one it gets wrong, only show that one exists.
>>
>> Excellent point. Diagonalization is not very informative.
>
> That's incorrect. Diagonalization in this case is constructive - given
> any Turing machine, we can easily find an input which it fails. In some
> cases it might be uncomputable to know exactly how it fails (whether it
> loops forever or eventually halts in the wrong state) but we know it's
> one of those two. In many cases it IS computable to know exactly how it
> fails.

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn // Ĥ applied to ⟨Ĥ⟩ does not halt

H ⟨Ĥ⟩ ⟨Ĥ⟩ (in a separate memory space) merely needs to report on
the actual behavior of Ĥ ⟨Ĥ⟩. We already know that Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ must
transition to Ĥ.Hqy or Ĥ.Hqn, H merely needs to see which one.

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

On 29/02/24 16:49, olcott wrote:
> On 2/29/2024 4:38 AM, immibis wrote:
>> On 29/02/24 01:03, olcott wrote:
>>
>>> H.q0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qy   // H applied to ⟨Ĥ⟩ ⟨Ĥ⟩ halts
>>> H.q0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qn   // H applied to ⟨Ĥ⟩ ⟨Ĥ⟩ does not halt
>>>
>>> Because H is required to always halt we can know that
>>> Ĥ.Hq0 applied to ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to Ĥ.Hqy or Ĥ.Hqn
>>> thus H merely needs to report on that.
>>>
>>> // Ĥ.q0 ⟨Ĥ⟩ copies its input then transitions to Ĥ.Hq0
>>> // Ĥ.Hq0 is the first state of The Linz hypothetical halt decider
>>> // H transitions to Ĥ.Hqy for halts and Ĥ.Hqn for does not halt
>>> // ∞ means an infinite loop has been appended to the Ĥ.Hqy state
>>> //
>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy  ∞ // Ĥ applied to ⟨Ĥ⟩ halts
>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn    // Ĥ applied to ⟨Ĥ⟩ does not halt
>>>
>>> When Ĥ is applied to ⟨Ĥ⟩ it contradicts whatever value that Ĥ.H
>>> returns making Ĥ self-contradictory.
>>>
>>
>> was there a purpose to posting this nonsense again? You might be
>> automatically spam-filtered if you keep posting the same post so many
>> times.
>
> All of the rebuttals have been incorrect.
>

Then why don't you explain how each one is incorrect?

On 29/02/24 16:25, olcott wrote:
> On 2/28/2024 8:32 PM, Mike Terry wrote:
>> On 29/02/2024 01:24, Andy Walker wrote:
>>> On 29/02/2024 00:37, Ben Bacarisse wrote:
>>>> Alan Mackenzie <acm@muc.de> writes:
>>>>> If you're going to be going with the contradiction argument that
>>>>> dominates this group, rather than saying you "construct" a counter
>>>>> example, say that you "select" it from the set of all programs, as
>>>>> though it already existed.
>>>> [...]
>>>> But I do like the idea when applied to the better "no TM decides
>>>> halting" proof.  We can number all TMs, and then "select" at least one
>>>> input that TM number 1 get wrong.  Then we can select at least one the
>>>> TM number 2 gets wrong and so on.  For every actual TM, there really is
>>>> one we can find to show that it fails to decide halting.
>>>
>>>      Is there not a problem in that the "selection" is not computable?
>>
>> If the numbering is directly tied to the TM representation, then the
>> mapping from TM number to "counterexample input" is computable - it is
>> just what Linz describes in his procedure to create H^ from H.  The
>> proof that H does indeed get the <H^><H^> input wrong is also the
>> proof from Linz.
>
> Linz never applies H to ⟨Ĥ⟩ ⟨Ĥ⟩ he only applies Ĥ to ⟨Ĥ⟩

One part of applying Ĥ to ⟨Ĥ⟩ is identical to applying H to ⟨Ĥ⟩ ⟨Ĥ⟩.
That it is identical cannot be ignored.

> Linz falsely assumes that Ĥ in a separate memory space can
> somehow thwart H in a different memory space.

There is no thwarting, and memory spaces do not exist in Turing
machines. It is a simple fact that an embedded copy of H always returns
the same result as H does.

On 29/02/24 16:07, olcott wrote:
> On 2/29/2024 4:11 AM, Mikko wrote:
>> On 2024-02-29 01:24:16 +0000, Andy Walker said:
>>
>>> On 29/02/2024 00:37, Ben Bacarisse wrote:
>>>> Alan Mackenzie <acm@muc.de> writes:
>>>>> If you're going to be going with the contradiction argument that
>>>>> dominates this group, rather than saying you "construct" a counter
>>>>> example, say that you "select" it from the set of all programs, as
>>>>> though it already existed.
>>>> [...]
>>>> But I do like the idea when applied to the better "no TM decides
>>>> halting" proof.  We can number all TMs, and then "select" at least one
>>>> input that TM number 1 get wrong.  Then we can select at least one the
>>>> TM number 2 gets wrong and so on.  For every actual TM, there really is
>>>> one we can find to show that it fails to decide halting.
>>>
>>>     Is there not a problem in that the "selection" is not computable?
>>> TM#1 with input [whatever] can do one of four things:  fail to halt;
>>> halt
>>> in some state other than "yes"/"no";  halt "yes";  or halt "no".  But we
>>> don't [and cannot] know in general which of these applies.  So we can't
>>> "really find" one it gets wrong, only show that one exists.  I don't see
>>> that this is any easier for the student than "If you claim that TM is a
>>> halt decider, then here is a construction that shows your claim is
>>> false".
>>
>> We can select it because it contains a particular algorithm to copy the
>> input, an exact copy of H, a trivial loop appended to every "yes"-
>> state of the copy of H, and nothing else. Just a simple comparison.
>>
>
> We can specify an infinite set of Turing Machines by the Linz template:
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn   // Ĥ applied to ⟨Ĥ⟩ does not halt
>
> We can see that none of these machines can possibly return a Boolean
> value corresponding to the actual behavior of Ĥ applied to ⟨Ĥ⟩

That's right, Olcott! Every corresponding H doesn't solve the halting
problem. Therefore it can't be solved. The end.

On 29/02/24 16:34, olcott wrote:
> On 2/29/2024 7:29 AM, Andy Walker wrote:
>> On 29/02/2024 10:42, immibis wrote:
>> [...]
>>> The selection is easily computable, by the usual method.
>>
>>      H^ is computable from H, but that doesn't solve the pedagogic
>> problem of avoiding proof-by-contradiction and other abstractions.
>> Further, it doesn't show an example that TM#1 and TM#2 [given below]
>> get wrong.
>>
>>> In case you are unaware of the usual proof:
>>
>>      I first taught it over 50 years ago, and it has been discussed
>> "ad nauseam" in this group.  I think I'm as aware of it as anyone here,
>> modulo whatever I've forgotten over those years.
>>
>>>                           If M is the Turing
>>> machine that you think computes halting,
>>
>>      "Please, Sir, what if I /don't/ think M computes halting?"
>>
>>>                        select a machine equivalent
>>> to: [...]
>>> and then compute M(f,f).
>>> If M(f,f) doesn't halt or halts in a state other than yes/no, it has
>>> already failed to compute halting.
>>
>>      "Please, Sir, how can we know M(f,f) doesn't halt?"
>>
>>>                      If it halts in yes, the correct
>>> answer was no; if it halts in no, the correct answer was yes.
>>
>>      Yes, and most people here accept that [tidied up a bit] as a
>> valid proof.  But Ben's claim in <87v868ksuy.fsf@bsb.me.uk> was that
>> there was a selection method that caused TM#n to give the wrong answer
>> and ISTM that Mike's elaboration of that is at least as abstract as
>> some other proofs.  I don't know whether it's even possible to find a
>> proof that is acceptable to students who don't understand abstraction
>> at least as far as proof-by-contradiction [luckily, my audiences have
>> always been mathematicians or close approximations thereto].
>>
>>      To fix ideas slightly, let us suppose that [using pseudo-code
>> in place of TMs]
>>
>>    TM#1 is 'L: goto L'
>>    TM#2 is 'print ("Don't know")'
>>    TM#3 is 'print (if {A} then "halts"
>>                  elif {B} then "doesn't halt"
>>                  else "Don't know")'
>>      where '{A}' and '{B}' are Boolean procedures
>>    TM#4 is 'if {Goldbach_Conjecture} then {...}'
>>    TM#5 is some UTM emulating your 'f'
>>
>> [Note that TM#3 and TM#5 may actually be quite useful.]  What specific
>> input do these TMs get wrong?  How do you know, in a way that would
>> convince a reasonably bright student who doesn't understand abstraction?
>> FTAOD, I am not claiming that these are HDs, or that TM#1 and TM#2 get
>> anything right.
>
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn   // Ĥ applied to ⟨Ĥ⟩ does not halt
>
> H ⟨Ĥ⟩ ⟨Ĥ⟩ (in a separate memory space) merely needs to report on
> the actual behavior of Ĥ ⟨Ĥ⟩. We already know that Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ must
> transition to Ĥ.Hqy or Ĥ.Hqn, H merely needs to see which one.
>
>
Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to Ĥ.Hqy if and only if H ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to
H.Hqy because they are identical copies.

On 2/29/2024 10:00 AM, immibis wrote:
> On 29/02/24 16:49, olcott wrote:
>> On 2/29/2024 4:38 AM, immibis wrote:
>>> On 29/02/24 01:03, olcott wrote:
>>>
>>>> H.q0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qy   // H applied to ⟨Ĥ⟩ ⟨Ĥ⟩ halts
>>>> H.q0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qn   // H applied to ⟨Ĥ⟩ ⟨Ĥ⟩ does not halt
>>>>
>>>> Because H is required to always halt we can know that
>>>> Ĥ.Hq0 applied to ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to Ĥ.Hqy or Ĥ.Hqn
>>>> thus H merely needs to report on that.
>>>>
>>>> // Ĥ.q0 ⟨Ĥ⟩ copies its input then transitions to Ĥ.Hq0
>>>> // Ĥ.Hq0 is the first state of The Linz hypothetical halt decider
>>>> // H transitions to Ĥ.Hqy for halts and Ĥ.Hqn for does not halt
>>>> // ∞ means an infinite loop has been appended to the Ĥ.Hqy state
>>>> //
>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy  ∞ // Ĥ applied to ⟨Ĥ⟩ halts
>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn    // Ĥ applied to ⟨Ĥ⟩ does not halt
>>>>
>>>> When Ĥ is applied to ⟨Ĥ⟩ it contradicts whatever value that Ĥ.H
>>>> returns making Ĥ self-contradictory.
>>>>
>>>
>>> was there a purpose to posting this nonsense again? You might be
>>> automatically spam-filtered if you keep posting the same post so many
>>> times.
>>
>> All of the rebuttals have been incorrect.
>>
>
> Then why don't you explain how each one is incorrect?

I did and you ignored them.
--
Copyright 2024 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

On 2/29/2024 10:01 AM, immibis wrote:
> On 29/02/24 16:25, olcott wrote:
>> On 2/28/2024 8:32 PM, Mike Terry wrote:
>>> On 29/02/2024 01:24, Andy Walker wrote:
>>>> On 29/02/2024 00:37, Ben Bacarisse wrote:
>>>>> Alan Mackenzie <acm@muc.de> writes:
>>>>>> If you're going to be going with the contradiction argument that
>>>>>> dominates this group, rather than saying you "construct" a counter
>>>>>> example, say that you "select" it from the set of all programs, as
>>>>>> though it already existed.
>>>>> [...]
>>>>> But I do like the idea when applied to the better "no TM decides
>>>>> halting" proof.  We can number all TMs, and then "select" at least one
>>>>> input that TM number 1 get wrong.  Then we can select at least one the
>>>>> TM number 2 gets wrong and so on.  For every actual TM, there
>>>>> really is
>>>>> one we can find to show that it fails to decide halting.
>>>>
>>>>      Is there not a problem in that the "selection" is not computable?
>>>
>>> If the numbering is directly tied to the TM representation, then the
>>> mapping from TM number to "counterexample input" is computable - it
>>> is just what Linz describes in his procedure to create H^ from H.
>>> The proof that H does indeed get the <H^><H^> input wrong is also the
>>> proof from Linz.
>>
>> Linz never applies H to ⟨Ĥ⟩ ⟨Ĥ⟩ he only applies Ĥ to ⟨Ĥ⟩
>
> One part of applying Ĥ to ⟨Ĥ⟩ is identical to applying H to ⟨Ĥ⟩ ⟨Ĥ⟩.
> That it is identical cannot be ignored.
>

[1] E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf

A loophole was found in the original by Richard:
Can Carol correctly answer “no” to this question?

This version eliminates this loophole.
Can Carol correctly answer “no” to this [yes/no] question?

Carol is asked the word-for-word same question as everyone else
yet this question is self-contradictory for Carol and not
self-contradictory for anyone else.

Whether or not Ĥ halts on its input ⟨Ĥ⟩ is self-contradictory
for Ĥ.H and not self-contradictory for H.

>> Linz falsely assumes that Ĥ in a separate memory space can
>> somehow thwart H in a different memory space.
>
> There is no thwarting, and memory spaces do not exist in Turing
> machines. It is a simple fact that an embedded copy of H always returns
> the same result as H does.

That the location of the Turing Machine states is never
specified cannot possibly mean that they exist no where.

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

On 2/29/2024 10:02 AM, immibis wrote:
> On 29/02/24 16:07, olcott wrote:
>> On 2/29/2024 4:11 AM, Mikko wrote:
>>> On 2024-02-29 01:24:16 +0000, Andy Walker said:
>>>
>>>> On 29/02/2024 00:37, Ben Bacarisse wrote:
>>>>> Alan Mackenzie <acm@muc.de> writes:
>>>>>> If you're going to be going with the contradiction argument that
>>>>>> dominates this group, rather than saying you "construct" a counter
>>>>>> example, say that you "select" it from the set of all programs, as
>>>>>> though it already existed.
>>>>> [...]
>>>>> But I do like the idea when applied to the better "no TM decides
>>>>> halting" proof.  We can number all TMs, and then "select" at least one
>>>>> input that TM number 1 get wrong.  Then we can select at least one the
>>>>> TM number 2 gets wrong and so on.  For every actual TM, there
>>>>> really is
>>>>> one we can find to show that it fails to decide halting.
>>>>
>>>>     Is there not a problem in that the "selection" is not computable?
>>>> TM#1 with input [whatever] can do one of four things:  fail to halt;
>>>> halt
>>>> in some state other than "yes"/"no";  halt "yes";  or halt "no".
>>>> But we
>>>> don't [and cannot] know in general which of these applies.  So we can't
>>>> "really find" one it gets wrong, only show that one exists.  I don't
>>>> see
>>>> that this is any easier for the student than "If you claim that TM is a
>>>> halt decider, then here is a construction that shows your claim is
>>>> false".
>>>
>>> We can select it because it contains a particular algorithm to copy the
>>> input, an exact copy of H, a trivial loop appended to every "yes"-
>>> state of the copy of H, and nothing else. Just a simple comparison.
>>>
>>
>> We can specify an infinite set of Turing Machines by the Linz template:
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn   // Ĥ applied to ⟨Ĥ⟩ does not halt
>>
>> We can see that none of these machines can possibly return a Boolean
>> value corresponding to the actual behavior of Ĥ applied to ⟨Ĥ⟩
>
> That's right, Olcott! Every corresponding H doesn't solve the halting
> problem. Therefore it can't be solved. The end.

Like Carols question:
Can Carol correctly answer “no” to this [yes/no] question?
Anyone besides Carol can provide a correct answer.
Any TM besides Ĥ.H can provide a correct answer.

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

On 2/29/2024 10:03 AM, immibis wrote:
> On 29/02/24 16:34, olcott wrote:
>> On 2/29/2024 7:29 AM, Andy Walker wrote:
>>> On 29/02/2024 10:42, immibis wrote:
>>> [...]
>>>> The selection is easily computable, by the usual method.
>>>
>>>      H^ is computable from H, but that doesn't solve the pedagogic
>>> problem of avoiding proof-by-contradiction and other abstractions.
>>> Further, it doesn't show an example that TM#1 and TM#2 [given below]
>>> get wrong.
>>>
>>>> In case you are unaware of the usual proof:
>>>
>>>      I first taught it over 50 years ago, and it has been discussed
>>> "ad nauseam" in this group.  I think I'm as aware of it as anyone here,
>>> modulo whatever I've forgotten over those years.
>>>
>>>>                           If M is the Turing
>>>> machine that you think computes halting,
>>>
>>>      "Please, Sir, what if I /don't/ think M computes halting?"
>>>
>>>>                        select a machine equivalent
>>>> to: [...]
>>>> and then compute M(f,f).
>>>> If M(f,f) doesn't halt or halts in a state other than yes/no, it has
>>>> already failed to compute halting.
>>>
>>>      "Please, Sir, how can we know M(f,f) doesn't halt?"
>>>
>>>>                      If it halts in yes, the correct
>>>> answer was no; if it halts in no, the correct answer was yes.
>>>
>>>      Yes, and most people here accept that [tidied up a bit] as a
>>> valid proof.  But Ben's claim in <87v868ksuy.fsf@bsb.me.uk> was that
>>> there was a selection method that caused TM#n to give the wrong answer
>>> and ISTM that Mike's elaboration of that is at least as abstract as
>>> some other proofs.  I don't know whether it's even possible to find a
>>> proof that is acceptable to students who don't understand abstraction
>>> at least as far as proof-by-contradiction [luckily, my audiences have
>>> always been mathematicians or close approximations thereto].
>>>
>>>      To fix ideas slightly, let us suppose that [using pseudo-code
>>> in place of TMs]
>>>
>>>    TM#1 is 'L: goto L'
>>>    TM#2 is 'print ("Don't know")'
>>>    TM#3 is 'print (if {A} then "halts"
>>>                  elif {B} then "doesn't halt"
>>>                  else "Don't know")'
>>>      where '{A}' and '{B}' are Boolean procedures
>>>    TM#4 is 'if {Goldbach_Conjecture} then {...}'
>>>    TM#5 is some UTM emulating your 'f'
>>>
>>> [Note that TM#3 and TM#5 may actually be quite useful.]  What specific
>>> input do these TMs get wrong?  How do you know, in a way that would
>>> convince a reasonably bright student who doesn't understand abstraction?
>>> FTAOD, I am not claiming that these are HDs, or that TM#1 and TM#2 get
>>> anything right.
>>
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn   // Ĥ applied to ⟨Ĥ⟩ does not halt
>>
>> H ⟨Ĥ⟩ ⟨Ĥ⟩ (in a separate memory space) merely needs to report on
>> the actual behavior of Ĥ ⟨Ĥ⟩. We already know that Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ must
>> transition to Ĥ.Hqy or Ĥ.Hqn, H merely needs to see which one.
>>
>>
> Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to Ĥ.Hqy if and only if H ⟨Ĥ⟩ ⟨Ĥ⟩ transitions to
> H.Hqy because they are identical copies.

That everyone assumes so does not make this assumption correct.

Like Carols question:
Can Carol correctly answer “no” to this [yes/no] question?
Anyone besides Carol can provide a correct answer.
Any TM besides Ĥ.H can provide a correct answer.

E C R Hehner. Objective and Subjective Specifications
WST Workshop on Termination, Oxford. 2018 July 18.
See https://www.cs.toronto.edu/~hehner/OSS.pdf

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

On 2024-02-29 15:51:56 +0000, olcott said:

> H ⟨Ĥ⟩ ⟨Ĥ⟩ (in a separate memory space) merely needs to report on

A Turing machine is not in any memory space.

--
Mikko