From Newsgroup: sci.logic

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.

actually i'm now thinking about using incompleteness against the
halting problem

How?

Which is what Incompleteness is about. It says that THE SYSTEM has a
true statement that THE SYSTEM can not prove. Doesn't matter that some
meta-system can prove it.

lol bruh, if there wasn't a meta system to prove it, how would godel
have proven it true outside the system???
at the very least godel's proof counts as a proof that exists outside
the system

G||del's proof is in the system of ZFC or whatever. It says something
about another formal system and its metasystem. Those may all be
different.

There is an additional proof that shows that while some of these
statements can be proved is some meta-system of the system, there will
always be some that can't be proved at any finite level of meta-system.

--
Am Sat, 20 Jul 2024 12:35:31 +0000 schrieb WM in sci.math:
It is not guaranteed that n+1 exists for every n.
--- Synchronet 3.21a-Linux NewsLink 1.2

From Newsgroup: sci.logic

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 4G, 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 halting/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.

--- Synchronet 3.21a-Linux NewsLink 1.2