I'm not a logician, but I think the question (a good one) is not quite well-posed. As I understand, in mathematical logic, a statement being provable means one can deduce it from a set of axioms. If you have a set of axioms A sufficiently powerful for Godel's construction to go through, the resulting Godel sentence s is (by construction) not provable from A, but one can always make it provable by appending s to the axioms A.
For a statement to be true, on the other hand, has a technical meaning: it means that there is a model (in the sense of model theory, see https://en.wikipedia.org/wiki/Model_theory ) in which both the axioms A and the sentence s are true. Godel's completeness theorem (https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th...) asserts that s is provable from A if and only if s is true in every model in which A holds.
Yet first order logic encompasses 99.9% of the mathematics anyone ever does, even professional mathematicians. The only people who consider anything but first order logic are people who have gone out of their way to make a point to study it just for its own sake. When the general subject of discussion is proof assistants and proofs in normal mathematics, I don't think it's necessary to constantly mention "only in first order logic". It's like discussing structural integrity of a building and constantly mentioning that all the calculations only hold on in our reality, but if we were living in an alternate dimension and the physical constants of the universe were different then the results wouldn't be applicable.
>Yet first order logic encompasses 99.9% of the mathematics anyone ever does, even professional mathematicians.
I'm way out of my depth here, but I'm curious about this statement. In first order logic you can't even assert that the natural numbers cannot be put into a one-to-one correspondence with the real numbers, which seems like a fairly basic mathematical fact.
Right, but you can't ensure that the only models of 'bijective functions' are actually bijective functions. To switch to a slightly simpler example, you can translate statements such as "x is finite" into a first order language (for example, set theory), but you can't ensure that x actually is finite in the models of this statement.
To your first point: yeah, some discomfort around it is valid, but I see it as a non-issue. Informally/philosophically, because a model's job is to capture everything a first-order theory can see about your object of study - so it's fine for (say) an "actually" countable set to model the reals, and not be up to the task of "actually being" the reals. Formally, you differentiate between internal and external statements and don't expect them to be the same (a rigorous version of my pretentious use of scare quotes above :).
It might be helpful to be a bit more precise here.
The expression "first-order logic" (FOL) is a bit vague. Do you mean
pure FOL (i.e. all axioms are about equality) or FOL plus additional
axioms? Pure FOL (without additional axioms) is indeed rather weak
and cannot be used for much. That's why mathematicians build a
foundation of mathematics on top of FOL by assuming the truth of
additional axioms.
The most well known foundation of mathematics built on top of FOL is
ZF-set theory which adds about a dozen additional axioms about how to
construct new sets from old, and when two sets are equal.
There are other FOL-based axiomatisations of mathematics such as Quine's NF, or
category theory (which can be expressed as a theory on top of
FOL). There are also foundations of mathematics that are not using FOL
(Martin-Loef type theory and successors such as HoTT).
Goedel's first incompleteness theorem forces all those axiomatisations
of mathematics to be incomplete, meaning there are formulae A such
that neither A nor the negation of A can be derived.
A statement like "99.9% of the mathematics anyone ever does" is about
FOL extended with foundations of mathematics like ZF, or a
type-theoretic equivalent.
However, mathematicians are getting ever better at producing
interesting formulae whose truth (or otherwise) cannot be settled in
ZF (or similar) [1]. In order to deal with such expressivity gaps,
mathematicians investigate more powerful axioms, called "large
cardinals", which claim the existence of certain extremely large sets.
You can also think of them as more powerful induction principles.
The problem with inventing new large cardinals (i.e. more powerful
induction principles) is to navigate between the Scylla of expressive
weakness (the axiom is a consequence of other axioms) and the
Charybdis of inconsistency (adding the axiom allows us to derive
"false").
For a statement to be true, on the other hand, has a technical meaning: it means that there is a model (in the sense of model theory, see https://en.wikipedia.org/wiki/Model_theory ) in which both the axioms A and the sentence s are true. Godel's completeness theorem (https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th...) asserts that s is provable from A if and only if s is true in every model in which A holds.