What can be said about collection of the unprovable formulas?

Question

From Godel's completeness theorem and incompleteness theorem, we can deduce that given certain nonlogical axioms, some unprovable formulas are true in some models of the axioms and false in others.

Let's consider the collection of such formulas, then what can we say about it? Is there any theory about that? Could you please point out any reference material on that? Any help is welcomed!

Answer 1

Theorem 5.2 in this paper by Calude and Jürgensen (2005), with my editing for clarity, states

Consider a consistent, sound, finitely-specified theory strong enough to formalize arithmetic. The probability that a true sentence of length $n$ is provable in the theory tends to zero when $n$ tends to infinity, while the probability that a sentence of length $n$ is true exceeds a positive quantity which is independent of $n$.