News for hackers. Stuff that matters.

A comment on A pilot project in universal algebra to explore new ways to collaborate. Parent comment

Re:A pilot project in universal algebra to explore new ways ... by khafra on Friday September 27, 2024 @02:32AM (#41666989)
> There are no unsolvable problems with undecidability or busy beaver numbers.

Actually, if you encode the axioms of ZF into a TM, it's impossible to prove the machine will ever halt:

https://scottaaronson.blog/?p=2725

[ Parent | on HN ]
Re:A pilot project in universal algebra to explore new ways ... by srcreigh on Friday September 27, 2024 @02:52AM (#41667113)
That machine doesn’t encode ZF. It encodes a problem that is independent of ZF. And it’s not impossible to prove that the machine runs forever, you just can’t use ZF to prove that.
[ Parent | on HN ]