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.

--
Ben.

On 19/02/2024 11:28, Ben Bacarisse wrote:
[HP proofs:]
> 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.

Moral: Don't try to teach such things to non-mathematicians?
In my time as a student, there were no CS/IT [first] degrees, and few
computing courses of any sort other than for mathematicians, which no
doubt coloured what went into them.

> 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.
When I did teach this stuff, I pretty-much followed the Minsky
route -- if H is a halt decider then [blah, blah], contradiction. My
lecture notes are on the web at

http://http://www.cuboid.me.uk/anw/G12FCO/lect17.html

[a reference I've given before], see about two-thirds down the page.
The following lecture and indeed the whole module are also relevant;
they are linked from the bottom of that page. In the light of what
has happened in this group, I might now, nearly 30 years later, be
tempted to do it via Busy Beaver, but both that and the Linz-style
proofs via languages seem to me a bit much for non-mathematicians.
So I would probably start not from "H is a halt decider" but rather
from "Let H be any program" [doing an abstract computation], then
"here is a construction" [usual hat stuff] showing that H is not a
halt decider. So there are no [perfect] halt deciders, QED. I think
that can be made more non-mathematician friendly. IOW, I think that
"So H is not a HD" is more friendly than "H /is/ a HD leads to a
contradiction".

There is still the problem that showing that something has
/a/ counter-example is not satisfying; it suggests that if only we
could tweak the problem slightly to avoid that one case, all would
be well. Lecture 18 from the above module addresses this in some
detail, inc the use of emulation; but I think this is the area in
which some contributors here get misled.

Meanwhile, I note from the above lecture notes:

" If you understand this proof at first glance, you are too clever
" to be doing this module, and should probably have been giving it.
" If you think you understand this proof at first glance, you
" probably don't. If you think you will /never/ understand this
" proof, please just run through it again, enlightenment will
" eventually dawn. "

How that relates to contributors here, I leave to the imagination.

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

On 02/19/2024 06:50 AM, Andy Walker wrote:
> On 19/02/2024 11:28, Ben Bacarisse wrote:
> [HP proofs:]
>> 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.
>
> Moral: Don't try to teach such things to non-mathematicians?
> In my time as a student, there were no CS/IT [first] degrees, and few
> computing courses of any sort other than for mathematicians, which no
> doubt coloured what went into them.
>
>> 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.
> When I did teach this stuff, I pretty-much followed the Minsky
> route -- if H is a halt decider then [blah, blah], contradiction. My
> lecture notes are on the web at
>
> http://http://www.cuboid.me.uk/anw/G12FCO/lect17.html
>
> [a reference I've given before], see about two-thirds down the page.
> The following lecture and indeed the whole module are also relevant;
> they are linked from the bottom of that page. In the light of what
> has happened in this group, I might now, nearly 30 years later, be
> tempted to do it via Busy Beaver, but both that and the Linz-style
> proofs via languages seem to me a bit much for non-mathematicians.
> So I would probably start not from "H is a halt decider" but rather
> from "Let H be any program" [doing an abstract computation], then
> "here is a construction" [usual hat stuff] showing that H is not a
> halt decider. So there are no [perfect] halt deciders, QED. I think
> that can be made more non-mathematician friendly. IOW, I think that
> "So H is not a HD" is more friendly than "H /is/ a HD leads to a
> contradiction".
>
> There is still the problem that showing that something has
> /a/ counter-example is not satisfying; it suggests that if only we
> could tweak the problem slightly to avoid that one case, all would
> be well. Lecture 18 from the above module addresses this in some
> detail, inc the use of emulation; but I think this is the area in
> which some contributors here get misled.
>
> Meanwhile, I note from the above lecture notes:
>
> " If you understand this proof at first glance, you are too clever
> " to be doing this module, and should probably have been giving it.
> " If you think you understand this proof at first glance, you
> " probably don't. If you think you will /never/ understand this
> " proof, please just run through it again, enlightenment will
> " eventually dawn. "
>
> How that relates to contributors here, I leave to the imagination.
>

It's a difficult enough concept "random access memory"
and "0-based or 1-based address offset computation"
and these kinds of things, figuring that students
know algebra and geometry at all.

You figure they're going to need "order theory", for
ordinals, about set theory, then the presentation of
set theory's trans-finites, is sort of necessary to
"put zero and infinity on the same page".

Then that the Halting problem and Church and Rice and
Goedel's and most all that is "the antidiagonal argument",
otherwise has for "recursion theory" maybe it's better
to have them get into "Concrete Mathematics" so that
they already have the usual notions of boundedness
and unboundedness, relating it to their geometry
and their algebra and their pre-calculus and calculus.

The "recurrence relations" are tougher than long division.

Of course they should know about Buridan's donkey, and
about the Heap/Sorites, and about Zeno, all the,
"paradoxes", of logic, before getting into,
"non-constructivist results after the trans-finite
in asymptotics in recursion theory".

I'm glad that when I learned logic it was De Morgan
and modus ponens and modus tollens and all that,
if it'd been "quasi-modal after ex falso quodlibet"
and I didn't already know "dividing by zero can just
lead to wrong results" I'd hope that I'd've rejected
it and said "there's the door, Monty Haul".

(I mostly learned "logic" from "logic puzzles".)

(I'm a "full-stack all-phases dev eng ops in the
enterprise corp" type that happens to have a copy
of Boolos and also have read into Forster, about
"set theories with universes" and such.)

Maybe try sticking with constructivism, related
rates, and asymptotics, and what, analysis,
instead of like "here's a quick reason to give up".

Of course formal automata and formal methods are great,
accepter/rejector, automata like the right linear,
they can help a lot for introductory, fundamental,
coding and information theory and signal theory,
that will be true everywhere and constructive.

The Entscheidungs though is kind of like,
well, there are various law(s) of large numbers, ....

Formal languages, ....

I don't know any results of Linz.

On 2/19/2024 10:17 AM, Ross Finlayson wrote:
> On 02/19/2024 06:50 AM, Andy Walker wrote:
>> On 19/02/2024 11:28, Ben Bacarisse wrote:
>> [HP proofs:]
>>> 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.
>>
>>      Moral:  Don't try to teach such things to non-mathematicians?
>> In my time as a student, there were no CS/IT [first] degrees, and few
>> computing courses of any sort other than for mathematicians, which no
>> doubt coloured what went into them.
>>
>>> 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.
>>      When I did teach this stuff, I pretty-much followed the Minsky
>> route -- if H is a halt decider then [blah, blah], contradiction.  My
>> lecture notes are on the web at
>>
>>    http://http://www.cuboid.me.uk/anw/G12FCO/lect17.html
>>
>> [a reference I've given before], see about two-thirds down the page.
>> The following lecture and indeed the whole module are also relevant;
>> they are linked from the bottom of that page.  In the light of what
>> has happened in this group, I might now, nearly 30 years later, be
>> tempted to do it via Busy Beaver, but both that and the Linz-style
>> proofs via languages seem to me a bit much for non-mathematicians.
>> So I would probably start not from "H is a halt decider" but rather
>> from "Let H be any program" [doing an abstract computation], then
>> "here is a construction" [usual hat stuff] showing that H is not a
>> halt decider.  So there are no [perfect] halt deciders, QED.  I think
>> that can be made more non-mathematician friendly.  IOW, I think that
>> "So H is not a HD" is more friendly than "H /is/ a HD leads to a
>> contradiction".
>>
>>      There is still the problem that showing that something has
>> /a/ counter-example is not satisfying;  it suggests that if only we
>> could tweak the problem slightly to avoid that one case, all would
>> be well.  Lecture 18 from the above module addresses this in some
>> detail, inc the use of emulation;  but I think this is the area in
>> which some contributors here get misled.
>>
>>      Meanwhile, I note from the above lecture notes:
>>
>>    " If you understand this proof at first glance, you are too clever
>>    " to be doing this module, and should probably have been giving it.
>>    " If you think you understand this proof at first glance, you
>>    " probably don't. If you think you will /never/ understand this
>>    " proof, please just run through it again, enlightenment will
>>    " eventually dawn. "
>>
>> How that relates to contributors here, I leave to the imagination.
>>
>
> It's a difficult enough concept "random access memory"
> and "0-based or 1-based address offset computation"
> and these kinds of things, figuring that students
> know algebra and geometry at all.
>
> You figure they're going to need "order theory", for
> ordinals, about set theory, then the presentation of
> set theory's trans-finites, is sort of necessary to
> "put zero and infinity on the same page".
>
> Then that the Halting problem and Church and Rice and
> Goedel's and most all that is "the antidiagonal argument",
> otherwise has for "recursion theory" maybe it's better
> to have them get into "Concrete Mathematics" so that
> they already have the usual notions of boundedness
> and unboundedness, relating it to their geometry
> and their algebra and their pre-calculus and calculus.
>
> The "recurrence relations" are tougher than long division.
>
> Of course they should know about Buridan's donkey, and
> about the Heap/Sorites, and about Zeno, all the,
> "paradoxes", of logic, before getting into,
> "non-constructivist results after the trans-finite
> in asymptotics in recursion theory".
>
> I'm glad that when I learned logic it was De Morgan
> and modus ponens and modus tollens and all that,
> if it'd been "quasi-modal after ex falso quodlibet"
> and I didn't already know "dividing by zero can just
> lead to wrong results" I'd hope that I'd've rejected
> it and said "there's the door, Monty Haul".
>
> (I mostly learned "logic" from "logic puzzles".)
>
> (I'm a "full-stack all-phases dev eng ops in the
> enterprise corp" type that happens to have a copy
> of Boolos and also have read into Forster, about
> "set theories with universes" and such.)
>
> Maybe try sticking with constructivism, related
> rates, and asymptotics, and what, analysis,
> instead of like "here's a quick reason to give up".
>
>
> Of course formal automata and formal methods are great,
> accepter/rejector, automata like the right linear,
> they can help a lot for introductory, fundamental,
> coding and information theory and signal theory,
> that will be true everywhere and constructive.
>
> The Entscheidungs though is kind of like,
> well, there are various law(s) of large numbers, ....
>
> Formal languages, ....
>
> I don't know any results of Linz.
>
>

The issue is not that I do not know enough computer science
the issue that that technical people are utterly clueless
about analytical truthmaker theory. They have been indoctrinated
to believe that:

....14 Every epistemological antinomy can likewise be used for a similar
undecidability proof...(Gödel 1931:43)
is not nonsense.

Analytical truthmaker theory knows that it <is> nonsense.

--
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-19 11:28:19 +0000, Ben Bacarisse said:

> Conversely, the classical proof by contradiction seems to lead a lot of
> non-mathematical students astray.

Therefore i'd prefer a direct proof, e.g., if M is a Turing machine
then M is not a halt decider for Turing machines.

--
Mikko

On 2/19/2024 1:15 PM, Mikko wrote:
> On 2024-02-19 11:28:19 +0000, Ben Bacarisse said:
>
>> Conversely, the classical proof by contradiction seems to lead a lot of
>> non-mathematical students astray.
>
> Therefore i'd prefer a direct proof, e.g., if M is a Turing machine
> then M is not a halt decider for Turing machines.
>

That is isomorphic to the Tarski Undefinability theorem proof:
If a truth predicate exists then
Boolean True(English, "This sentence is not true.")
correctly returns true or false.

That technical people are clueless about analytical truth makers
means that they lack the basis to correctly evaluate these things.

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

On 02/19/2024 11:15 AM, Mikko wrote:
> On 2024-02-19 11:28:19 +0000, Ben Bacarisse said:
>
>> Conversely, the classical proof by contradiction seems to lead a lot of
>> non-mathematical students astray.
>
> Therefore i'd prefer a direct proof, e.g., if M is a Turing machine
> then M is not a halt decider for Turing machines.
>

What about if M_0(n) is a Turing machine of finite bound n,
then there exists M_1(m) where m > n or m >> n,
that is a halt decider for M_0(n).

How about that?

Goedel has "completeness results" before "incompleteness results".
(The rulial, the regular, the ordinary, the proportional, ....)

Whether there's an M_2(o) for o < n that is a halt decider for M_0(n), ....

This then can introduce Chaitin's ideas, about what are
the "probabilities" of "random" machines halting, or its
alternatives: looping or growing unboundedly.

Of course anything that involves the anti-diagonal,
or the Diagonal Argument or Diagonal Method as sometimes
it's called, some have that as a proof by contradiction
also, i.e. it assumes something is, shows it isn't, ....

Having "completeness" results first can go a long
way then for helping establish the reasoning why
there results "inductive impasse" or forward inductive
impasse, and why deductive inference arrives at sorts
"bridge" results of otherwise what just talks past itself.

Then for infinite tapes, first is the sort of results
that result completion in those, i.e., given that
M_a is an instance of a Turing machine, there's for example
the co-completions, like notions of co-consistency,
is for not leaving students adrift at "give up".

Assume there's an ordinary inductive set, its elements
in a theory of only sets that don't contain themselves,
quantify over that, it's the Russell set, it's extra-ordinary
or a fragment, the, "double reductio", ....

That's for you, though, to figure out.

On 2/19/2024 2:29 PM, Ross Finlayson wrote:
> On 02/19/2024 11:15 AM, Mikko wrote:
>> On 2024-02-19 11:28:19 +0000, Ben Bacarisse said:
>>
>>> Conversely, the classical proof by contradiction seems to lead a lot of
>>> non-mathematical students astray.
>>
>> Therefore i'd prefer a direct proof, e.g., if M is a Turing machine
>> then M is not a halt decider for Turing machines.
>>
>
> What about if M_0(n) is a Turing machine of finite bound n,
> then there exists M_1(m) where m > n or m >> n,
> that is a halt decider for M_0(n).
>
> How about that?
>
> Goedel has "completeness results" before "incompleteness results".
> (The rulial, the regular, the ordinary, the proportional, ....)
>
> Whether there's an M_2(o) for o < n that is a halt decider for M_0(n), ....
>
> This then can introduce Chaitin's ideas, about what are
> the "probabilities" of "random" machines halting, or its
> alternatives: looping or growing unboundedly.
>
>
> Of course anything that involves the anti-diagonal,
> or the Diagonal Argument or Diagonal Method as sometimes
> it's called, some have that as a proof by contradiction
> also, i.e. it assumes something is, shows it isn't, ....
>
> Having "completeness" results first can go a long
> way then for helping establish the reasoning why
> there results "inductive impasse" or forward inductive
> impasse, and why deductive inference arrives at sorts
> "bridge" results of otherwise what just talks past itself.
>
> Then for infinite tapes, first is the sort of results
> that result completion in those, i.e., given that
> M_a is an instance of a Turing machine, there's for example
> the co-completions, like notions of co-consistency,
> is for not leaving students adrift at "give up".
>
>
> Assume there's an ordinary inductive set, its elements
> in a theory of only sets that don't contain themselves,
> quantify over that, it's the Russell set, it's extra-ordinary
> or a fragment, the, "double reductio", ....
>
> That's for you, though, to figure out.
>
>

....14 Every epistemological antinomy can likewise be used for a similar
undecidability proof...(Gödel 1931:43)

Conclusively proves that Gödel was totally clueless about
analytic truth-makers.

x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x
https://liarparadox.org/Tarski_275_276.pdf
Proves that Tarski made the same mistake.

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

Andy Walker <anw@cuboid.co.uk> writes:

> On 19/02/2024 11:28, Ben Bacarisse wrote:
> [HP proofs:]
>> 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.
>
> Moral: Don't try to teach such things to non-mathematicians?

That's not really an option in many cases.

> In my time as a student, there were no CS/IT [first] degrees, and few
> computing courses of any sort other than for mathematicians, which no
> doubt coloured what went into them.
>
>> 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.
> When I did teach this stuff, I pretty-much followed the Minsky
> route -- if H is a halt decider then [blah, blah], contradiction. My
> lecture notes are on the web at
>
> http://http://www.cuboid.me.uk/anw/G12FCO/lect17.html

Thanks. What were the students studying?

You may have misunderstood the reference to Minsky machines as your
proof is based on TMs. Minsky wrote a lot about TMS but Minsky machines
are counter machines, often drawn as FSMs, with increment, decrement and
"follow on zero" arcs between states.

(A minor point, your proof is not of the halting theorem, but of a very
closely related problem that is often called something like "self
accept".)

> [a reference I've given before], see about two-thirds down the page.
> The following lecture and indeed the whole module are also relevant;
> they are linked from the bottom of that page. In the light of what
> has happened in this group, I might now, nearly 30 years later, be
> tempted to do it via Busy Beaver, but both that and the Linz-style
> proofs via languages seem to me a bit much for non-mathematicians.
> So I would probably start not from "H is a halt decider" but rather
> from "Let H be any program" [doing an abstract computation], then
> "here is a construction" [usual hat stuff] showing that H is not a
> halt decider. So there are no [perfect] halt deciders, QED.

This ended up as my preferred argument.

> I think
> that can be made more non-mathematician friendly. IOW, I think that
> "So H is not a HD" is more friendly than "H /is/ a HD leads to a
> contradiction".

100% with you on this.

> There is still the problem that showing that something has
> /a/ counter-example is not satisfying; it suggests that if only we
> could tweak the problem slightly to avoid that one case, all would
> be well. Lecture 18 from the above module addresses this in some
> detail, inc the use of emulation; but I think this is the area in
> which some contributors here get misled.

Yes. There's an inherent problem here. We must show one actual
constructable counter-example, but that leads to the "just spot it"
avoidance issue. I would address that by giving simpler examples like
"no number is the largest".

> Meanwhile, I note from the above lecture notes:
>
> " If you understand this proof at first glance, you are too clever
> " to be doing this module, and should probably have been giving it.
> " If you think you understand this proof at first glance, you
> " probably don't. If you think you will /never/ understand this
> " proof, please just run through it again, enlightenment will
> " eventually dawn. "
>
> How that relates to contributors here, I leave to the imagination.

--
Ben.

On 2/19/2024 5:38 PM, Ben Bacarisse wrote:
> Andy Walker <anw@cuboid.co.uk> writes:
>
>> On 19/02/2024 11:28, Ben Bacarisse wrote:
>> [HP proofs:]
>>> 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.
>>
>> Moral: Don't try to teach such things to non-mathematicians?
>
> That's not really an option in many cases.
>
>> In my time as a student, there were no CS/IT [first] degrees, and few
>> computing courses of any sort other than for mathematicians, which no
>> doubt coloured what went into them.
>>
>>> 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.
>> When I did teach this stuff, I pretty-much followed the Minsky
>> route -- if H is a halt decider then [blah, blah], contradiction. My
>> lecture notes are on the web at
>>
>> http://http://www.cuboid.me.uk/anw/G12FCO/lect17.html
>
> Thanks. What were the students studying?
>
> You may have misunderstood the reference to Minsky machines as your
> proof is based on TMs. Minsky wrote a lot about TMS but Minsky machines
> are counter machines, often drawn as FSMs, with increment, decrement and
> "follow on zero" arcs between states.
>
> (A minor point, your proof is not of the halting theorem, but of a very
> closely related problem that is often called something like "self
> accept".)
>
>> [a reference I've given before], see about two-thirds down the page.
>> The following lecture and indeed the whole module are also relevant;
>> they are linked from the bottom of that page. In the light of what
>> has happened in this group, I might now, nearly 30 years later, be
>> tempted to do it via Busy Beaver, but both that and the Linz-style
>> proofs via languages seem to me a bit much for non-mathematicians.
>> So I would probably start not from "H is a halt decider" but rather
>> from "Let H be any program" [doing an abstract computation], then
>> "here is a construction" [usual hat stuff] showing that H is not a
>> halt decider. So there are no [perfect] halt deciders, QED.
>
> This ended up as my preferred argument.
>
>> I think
>> that can be made more non-mathematician friendly. IOW, I think that
>> "So H is not a HD" is more friendly than "H /is/ a HD leads to a
>> contradiction".
>
> 100% with you on this.
>
>> There is still the problem that showing that something has
>> /a/ counter-example is not satisfying; it suggests that if only we
>> could tweak the problem slightly to avoid that one case, all would
>> be well. Lecture 18 from the above module addresses this in some
>> detail, inc the use of emulation; but I think this is the area in
>> which some contributors here get misled.
>
> Yes. There's an inherent problem here. We must show one actual
> constructable counter-example, but that leads to the "just spot it"
> avoidance issue. I would address that by giving simpler examples like
> "no number is the largest".
>
>> Meanwhile, I note from the above lecture notes:
>>
>> " If you understand this proof at first glance, you are too clever
>> " to be doing this module, and should probably have been giving it.
>> " If you think you understand this proof at first glance, you
>> " probably don't. If you think you will /never/ understand this
>> " proof, please just run through it again, enlightenment will
>> " eventually dawn. "
>>
>> How that relates to contributors here, I leave to the imagination.
>

I now have two PhD computer science professors
independently affirm my 2004 statement.

*Problems with the Halting Problem* Eric C.R. Hehner (2011)
COMPUTING2011 Symposium on 75 years of Turing Machine and
Lambda-Calculus, Karlsruhe Germany, invited, 2011 October 20-21;
Advances in Computer Science and Engineering v.10 n.1 p.31-60, 2013
https://www.cs.toronto.edu/~hehner/PHP.pdf

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

Bill Stoddart. *The Halting Paradox*
20 December 2017
https://arxiv.org/abs/1906.05340
arXiv:1906.05340 [cs.LO]

Alan Turing's Halting Problem is incorrectly formed (PART-TWO) sci.logic
On 6/20/2004 11:31 AM, Peter Olcott wrote:
> PREMISES:
> (1) The Halting Problem was specified in such a way that a solution
> was defined to be impossible.
>
> (2) The set of questions that are defined to not have any possible
> correct answer(s) forms a proper subset of all possible questions.
> …
> CONCLUSION:
> Therefore the Halting Problem is an ill-formed question.
>
USENET Message-ID:
<kZiBc.103407$Gx4.18142@bgtnsc04-news.ops.worldnet.att.net>

On 19/02/24 17:27, olcott wrote:
> On 2/19/2024 10:17 AM, Ross Finlayson wrote:
>> On 02/19/2024 06:50 AM, Andy Walker wrote:
>>> On 19/02/2024 11:28, Ben Bacarisse wrote:
>>> [HP proofs:]
>>>> 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.
>>>
>>>      Moral:  Don't try to teach such things to non-mathematicians?
>>> In my time as a student, there were no CS/IT [first] degrees, and few
>>> computing courses of any sort other than for mathematicians, which no
>>> doubt coloured what went into them.
>>>
>>>> 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.
>>>      When I did teach this stuff, I pretty-much followed the Minsky
>>> route -- if H is a halt decider then [blah, blah], contradiction.  My
>>> lecture notes are on the web at
>>>
>>>    http://http://www.cuboid.me.uk/anw/G12FCO/lect17.html
>>>
>>> [a reference I've given before], see about two-thirds down the page.
>>> The following lecture and indeed the whole module are also relevant;
>>> they are linked from the bottom of that page.  In the light of what
>>> has happened in this group, I might now, nearly 30 years later, be
>>> tempted to do it via Busy Beaver, but both that and the Linz-style
>>> proofs via languages seem to me a bit much for non-mathematicians.
>>> So I would probably start not from "H is a halt decider" but rather
>>> from "Let H be any program" [doing an abstract computation], then
>>> "here is a construction" [usual hat stuff] showing that H is not a
>>> halt decider.  So there are no [perfect] halt deciders, QED.  I think
>>> that can be made more non-mathematician friendly.  IOW, I think that
>>> "So H is not a HD" is more friendly than "H /is/ a HD leads to a
>>> contradiction".
>>>
>>>      There is still the problem that showing that something has
>>> /a/ counter-example is not satisfying;  it suggests that if only we
>>> could tweak the problem slightly to avoid that one case, all would
>>> be well.  Lecture 18 from the above module addresses this in some
>>> detail, inc the use of emulation;  but I think this is the area in
>>> which some contributors here get misled.
>>>
>>>      Meanwhile, I note from the above lecture notes:
>>>
>>>    " If you understand this proof at first glance, you are too clever
>>>    " to be doing this module, and should probably have been giving it.
>>>    " If you think you understand this proof at first glance, you
>>>    " probably don't. If you think you will /never/ understand this
>>>    " proof, please just run through it again, enlightenment will
>>>    " eventually dawn. "
>>>
>>> How that relates to contributors here, I leave to the imagination.
>>>
>>
>> It's a difficult enough concept "random access memory"
>> and "0-based or 1-based address offset computation"
>> and these kinds of things, figuring that students
>> know algebra and geometry at all.
>>
>> You figure they're going to need "order theory", for
>> ordinals, about set theory, then the presentation of
>> set theory's trans-finites, is sort of necessary to
>> "put zero and infinity on the same page".
>>
>> Then that the Halting problem and Church and Rice and
>> Goedel's and most all that is "the antidiagonal argument",
>> otherwise has for "recursion theory" maybe it's better
>> to have them get into "Concrete Mathematics" so that
>> they already have the usual notions of boundedness
>> and unboundedness, relating it to their geometry
>> and their algebra and their pre-calculus and calculus.
>>
>> The "recurrence relations" are tougher than long division.
>>
>> Of course they should know about Buridan's donkey, and
>> about the Heap/Sorites, and about Zeno, all the,
>> "paradoxes", of logic, before getting into,
>> "non-constructivist results after the trans-finite
>> in asymptotics in recursion theory".
>>
>> I'm glad that when I learned logic it was De Morgan
>> and modus ponens and modus tollens and all that,
>> if it'd been "quasi-modal after ex falso quodlibet"
>> and I didn't already know "dividing by zero can just
>> lead to wrong results" I'd hope that I'd've rejected
>> it and said "there's the door, Monty Haul".
>>
>> (I mostly learned "logic" from "logic puzzles".)
>>
>> (I'm a "full-stack all-phases dev eng ops in the
>> enterprise corp" type that happens to have a copy
>> of Boolos and also have read into Forster, about
>> "set theories with universes" and such.)
>>
>> Maybe try sticking with constructivism, related
>> rates, and asymptotics, and what, analysis,
>> instead of like "here's a quick reason to give up".
>>
>>
>> Of course formal automata and formal methods are great,
>> accepter/rejector, automata like the right linear,
>> they can help a lot for introductory, fundamental,
>> coding and information theory and signal theory,
>> that will be true everywhere and constructive.
>>
>> The Entscheidungs though is kind of like,
>> well, there are various law(s) of large numbers, ....
>>
>> Formal languages, ....
>>
>> I don't know any results of Linz.
>>
>>
>
> The issue is not that I do not know enough computer science
> the issue that that technical people are utterly clueless
> about analytical truthmaker theory.

That's because you just made it up.

> They have been indoctrinated
> to believe that:
>
> ...14 Every epistemological antinomy can likewise be used for a similar
> undecidability proof...(Gödel 1931:43)
> is not nonsense.

"Epistemological antinomy" sounds like something Gödel just made up. I
have no idea what this means and I am certainly not indoctrinated to
believe it.

Mikko <mikko.levanto@iki.fi> writes:

> On 2024-02-19 11:28:19 +0000, Ben Bacarisse said:
>
>> Conversely, the classical proof by contradiction seems to lead a lot of
>> non-mathematical students astray.
>
> Therefore i'd prefer a direct proof, e.g., if M is a Turing machine
> then M is not a halt decider for Turing machines.

Yes, that's how I ended up doing it in class.

--
Ben.

Ross Finlayson <ross.a.finlayson@gmail.com> writes:

> What about if M_0(n) is a Turing machine of finite bound n,

Care to define what that you mean?

> then there exists M_1(m) where m > n or m >> n,
> that is a halt decider for M_0(n).

I'm not sure what role the subscripts 0 and 1 are playing here. Also,
I'd urge you to be careful about terms like "X is a ..." when I think
you mean "X is any one of the class of ...". It's OK provided everyone
is on board, but when things are new, extra care is sometimes needed.

> How about that?

With appropriate definitions, I feel sure sure one can do something like
that.

Why are interested in such results? Do they lead to some interesting
theory?

--
Ben.

On 20/02/24 00:38, Ben Bacarisse wrote:
> Yes. There's an inherent problem here. We must show one actual
> constructable counter-example, but that leads to the "just spot it"
> avoidance issue. I would address that by giving simpler examples like
> "no number is the largest".

I seem to recall that Olcott avoided talking about the fact his style of
"proof" that a halting decider exists also "proves" that a biggest
natural number exists. So this example might not work either.

(It's 5. Proof: Any number bigger than 5 was intentionally defined to be
contradictory to the fact that 5 is the biggest natural number, so it
doesn't count. Since no number can be proven to be bigger than 5, 5 is
the biggest.)

On 19/02/24 20:36, olcott wrote:
> On 2/19/2024 1:15 PM, Mikko wrote:
>> On 2024-02-19 11:28:19 +0000, Ben Bacarisse said:
>>
>>> Conversely, the classical proof by contradiction seems to lead a lot of
>>> non-mathematical students astray.
>>
>> Therefore i'd prefer a direct proof, e.g., if M is a Turing machine
>> then M is not a halt decider for Turing machines.
>>
>
> That is isomorphic to the Tarski Undefinability theorem proof:
> If a truth predicate exists then
> Boolean True(English, "This sentence is not true.")
> correctly returns true or false.
>
> That technical people are clueless about analytical truth makers
> means that they lack the basis to correctly evaluate these things.
>

The fact that M is not a halt decider for Turing machines is completely
unrelated to Tarski's undefinability theorem, and "analytical truth
maker" is something you made up.

On 2/19/24 11:27 AM, olcott wrote:

> The issue is not that I do not know enough computer science
> the issue that that technical people are utterly clueless
> about analytical truthmaker theory. They have been indoctrinated
> to believe that:
>
> ...14 Every epistemological antinomy can likewise be used for a similar
> undecidability proof...(Gödel 1931:43)
> is not nonsense.
>
> Analytical truthmaker theory knows that it <is> nonsense.
>

No, the issue IS that you don't understand enough about Computer Science
to understand what the papers are talking about.

You don't seem to understand enough about how logic works to actually
understand what Analytical Truthmaker Theory actually would say (or ANY
Analytical Theory for that matter).

Note, a lot of "Truthmaker" discussions seem to be very much in the
"metaphysical" realm, an NOT part of "Formal Logic", which seems to be a
foreign concept to you (which is one big source of your errors).

On 2/19/24 10:08 PM, immibis wrote:
> On 19/02/24 20:36, olcott wrote:
>> On 2/19/2024 1:15 PM, Mikko wrote:
>>> On 2024-02-19 11:28:19 +0000, Ben Bacarisse said:
>>>
>>>> Conversely, the classical proof by contradiction seems to lead a lot of
>>>> non-mathematical students astray.
>>>
>>> Therefore i'd prefer a direct proof, e.g., if M is a Turing machine
>>> then M is not a halt decider for Turing machines.
>>>
>>
>> That is isomorphic to the Tarski Undefinability theorem proof:
>> If a truth predicate exists then
>> Boolean True(English, "This sentence is not true.")
>> correctly returns true or false.
>>
>> That technical people are clueless about analytical truth makers
>> means that they lack the basis to correctly evaluate these things.
>>
>
> The fact that M is not a halt decider for Turing machines is completely
> unrelated to Tarski's undefinability theorem, and "analytical truth
> maker" is something you made up.

"Truthmaker Theory" is a real thing, but seems to be way out in the
metaphysics space.

Olcott seems to be trying to tie the term "Truthmaker" with the idea
that Analytic Logic works by DEFINING that things are Analytically True
if they follow from a connection to the fundamental "Truthmakers" of the
system.

Of course, in Analytical Theory, there is no arguement about
"Truthmakers" are presumed by the definitions. It is only the
non-analytic metaphysicians that argue if all truth is tied to truthmakers.

So, just another of Peters ignorance of what he is talking about.

On 02/19/2024 04:15 PM, Ben Bacarisse wrote:
> Ross Finlayson <ross.a.finlayson@gmail.com> writes:
>
>> What about if M_0(n) is a Turing machine of finite bound n,
>
> Care to define what that you mean?
>
>> then there exists M_1(m) where m > n or m >> n,
>> that is a halt decider for M_0(n).
>
> I'm not sure what role the subscripts 0 and 1 are playing here. Also,
> I'd urge you to be careful about terms like "X is a ..." when I think
> you mean "X is any one of the class of ...". It's OK provided everyone
> is on board, but when things are new, extra care is sometimes needed.
>
>> How about that?
>
> With appropriate definitions, I feel sure sure one can do something like
> that.
>
> Why are interested in such results? Do they lead to some interesting
> theory?
>

I think it's good the concept that the halting problem
makes for an argument that "static analysis always halts".

What I mean by that is relating it to something like Zeno,
you show it doesn't go through, so show it never gets anywhere.

So, showing completeness results first, then makes
for that the student doesn't get left with the idea
of "give up", instead "get over it", or "get through it".

I.e. the idea is to make sure that there's completeness first,
then, to forestall the feeling locked in with absence of
free will or the conscious about it, instead, that incompleteness
is sort of framed as about "there's asymptotic freedom",
in a sense.

Either way it's sort of liberating "my Turing machine can compute"
or "the Turing machine can't compute me". Here the idea is to
make sure there's that "my Turing machine can compute", first,
then "the Turing machine can't compute me" doesn't result
"my Turing machine can't compute".

Framing these kinds of things in universals and the infinite
is sort of for "it's an open box", for the anxiety-prone of
the claustrophobic sort, vis-a-vis the agoraphobe, fear of
being closed in or wide-open spaces. I.e. for not offending
the sensibilities, is first for "here's the great part,
it's closed, out through the unbounded, each is closed",
you know, deterministic, then "here's the kicker: it's open",
so that then they can imagine it in the infinite.

(Here the subscripts are just to indicate the generator
and the instructions, about what populates the tape
then what reads the tape.)

(The, "epistemological antinomies" would probably relate
to "non-logical/properly-logical paradoxes" meaning
terms introduced above the logic, vis-a-vis "logical
paradoxes", what are just any of the usual sorts class/set
distinction issues like in set theory after expansion of
comprehension into quantifier disambiguation. Here for
example the UTM has the monad of its state, it's sort of
non-logical.)

I'm only a practicing sort of corp enterprise software
eng dev where UTM's are really academic, but formal languages
about automata more generally like state-machines are real
apropos, there are bounds, it's unbounded, then I usually
sort of describe things "survey, audit, gap", in terms of
"sensible, fungible, tractable". Got to know your "Big O".

I studied foundations for thirty years though and sort of
have a combined approach about uncountability and logical
paradox, though. Like in my youtube videos or 10,000's posts
to sci.math I demand that there are at least three continuous
domains in mathematics, including line-reals [0,1], the
complete ordered field as field-reals, and signal-reals,
about the analytic construction, and their doubling/halving spaces.
So, I would probably explore that first, ..., Zeno you know.
Yet, that's my opinion.

Like "today we're going to talk Halting Problem or Entscheidungs,
Branching Problem. Does anybody not know Zeno? Has everybody
got that Goedel has complete arithmetic then incomplete arithmetic?
Cantor's Uncountability and the Diagonal or Anti-Diagonal?
Alright, since we already have bounded-tape Turing machines,
Halting Problem is about same as Goedel incompleteness."

Otherwise I'd just kind of leave that out. It's enrichment,
vis-a-vis formal languages, accepter/rejector, automata,
states, open/closed items, in time, these kinds of things.

I'd make such notions more part of a survey in foundations
or formal systems than formal languages and formal automata
(defined, deterministic, and closed).

Russell's Antinomy, Goedel's Incompleteness, the Halting Problem,
Cantor's Paradox (the universe would be its own powerset),
these sort of go together in "a survey of confounding results".

Zeno, ....

On 2/19/2024 10:21 PM, Ross Finlayson wrote:
> On 02/19/2024 04:15 PM, Ben Bacarisse wrote:
>> Ross Finlayson <ross.a.finlayson@gmail.com> writes:
>>
>>> What about if M_0(n) is a Turing machine of finite bound n,
>>
>> Care to define what that you mean?
>>
>>> then there exists M_1(m) where m > n or m >> n,
>>> that is a halt decider for M_0(n).
>>
>> I'm not sure what role the subscripts 0 and 1 are playing here.  Also,
>> I'd urge you to be careful about terms like "X is a ..." when I think
>> you mean "X is any one of the class of ...".  It's OK provided everyone
>> is on board, but when things are new, extra care is sometimes needed.
>>
>>> How about that?
>>
>> With appropriate definitions, I feel sure sure one can do something like
>> that.
>>
>> Why are interested in such results?  Do they lead to some interesting
>> theory?
>>
>
> I think it's good the concept that the halting problem
> makes for an argument that "static analysis always halts".
>
> What I mean by that is relating it to something like Zeno,
> you show it doesn't go through, so show it never gets anywhere.
>
> So, showing completeness results first, then makes
> for that the student doesn't get left with the idea
> of "give up", instead "get over it", or "get through it".
>
> I.e. the idea is to make sure that there's completeness first,
> then, to forestall the feeling locked in with absence of
> free will or the conscious about it, instead, that incompleteness
> is sort of framed as about "there's asymptotic freedom",
> in a sense.
>
> Either way it's sort of liberating "my Turing machine can compute"
> or "the Turing machine can't compute me".  Here the idea is to
> make sure there's that "my Turing machine can compute", first,
> then "the Turing machine can't compute me" doesn't result
> "my Turing machine can't compute".
>
>
> Framing these kinds of things in universals and the infinite
> is sort of for "it's an open box", for the anxiety-prone of
> the claustrophobic sort, vis-a-vis the agoraphobe, fear of
> being closed in or wide-open spaces.  I.e. for not offending
> the sensibilities, is first for "here's the great part,
> it's closed, out through the unbounded, each is closed",
> you know, deterministic, then "here's the kicker:  it's open",
> so that then they can imagine it in the infinite.
>
>
>
>
> (Here the subscripts are just to indicate the generator
> and the instructions, about what populates the tape
> then what reads the tape.)
>
>
>
> (The, "epistemological antinomies" would probably relate
> to "non-logical/properly-logical paradoxes" meaning
> terms introduced above the logic, vis-a-vis "logical
> paradoxes", what are just any of the usual sorts class/set
> distinction issues like in set theory after expansion of
> comprehension into quantifier disambiguation.  Here for
> example the UTM has the monad of its state, it's sort of
> non-logical.)
>
>
> I'm only a practicing sort of corp enterprise software
> eng dev where UTM's are really academic, but formal languages
> about automata more generally like state-machines are real
> apropos, there are bounds, it's unbounded, then I usually
> sort of describe things "survey, audit, gap", in terms of
> "sensible, fungible, tractable".  Got to know your "Big O".
>
> I studied foundations for thirty years though and sort of
> have a combined approach about uncountability and logical
> paradox, though.  Like in my youtube videos or 10,000's posts
> to sci.math I demand that there are at least three continuous
> domains in mathematics, including line-reals [0,1], the
> complete ordered field as field-reals, and signal-reals,
> about the analytic construction, and their doubling/halving spaces.
> So, I would probably explore that first, ..., Zeno you know.
> Yet, that's my opinion.
>
> Like "today we're going to talk Halting Problem or Entscheidungs,
> Branching Problem.  Does anybody not know Zeno?  Has everybody
> got that Goedel has complete arithmetic then incomplete arithmetic?
> Cantor's Uncountability and the Diagonal or Anti-Diagonal?
> Alright, since we already have bounded-tape Turing machines,
> Halting Problem is about same as Goedel incompleteness."
>
> Otherwise I'd just kind of leave that out.  It's enrichment,
> vis-a-vis formal languages, accepter/rejector, automata,
> states, open/closed items, in time, these kinds of things.
>
> I'd make such notions more part of a survey in foundations
> or formal systems than formal languages and formal automata
> (defined, deterministic, and closed).
>
>
> Russell's Antinomy, Goedel's Incompleteness, the Halting Problem,
> Cantor's Paradox (the universe would be its own powerset),
> these sort of go together in "a survey of confounding results".

The key difference with Russell's Paradox is that they figured out
that they were thinking about the problem incorrectly and changed
how they thought about the problem to abolish the paradox.

ZFC prevents the existence of sets containing themselves. The same
approach can be applied to all self-reference paradox. I have been
focusing on self-reference paradox for twenty years.

*The halting problem <is> an instance of self-reference paradox*
*that a ZFC like solution will cure*

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

On 20/02/24 05:31, olcott wrote:
>
> The key difference with Russell's Paradox is that they figured out
> that they were thinking about the problem incorrectly and changed
> how they thought about the problem to abolish the paradox.
>
> ZFC prevents the existence of sets containing themselves. The same
> approach can be applied to all self-reference paradox. I have been
> focusing on self-reference paradox for twenty years.

So how do you think the halting problem should be redefined to make it
solvable?

On 2/19/2024 11:09 PM, immibis wrote:
> On 20/02/24 05:31, olcott wrote:
>>
>> The key difference with Russell's Paradox is that they figured out
>> that they were thinking about the problem incorrectly and changed
>> how they thought about the problem to abolish the paradox.
>>
>> ZFC prevents the existence of sets containing themselves. The same
>> approach can be applied to all self-reference paradox. I have been
>> focusing on self-reference paradox for twenty years.
>
> So how do you think the halting problem should be redefined to make it
> solvable?
>

There are at least two ways, one of these is consistent
with the way that the rest of the self-reference paradoxes
are solved. ZFC prevents sets that are members of themselves
from coming into existence. This abolished Russell's Paradox.

The analogous halting problem solution is to reject the
self-contradictory input.

This same thing applies to solving Tarski Undefinability.
Boolean(English, "This sentence is not true.")
Simply reject the input as invalid.

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

On 20/02/24 06:23, olcott wrote:
> On 2/19/2024 11:09 PM, immibis wrote:
>> On 20/02/24 05:31, olcott wrote:
>>>
>>> The key difference with Russell's Paradox is that they figured out
>>> that they were thinking about the problem incorrectly and changed
>>> how they thought about the problem to abolish the paradox.
>>>
>>> ZFC prevents the existence of sets containing themselves. The same
>>> approach can be applied to all self-reference paradox. I have been
>>> focusing on self-reference paradox for twenty years.
>>
>> So how do you think the halting problem should be redefined to make it
>> solvable?
>>
>
> There are at least two ways, one of these is consistent
> with the way that the rest of the self-reference paradoxes
> are solved. ZFC prevents sets that are members of themselves
> from coming into existence. This abolished Russell's Paradox.
>
> The analogous halting problem solution is to reject the
> self-contradictory input.
>
> This same thing applies to solving Tarski Undefinability.
> Boolean(English, "This sentence is not true.")
> Simply reject the input as invalid.
>

So what are the ways?

A Turing machine tape is defined to contain any sequence of symbols. You
want to change it so that a Turing machine tape contains any sequence of
symbols except for one that represents the input of a program to itself?

On 2/19/2024 11:34 PM, immibis wrote:
> On 20/02/24 06:23, olcott wrote:
>> On 2/19/2024 11:09 PM, immibis wrote:
>>> On 20/02/24 05:31, olcott wrote:
>>>>
>>>> The key difference with Russell's Paradox is that they figured out
>>>> that they were thinking about the problem incorrectly and changed
>>>> how they thought about the problem to abolish the paradox.
>>>>
>>>> ZFC prevents the existence of sets containing themselves. The same
>>>> approach can be applied to all self-reference paradox. I have been
>>>> focusing on self-reference paradox for twenty years.
>>>
>>> So how do you think the halting problem should be redefined to make
>>> it solvable?
>>>
>>
>> There are at least two ways, one of these is consistent
>> with the way that the rest of the self-reference paradoxes
>> are solved. ZFC prevents sets that are members of themselves
>> from coming into existence. This abolished Russell's Paradox.
>>
>> The analogous halting problem solution is to reject the
>> self-contradictory input.
>>
>> This same thing applies to solving Tarski Undefinability.
>> Boolean(English, "This sentence is not true.")
>> Simply reject the input as invalid.
>>
>
> So what are the ways?

A Halt decider recognizes and rejects self-contradictory inputs.
My code already does that.

>
> A Turing machine tape is defined to contain any sequence of symbols. You
> want to change it so that a Turing machine tape contains any sequence of
> symbols except for one that represents the input of a program to itself?

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

immibis <news@immibis.com> writes:

> On 20/02/24 00:38, Ben Bacarisse wrote:
>> Yes. There's an inherent problem here. We must show one actual
>> constructable counter-example, but that leads to the "just spot it"
>> avoidance issue. I would address that by giving simpler examples like
>> "no number is the largest".
>
> I seem to recall that Olcott avoided talking about the fact his style of
> "proof" that a halting decider exists also "proves" that a biggest natural
> number exists. So this example might not work either.

But I am talking about real students on a real degree course! Someone
like PO would fail the first year and my "Models of Computation" course
was a second year module!

But seriously. Try to stop thinking about PO. You may be new to the
game here but he's been posting junk for more than twenty years, and
what you see here is only the tip of his madness. He has claimed in a
court of law that he is god. What purpose is served by replying to him?

--
Ben.

Ross Finlayson <ross.a.finlayson@gmail.com> writes:

> On 02/19/2024 04:15 PM, Ben Bacarisse wrote:
>> Ross Finlayson <ross.a.finlayson@gmail.com> writes:
>>
>>> What about if M_0(n) is a Turing machine of finite bound n,
>>
>> Care to define what that you mean?
>>
>>> then there exists M_1(m) where m > n or m >> n,
>>> that is a halt decider for M_0(n).
>>
>> I'm not sure what role the subscripts 0 and 1 are playing here. Also,
>> I'd urge you to be careful about terms like "X is a ..." when I think
>> you mean "X is any one of the class of ...". It's OK provided everyone
>> is on board, but when things are new, extra care is sometimes needed.
>>
>>> How about that?
>>
>> With appropriate definitions, I feel sure sure one can do something like
>> that.
>>
>> Why are interested in such results? Do they lead to some interesting
>> theory?
>
> I think it's good the concept that the halting problem
> makes for an argument that "static analysis always halts".

Sorry, my mistake.

--
Ben.