In an axiomatic system, there are true statements, some but not all of which are provable. Is there any sense in which we can quantify the proportion of those statements that are true?
Here's an extremely simple way to look at the question: let $f_n$ be the proportion of all true theorems that can be expressed in $n$ symbols that is provable. What is $\lim_{n \rightarrow \infty}{f_n}$?
Has there been attempt to do something along these lines? I'm not asking whether anyone has actually calculated $f$ -- that surely hasn't been done -- but is there a theoretical framework in place for discussing this sort of question?
I am reorganizing my answer:
Here is an approach to forming an infinite sequence of distinct "true-but-unprovable" statements from Gödel’s original statement. Recall that Gödel created a statement about his axiomatic system which, from a higher level, means "This statement is unprovable." I will work on this intuitive level. My answer is necessarily incomplete since I am not providing the formal structure that is needed to map these higher-level meanings to axiomatic statements:
1) Gödel’s statement ("This statement is unprovable")
2) "This statement is not implied by 1, and 1 is true."
3) "This statement is not implied by any statement in the set $\{1,2\}$, and 2 is true."
4) "This statement is not implied by any statement in the set $\{1,2,3\}$, and 3 is true."
and so on.
Claim: All statements of this sequence are true-but-unprovable, and no statement is implied by any one of the previous ones (so all statements are distinct).
Proof: Suppose each statement in the set $\{1, ..., n\}$ is true-but-unprovable and is not implied by any one of its preceeding statements (this holds for $n=1$). We want to show this also holds for statement $n+1$.
Suppose statement $n+1$ is false (we reach a contradiction). This statement is:
(Statement $n+1$) "This statement is not implied by any statement in the set $\{1, ..., n\}$, and statement $n$ is true."
Since statement $n+1$ is false, we either have that it is implied by one of the previous ones, or statement $n$ is false. Since we already know statement $n$ is true, it must be that statement $n+1$ is implied by a statement $i \in \{1, ..., n\}$. But we already know statement $i$ is true. Since statement $i$ implies statement $n+1$, it must be that $n+1$ is true, a contradiction (so $n+1$ must be true).
Now that we have shown $n+1$ is true, it is easy to see that it is also true-but-unprovable (since if it were provable, it would prove statement $n$, which is not provable). Finally, since $n+1$ is true, it is not implied by any of the previous ones. $\Box$
Once you have an infinite sequence if distinct true-but-unprovable statements, you can list them and insert all the remaining true statements in your list in a sparse way. In this way, you can produce an ordering such that: $$ \lim_{n\rightarrow\infty} \frac{\mbox{Number of true-but-unprovable statements within the first $n$ statements}}{n} = 1 $$ (This of course is not the same way of defining the ratio as the way the asker of this question suggests). So, in this ordering, almost all true statements would be true-but-unprovable.
The following reference may be relevant. I only read the abstract, but the abstract indeed suggests that "almost all true statements are unprovable."
Calude and Jürgensen, "Is complexity a source of incompleteness?", 2005:
http://www.sciencedirect.com/science/article/pii/S0196885804001277