You're right that this doesn't work. I seem to have thought of verifiability as provable from outside the theory and discoverable as provable from inside the theory. This clearly doesn't get at what Greg is arguing.

Thanks for pointing this out! I'll update the post.

I'm now not sure what's the distinction between verifiability and discoverability among truths in a formal system.