> Within the scope of mathematical logic, there’s a counterexample with Gödel’s first incompleteness theorem, which says that any theory sufficiently strong enough to model arithmetic contains a true sentence that’s not provable, called a Gödel sentence for the theory. The Gödel sentence is verifiable by its construction; however, it’s not provable from below.

I don't think this is a valid counterexample. The Gödel sentence is only verifiable from outside the theory, and you can prove it from outside the theory in the same way (e.g. with a large cardinal assumption for ZFC).

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.