Hacker News new | ask | show | jobs
by phs 356 days ago
So what is the richest logic whose proofs can be enumerated with only a five state TM?
2 comments

While that question depends on what you count as an 'enumeration', there's the related question of "What's the richest logic that cannot prove the halting status of all 5-state TMs?" That is, what's the richest logic that some 5-state TM's halting status is independent of?

I've pondered that version of the question a bit, but I couldn't get very far due to my lack of expertise in first-order logic. What I do know is that Skelet #17 [0] is one of the toughest machines to prove non-halting on a mathematical level [1], so any theory sufficient to prove that Skelet #17 doesn't halt is likely sufficient to decide the rest of the 5-state machines.

[0] https://bbchallenge.org/1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA

[1] https://arxiv.org/abs/2407.02426

That entirely depends on how you want to interpret a finite binary string as an enumeration of logic proofs?!