From: news.dead.person.stones@darjeeling.plus.com   
      
   On 30/12/2025 09:47, joes wrote:   
   > Am Mon, 29 Dec 2025 23:26:15 -0800 schrieb dart200:   
   >> On 12/29/25 5:37 AM, Richard Damon wrote:   
   >   
   >>> I believe there is then another proof that shows that because there is   
   >>> no decider that gets all inputs correctly, you can show that there must   
   >>> be some program that no known to be corret partial decider gets right,   
   >>> in other words, a program that we can not know its halting status, as   
   >>> we can not prove it will not halt.   
   > I believe not, but I would be delighted to see.   
   >   
      
   Problem:  what is a "known to be correct" decider?  And what if we don't know   
   a decider is correct   
   today, but tomorrow we prove that it is in fact correct?   
      
   Then Richard suggests that is equivalent to a program that we *can not* know   
   its halting status, but   
   these two ideas are not the same - the first is a point-in-time statement, and   
   the second tries to   
   be absolute.  Possibly the first statement was also intended to be absolute.   
      
   I don't see how we can make absolute statements about what is "knowable".  It   
   doesn't seem to be a   
   mathematical idea.  It's like the G sentence in a formal theory like PA   
   (Peano's axioms of   
   arithmetic) - PA proves neither G nor ¬G, but that doesn't imply the truth of   
   G is "unknowable" in   
   any absolute sense.  In fact, most mathematicians would take the natural   
   numbers as being a model of   
   PA, in which case we can see that G must be true.  To say that some arithmetic   
   statement is   
   unknowable in some absolute sense, surely we would need to define /exactly/   
   what it is possible to   
   "know" and why.  Otherwise who is to say that we will not have some new   
   insight into the nature of   
   the natural numbers, which renders new arithmetic statements provable?  (i.e.   
   we accept new axioms   
   into our existing framework, which lead to resolving problems we were   
   previously stuck on.)   
      
   If the claim is just that one fixed formal system cannot prove h   
   lting/nonhalting for all TMs, that   
   seems clear enough (i.e. that statement being correct).  E.g. given a TM M, we   
   could form the   
   statements in our formal system that M halts, and that M never halts.  If our   
   formal system can   
   prove one or the other of these, we can write a program to enumerate all   
   theorems of the system   
   until we hit a proof for M halting, or M never halting.  We can argue that we   
   have now created a   
   universal halt decider, which is a contradiction etc..  (So there must be some   
   machine M our system   
   cannot decide...)   Well, assuming we have confidence in the soundness of our   
   formal system I guess...   
      
   Anyway, we have entered a /much/ trickier domain, since we're no longer just   
   interested in halt   
   deciders, but /provability/ of halting, and even what it means for something   
   to be ultimately   
   "knowable" by the human mind which is not some /fixed/ formal system.  (Hehe,   
   unless you want to   
   claim the whole universe is one giant TM computation perhaps!)   
      
      
   Mike.   
      
   --- SoupGate-DOS v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)