Comment on A pilot project in universal algebra to explore new ways to collaborateparentComments−khafra1y 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−srcreigh1yThat 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.
Comments
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
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.