Not sure what work “necessarily” is doing, but mostly I’m with you. Still, I think this is mistaken:
I’ll just say that Provable(X) doesn’t imply Provable(Provable(X)), and if you think it does, it’s because your ontology of mathematics is wrong and Gödel will eat you.
Though it is true and important that Unprovable(X) does not imply Provable(Unprovable(X)).
Not sure what work “necessarily” is doing, but mostly I’m with you. Still, I think this is mistaken:
Though it is true and important that Unprovable(X) does not imply Provable(Unprovable(X)).