> But let's note that "undecidable" has a specific meaning here, that batches of logic axioms can't prove their own consistency
It's not actually that specific. There are many statements that we know are unprovable in ZF. ZFs own consistency is just one of them. The original work to find the 8000 state TM independent of ZF encodes an entirely different statement about graphs.
We are talking about finding TMs which encode a statement which is unprovable in say ZF. Specifically, the TM loops forever iff the statement (which is unprovable in ZF) is true. Not necessarily looking for inconsistencies Godel-style
It's not actually that specific. There are many statements that we know are unprovable in ZF. ZFs own consistency is just one of them. The original work to find the 8000 state TM independent of ZF encodes an entirely different statement about graphs.
We are talking about finding TMs which encode a statement which is unprovable in say ZF. Specifically, the TM loops forever iff the statement (which is unprovable in ZF) is true. Not necessarily looking for inconsistencies Godel-style