Stepping back, what’s the ultimate point of all this? Traditional wisdom states that GSI and Löb’s theorem puts fundamental limitations on various formal logics preventing them from reasoning about themselves in a useful way. I no longer believe this to be the case. We can, with some cleverness, get these systems to do just that.
Taking the outside view (the traditional wisdom), I’d expect it more likely there’s some mistake here I’m not adept enough to identify or that it doesn’t actually grant you as much as you think it does. So I guess the question would be what the case is that others missed this and that you’ve discovered something novel?
(Note: asking this question in the spirit of starting a conversation. I didn’t have time to follow the math closely enough and I’ve been out of this sort of math for long enough that I don’t have a very informed opinion of what’s going on here, so this is mostly about poking to see what you think about this makes it different and exciting and likely to be useful.)
I do worry that there’s some technical subtlety not obvious until the end game that makes this particular construction impossible. I’ve been trying to spot some places where something might go wrong, and there are a few parts I don’t know how to fill in. I think there might be a problem relativizing a proof of the totality of ordinal multiplication which may prevent either the proof predicate relativization or the transfinite induction derivation from working. Or there may be some more subtle reason the steps I outlined won’t work. I was hoping that someone in the community might be able to say “I’ve seen this before, and it didn’t work because of XYZ”, but that hasn’t happened yet, which means I’ll probably have to attempt to formalize the whole argument to get a definitive answer, which I’m not confident is worth the effort.
Regardless, I don’t think my idea relies on this specific construct. The example from the beginning of the post that I find unsatisfying already sidesteps lob’s theorem, and just because I’m unsatisfied with it doesn’t mean it, or something equally as simple, isn’t useful to someone. Even if there’s a mistake here, I think the broad idea has legs.
Taking the outside view (the traditional wisdom), I’d expect it more likely there’s some mistake here I’m not adept enough to identify or that it doesn’t actually grant you as much as you think it does. So I guess the question would be what the case is that others missed this and that you’ve discovered something novel?
(Note: asking this question in the spirit of starting a conversation. I didn’t have time to follow the math closely enough and I’ve been out of this sort of math for long enough that I don’t have a very informed opinion of what’s going on here, so this is mostly about poking to see what you think about this makes it different and exciting and likely to be useful.)
I do worry that there’s some technical subtlety not obvious until the end game that makes this particular construction impossible. I’ve been trying to spot some places where something might go wrong, and there are a few parts I don’t know how to fill in. I think there might be a problem relativizing a proof of the totality of ordinal multiplication which may prevent either the proof predicate relativization or the transfinite induction derivation from working. Or there may be some more subtle reason the steps I outlined won’t work. I was hoping that someone in the community might be able to say “I’ve seen this before, and it didn’t work because of XYZ”, but that hasn’t happened yet, which means I’ll probably have to attempt to formalize the whole argument to get a definitive answer, which I’m not confident is worth the effort.
Regardless, I don’t think my idea relies on this specific construct. The example from the beginning of the post that I find unsatisfying already sidesteps lob’s theorem, and just because I’m unsatisfied with it doesn’t mean it, or something equally as simple, isn’t useful to someone. Even if there’s a mistake here, I think the broad idea has legs.