Hacker News Reader

You need to be a bit more specific: no matter what kind of true, computable axiom-set you're using (this has nothing to do with 'how much mathematics generally speaking develops'), there will be objectively true mathematical statements that can't be proven by that axiom-set.

>a disconnect between what's knowable and what's provable

"what's provable [from a given axiom-set]" is a concrete, technical, unambiguously defined set of things. "what's knowable" is a vague philosophical set of things. Goedel's Incompleteness Theorem is a technical result about the former, and it's a common mistake to assume it says anything about the latter, except very tangentially.

For those who are interested in the misty area where the two things do overlap, I will shamelessly plug this 2-page paper of mine, "Mathematical shortcomings in a simulated universe": https://philpapers.org/archive/ALEMSI.pdf

I think they meant what is true, which is also concrete, technical and unambiguously defined in this setting. But you are very correct to make the distinction between truth and knowledge. Pointing out that many philosophers have believed that knowledge is justified true belief might elucidate the relationship a bit.

> If that part of my understanding is correct, the part that's really interesting to me is whether we can know these true statements to be true, despite them not having proofs.

There may be proofs, just using different fundamental axioms. The finding is that there is no initial set of axioms that by themselves allow proving all provable truths.

You're thinking of his incompleteness theorems, not this completeness theorem for first order logic. My response to the parent covers both.