info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
Linz's proofs.
95 views
Skip to first unread message
Ben Bacarisse
Feb 19, 2024, 6:28:25 AMFeb 19
to
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.
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.
Andy Walker
Feb 19, 2024, 9:50:48 AMFeb 19
to
On 19/02/2024 11:28, Ben Bacarisse wrote:
[HP proofs:]
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
[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?
> 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.
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.
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
Ross Finlayson
Feb 19, 2024, 11:17:23 AMFeb 19
to
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.
olcott
Feb 19, 2024, 11:27:06 AMFeb 19
to
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
Mikko
Feb 19, 2024, 2:15:52 PMFeb 19
to
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
> Conversely, the classical proof by contradiction seems to lead a lot of
> non-mathematical students astray.
then M is not a halt decider for Turing machines.
--
Mikko
olcott
Feb 19, 2024, 2:36:11 PMFeb 19
to
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.
Ross Finlayson
Feb 19, 2024, 3:28:59 PMFeb 19
to
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.
olcott
Feb 19, 2024, 4:35:18 PMFeb 19
to
...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
undecidability proof...(Gödel 1931:43)
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.
Ben Bacarisse
Feb 19, 2024, 6:38:35 PMFeb 19
to
Andy Walker <a...@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.
> 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
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.
> 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.
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.
--
polcot2
Feb 19, 2024, 6:52:47 PMFeb 19
to
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....@bgtnsc04-news.ops.worldnet.att.net>
immibis
Feb 19, 2024, 7:06:39 PMFeb 19
to
> 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.
have no idea what this means and I am certainly not indoctrinated to
believe it.
Ben Bacarisse
Feb 19, 2024, 7:08:21 PMFeb 19
to
--
Ben.
Ben Bacarisse
Feb 19, 2024, 7:15:43 PMFeb 19
to
Ross Finlayson <ross.a.f...@gmail.com> writes:
> What about if M_0(n) is a Turing machine of finite bound n,
Care to define what that you mean?
> 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).
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.
immibis
Feb 19, 2024, 9:31:15 PMFeb 19
to
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
> 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".
"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.)
immibis
Feb 19, 2024, 10:09:00 PMFeb 19
to
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
> 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.
>
unrelated to Tarski's undefinability theorem, and "analytical truth
maker" is something you made up.
Richard Damon
Feb 19, 2024, 10:48:02 PMFeb 19
to
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
> 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.
>
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).
Richard Damon
Feb 19, 2024, 10:48:03 PMFeb 19
to
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.
Ross Finlayson
Feb 19, 2024, 11:20:27 PMFeb 19
to
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, ....
olcott
Feb 19, 2024, 11:31:38 PMFeb 19
to
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*
immibis
Feb 20, 2024, 12:09:08 AMFeb 20
to
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
>
> 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.
solvable?
olcott
Feb 20, 2024, 12:23:43 AMFeb 20
to
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.
immibis
Feb 20, 2024, 12:34:32 AMFeb 20
to
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?
> 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.
>
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?
olcott
Feb 20, 2024, 12:43:16 AMFeb 20
to
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.
> 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?
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?
Ben Bacarisse
Feb 20, 2024, 6:42:39 AMFeb 20
to
immibis <ne...@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
> 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.
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.
Ben Bacarisse
Feb 20, 2024, 6:44:00 AMFeb 20
to
Ross Finlayson <ross.a.f...@gmail.com> writes:
> On 02/19/2024 04:15 PM, Ben Bacarisse wrote:
>> Ross Finlayson <ross.a.f...@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.
> On 02/19/2024 04:15 PM, Ben Bacarisse wrote:
>> Ross Finlayson <ross.a.f...@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".
--
Ben.
Ben Bacarisse
Feb 20, 2024, 6:46:52 AMFeb 20
to
problem that is not the halting problem? What do you think you will
learn from him?
--
Ben.
Richard Damon
Feb 20, 2024, 7:34:31 AMFeb 20
to
Try to show how you can define a replacement for the definition of a
"Turing Machine" that doesn't allow the formation of that same problem.
The steps used to make H^ are basic fundamental steps, that no allowing
them means you break the power of the computation system.
Then you run into the issue that even if you somehow "ban" the contrary
action, there are still other (much more complicated) problem which can
be shown not to be computable, so you haven't actually fixed your issue.
Unless you totally destroy the power of computation, there will be
clearly definable problems that are not computable.
You are just proving your ignorance.
Mikko
Feb 20, 2024, 8:46:05 AMFeb 20
to
On 2024-02-19 19:36:06 +0000, olcott said:
> 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.
Tarski wrote to readers who do understand indirect proofs.
> 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.
--
Mikko
Mikko
Feb 20, 2024, 8:49:27 AMFeb 20
to
On 2024-02-19 20:29:13 +0000, Ross Finlayson said:
> 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?
Nothing about that before the non-solvability of the halting problem
> 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?
is unsderstood.
--
Mikko
olcott
Feb 20, 2024, 9:05:12 AMFeb 20
to
Boolean True(English, "This sentence is not true.")
When a correct and consistent truth predicate / halt decider
rejects self-contradictory inputs as invalid then as with
ZFC applied to Russell's Paradox the paradox is abolished.
olcott
Feb 20, 2024, 9:17:00 AMFeb 20
to
olcott
Feb 20, 2024, 9:21:48 AMFeb 20
to
inability to correctly answer self-contradictory questions
that are invalid input because they are self-contradictory.
Neither Tarski, Gödel nor Turing understood that self-contradictory
input is not in the domain of any Boolean decider.
Self-contradictory input is not a truth bearer thus has no
associated Boolean value.
Ross Finlayson
Feb 20, 2024, 1:04:43 PMFeb 20
to
tape is "infinite", or just "unbounded", then,
"what's on the tape" is usual matters of defining
infinite sequences.
The "definable" and these kinds of things, get into
notions like "every Cauchy sequence is definable,
but our language of defining words is countable,
how can it be that the language runs out but each
is defined", these kinds of things.
The only point there is "for any finite input,
for any finite program, there exists a static analyzer
or arbitrarily larger finite bounds, that answers
whether it halts".
It's like "that math is old, I want new math."
And it's like "math is discovered, not invented."
Then it's like, "I want to discover new math",
and it's like, "well, then you need to know what's old",
and it's like, "I just want to look smart",
and it's like, "get some glasses, read a book".
It's like, "that math is old, I want New Math",
and it's like, "no, you don't".
I'm sort of old and think that anything that
employs "ex falso quodlibet" that isn't specifically
bounded and that it's up-front that it's at best
quasi-modal, not having otherwise a modality or
being temporal or usual "classical quasi-modal logic",
in settings that would demand better than the quasi-modal,
this is thinking that that which employs EFW and material
implication, is unsuitable for usual results, which
must always have an edition of their results,
that uses direct implication only.
That's not to say I eschew intuitionism, far from it,
the very notions of deductive inference and abductive theory
very much are intuitionistic, but that's after and including
a very strong constructivism and structuralism.
I.e. "inexistence proofs via contradiction" and
"existence proofs without examples" are considered
on the sort of cusp of, redefinition, as it were.
Ross Finlayson
Feb 20, 2024, 4:53:56 PMFeb 20
to
"Will it shine?": Yeah.
You want it when?
immibis
Feb 20, 2024, 9:32:41 PMFeb 20
to
On 20/02/24 15:16, olcott wrote:
> On 2/20/2024 7:46 AM, Mikko wrote:
>> On 2024-02-19 19:36:06 +0000, olcott said:
>>
>>> 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.
>>
>> Tarski wrote to readers who do understand indirect proofs.
>>
>
> Do you understand that the Liar Paradox is neither true nor false?
Do you understand that the Liar Paradox is not a Turing machine, but
> On 2/20/2024 7:46 AM, Mikko wrote:
>> On 2024-02-19 19:36:06 +0000, olcott said:
>>
>>> 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.
>>
>> Tarski wrote to readers who do understand indirect proofs.
>>
>
> Do you understand that the Liar Paradox is neither true nor false?
H-hat is a Turing machine?
Richard Damon
Feb 20, 2024, 10:09:42 PMFeb 20
to
tyou don't understand what he is talking about.
It just shows that you think "Strawmen" are valid argument forms.
>
> When a correct and consistent truth predicate / halt decider
> rejects self-contradictory inputs as invalid then as with
> ZFC applied to Russell's Paradox the paradox is abolished.
>
we can prove that the "Liar" has a valid truth value.
Thus, since that can't be right, we can't have the existance of a valid
Truth Predicate.
Note, the ZFC rule can't be applied here, as the "problem" comes in via
to indirect of a path, and in effect, you would need to solve halting
(in the currect definition) to be able to reject you "invalid" inputs.
Richard Damon
Feb 20, 2024, 10:09:45 PMFeb 20
to
On 2/20/24 9:21 AM, olcott wrote:
> On 2/20/2024 7:49 AM, Mikko wrote:
>> On 2024-02-19 20:29:13 +0000, Ross Finlayson said:
>>
>>> 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?
>>
>> Nothing about that before the non-solvability of the halting problem
>> is unsderstood.
>>
>
> The unsolvability of the halting problem is merely the
> inability to correctly answer self-contradictory questions
> that are invalid input because they are self-contradictory.
>
> Neither Tarski, Gödel nor Turing understood that self-contradictory
> input is not in the domain of any Boolean decider.
>
> Self-contradictory input is not a truth bearer thus has no
> associated Boolean value.
>
Nope, as the actual quesiton isn't self-contradictory.
> On 2/20/2024 7:49 AM, Mikko wrote:
>> On 2024-02-19 20:29:13 +0000, Ross Finlayson said:
>>
>>> 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?
>>
>> Nothing about that before the non-solvability of the halting problem
>> is unsderstood.
>>
>
> The unsolvability of the halting problem is merely the
> inability to correctly answer self-contradictory questions
> that are invalid input because they are self-contradictory.
>
> Neither Tarski, Gödel nor Turing understood that self-contradictory
> input is not in the domain of any Boolean decider.
>
> Self-contradictory input is not a truth bearer thus has no
> associated Boolean value.
>
You are just showing your own ignorance.
The problem with your logic is that this says that some program
constructed by the fundamental rules of program construction, are not
"valid programs".
Thus, your logic creates a computation system that is no longer "Turing
Complete", but you are too ignorant to underastand what that means.
IF your H is an actual "Computation", then so is H^, and thus (H^) (H^)
is the description of an actual computation, and thus needs to be a
valid question.
Trying to define it otherwise, just breaks your logic, but you seem to
not understand things well enough to understand that fact.
Andy Walker
Feb 21, 2024, 7:00:00 AMFeb 21
to
On 19/02/2024 23:38, Ben Bacarisse wrote:
>> [HP proofs:]
>>> 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.
Well, it was only a tongue-in-cheek proposal. But someone controls
the syllabus and pre-requisites for any given module/course, and if these
are incompatible and the controller is not the teacher/lecturer, then there
is needs to be a discussion.
>> 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?
[As described in the module introduction, linked from the above
page] the students were 2nd-yr mathematicians. They would have had a
fairly short introductory programming module in the first year, and [by
the 1990s] would have had some IT at school. Many, perhaps most, would
have been experienced home-computer users.
> You may have misunderstood the reference to Minsky machines [...].
No, I meant that I was following, for this part of the module,
Minsky's "Computation". One of my favourite CS books, perhaps first-
equal with Dijkstra's "A Discipline of Programming".
>> There is still the problem that showing that something has
>> /a/ counter-example is not satisfying; [...].
infinity?", when the answer "infinity isn't a number" is just as not-
satisfying as the original problem and also depends on what sort of
number you're using, which gets us into some fairly deep maths [which
is what we were trying to avoid]. Likewise, "the largest number < 1"
invites debate about 0.999... and debate about the surreals [which
again takes us too far afield]. I don't have a Good Answer.
I do wonder whether there's some mileage in the "Surprise
Examination":
Version A:
Teacher: "There will be an exam at 11am one day next week, but which
day will be a surprise."
Bright students: "Well, it can't be on Friday, because if we get to
Thursday evening, we know the exam has to be Friday and it won't
be a surprise. So it can't be on Thursday either; if we get to
Wednesday evening, it has to be on Thursday and it won't be a
surprise. Similarly, it can't be on Wednesday, or Tuesday, or
Monday, so Teacher is lying."
Cometh Wednesday [or whichever] 11am, and the teacher sets the exam,
and the students are surprised, so Teacher told the truth.
Version B:
Teacher: "There will be an exam at 11am one day, but it will be a
surprise."
Class: "Well, it can't be at any bounded distance into the future.
So it's infinitely far away, so it won't happen, and Teacher
is lying."
Cometh Friday two weeks hence ....
Version C:
BenB: "This program will halt, but you can't tell when by the use of
any TM."
Student: "Well, it can't be after any bounded number of steps, so
the halt is infinitely far away, so it can't happen, and Ben is
lying."
Cometh [...] and Ben told the truth.
Comp.Theory: Unbounded debate about programs halting or otherwise.
--
Andy Walker, Nottingham.
Andy's music pages: www.cuboid.me.uk/andy/Music
Composer of the day: www.cuboid.me.uk/andy/Music/Composers/Liszt
>> [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.
Well, it was only a tongue-in-cheek proposal. But someone controls
the syllabus and pre-requisites for any given module/course, and if these
are incompatible and the controller is not the teacher/lecturer, then there
is needs to be a discussion.
>> 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?
[As described in the module introduction, linked from the above
page] the students were 2nd-yr mathematicians. They would have had a
fairly short introductory programming module in the first year, and [by
the 1990s] would have had some IT at school. Many, perhaps most, would
have been experienced home-computer users.
> You may have misunderstood the reference to Minsky machines [...].
No, I meant that I was following, for this part of the module,
Minsky's "Computation". One of my favourite CS books, perhaps first-
equal with Dijkstra's "A Discipline of Programming".
>> There is still the problem that showing that something has
>> /a/ counter-example is not satisfying; [...].
> 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".
You're in danger of running up against "But Sir, Sir, what about
> 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".
infinity?", when the answer "infinity isn't a number" is just as not-
satisfying as the original problem and also depends on what sort of
number you're using, which gets us into some fairly deep maths [which
is what we were trying to avoid]. Likewise, "the largest number < 1"
invites debate about 0.999... and debate about the surreals [which
again takes us too far afield]. I don't have a Good Answer.
I do wonder whether there's some mileage in the "Surprise
Examination":
Version A:
Teacher: "There will be an exam at 11am one day next week, but which
day will be a surprise."
Bright students: "Well, it can't be on Friday, because if we get to
Thursday evening, we know the exam has to be Friday and it won't
be a surprise. So it can't be on Thursday either; if we get to
Wednesday evening, it has to be on Thursday and it won't be a
surprise. Similarly, it can't be on Wednesday, or Tuesday, or
Monday, so Teacher is lying."
Cometh Wednesday [or whichever] 11am, and the teacher sets the exam,
and the students are surprised, so Teacher told the truth.
Version B:
Teacher: "There will be an exam at 11am one day, but it will be a
surprise."
Class: "Well, it can't be at any bounded distance into the future.
So it's infinitely far away, so it won't happen, and Teacher
is lying."
Cometh Friday two weeks hence ....
Version C:
BenB: "This program will halt, but you can't tell when by the use of
any TM."
Student: "Well, it can't be after any bounded number of steps, so
the halt is infinitely far away, so it can't happen, and Ben is
lying."
Cometh [...] and Ben told the truth.
Comp.Theory: Unbounded debate about programs halting or otherwise.
--
Andy Walker, Nottingham.
Andy's music pages: www.cuboid.me.uk/andy/Music
Composer of the day: www.cuboid.me.uk/andy/Music/Composers/Liszt
immibis
Feb 21, 2024, 7:34:48 AMFeb 21
to
problem so that it can be solved. How do you precisely modify the
problem to avoid the possibility of contradiction? Do you say that a
Turing machine tape can't contain a description of a "self-contradictory
Turing machine"? Do you limit the amount of memory?
immibis
Feb 21, 2024, 8:03:45 AMFeb 21
to
On 20/02/24 15:21, olcott wrote:
> On 2/20/2024 7:49 AM, Mikko wrote:
>> On 2024-02-19 20:29:13 +0000, Ross Finlayson said:
>>
>>> 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?
>>
>> Nothing about that before the non-solvability of the halting problem
>> is unsderstood.
>>
>
> The unsolvability of the halting problem is merely the
> inability to correctly answer self-contradictory questions
> that are invalid input because they are self-contradictory.
The unsolvability of the halting problem is merely the fact that the
> On 2/20/2024 7:49 AM, Mikko wrote:
>> On 2024-02-19 20:29:13 +0000, Ross Finlayson said:
>>
>>> 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?
>>
>> Nothing about that before the non-solvability of the halting problem
>> is unsderstood.
>>
>
> The unsolvability of the halting problem is merely the
> inability to correctly answer self-contradictory questions
> that are invalid input because they are self-contradictory.
halting problem is self-contradictory, and therefore unsolvable? Glad
you agree that the halting problem is unsolvable and therefore it cannot
be solved.
Mikko
Feb 22, 2024, 3:58:12 AMFeb 22
to
On 2024-02-20 14:16:55 +0000, olcott said:
> On 2/20/2024 7:46 AM, Mikko wrote:
>> On 2024-02-19 19:36:06 +0000, olcott said:
>>
>>> 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.
>>
>> Tarski wrote to readers who do understand indirect proofs.
>>
>
> Do you understand that the Liar Paradox is neither true nor false?
It does not matter what I understand.
> On 2/20/2024 7:46 AM, Mikko wrote:
>> On 2024-02-19 19:36:06 +0000, olcott said:
>>
>>> 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.
>>
>> Tarski wrote to readers who do understand indirect proofs.
>>
>
> Do you understand that the Liar Paradox is neither true nor false?
--
Mikko
olcott
Feb 22, 2024, 9:54:22 AMFeb 22
to
what I and others are saying about the halting problem then
understanding the Liar Paradox is a prerequisite.
0 new messages