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.
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.