On 2/24/2024 12:11 PM, Richard Damon wrote:
> On 2/24/24 12:50 PM, olcott wrote:
>> On 2/24/2024 11:46 AM, Ross Finlayson wrote:
>>> On 02/24/2024 12:22 AM, immibis wrote:
>>>> 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. 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.
>>>>>
>>>>
>>>> I have never read this sentence, it sounds like something he made up,
>>>> and I definitely haven't been indoctrinated to believe it. Nonetheless
>>>> the halting problem is obviously unsolvable.
>>>
>>> Consider a source-book like "approximation algorithms for NP-hard
>>> problems". Now, NP-hard problems would require NP resources,
>>> which for example, in the resource of time, might not exist.
>>> Yet, approximation algorithms both get a bunch of results,
>>> and, asymptotically solve the thing.
>>>
>>> So, is it solvable? Or maybe intractable?
>>>
>>> Now, there are some crossed wires in Olcott's approach it seems,
>>
>> On 2/23/2024 9:22 PM, Richard Damon wrote:
>>  > Yes, Epistemological antinomies, when given to a True Predicate, get
>>  > "rejected" in a sense, the predicate returns FALSE.
>>  >
>>  > That doesn't mean the statement is false, just that it isn't true.
>>  >
>>  > It also doesn't mean the predicate doesn't answer.
>>
>> Is my approach documented in this forum years ago.
>
> Nope. You have said what you want to change.

On 2/24/24 2:04 PM, olcott wrote:
> On 2/24/2024 12:11 PM, Richard Damon wrote:
>> On 2/24/24 12:50 PM, olcott wrote:
>>> On 2/24/2024 11:46 AM, Ross Finlayson wrote:
>>>> On 02/24/2024 12:22 AM, immibis wrote:
>>>>> 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. 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.
>>>>>>
>>>>>
>>>>> I have never read this sentence, it sounds like something he made up,
>>>>> and I definitely haven't been indoctrinated to believe it. Nonetheless
>>>>> the halting problem is obviously unsolvable.
>>>>
>>>> Consider a source-book like "approximation algorithms for NP-hard
>>>> problems". Now, NP-hard problems would require NP resources,
>>>> which for example, in the resource of time, might not exist.
>>>> Yet, approximation algorithms both get a bunch of results,
>>>> and, asymptotically solve the thing.
>>>>
>>>> So, is it solvable? Or maybe intractable?
>>>>
>>>> Now, there are some crossed wires in Olcott's approach it seems,
>>>
>>> On 2/23/2024 9:22 PM, Richard Damon wrote:
>>>  > Yes, Epistemological antinomies, when given to a True Predicate, get
>>>  > "rejected" in a sense, the predicate returns FALSE.
>>>  >
>>>  > That doesn't mean the statement is false, just that it isn't true.
>>>  >
>>>  > It also doesn't mean the predicate doesn't answer.
>>>
>>> Is my approach documented in this forum years ago.
>>
>> Nope. You have said what you want to change.
>
> On 2/23/2024 9:22 PM, Richard Damon wrote:
> > Yes, Epistemological antinomies, when given to a True Predicate, get
> > "rejected" in a sense, the predicate returns FALSE.
> >
> > That doesn't mean the statement is false, just that it isn't true.
> >
> > It also doesn't mean the predicate doesn't answer.
>
> Was documented as my solution to Epistemological antinomies,
> quite a few years ago in these same forums.
>