This question is in response to one of the questions asked here. The OP wanted to know if the percentage of statements provable from ZFC tended to some value, and if so, what it was. In particular, the OP seemed interested in determining a possible asymptotic density:
$\lim_{n \rightarrow \infty} \frac{T(n)}{n}$
where $T(n)$ represents the number of statements provable from ZFC with Gödel number at most $n$ where the Gödel coding is bijective between the set of Natural numbers and formulas in the language of set theory. Of course, the Gödel coding should be computable in the sense that the set of the codes for the ZFC theorems should be semi-decidable. (i.e., We should be able to list the theorems of ZFC with a computer program.)
One problem that immediately comes to mind is the possibility that ZFC is inconsistent whereby all statements would be provable making the asymptotic density trivially have value 1. Another potential problem that I can see is the fact that the provability relation is computably enumerable but not computable (unless ZFC is inconsistent).
Therefore, let's fix a proof system and instead consider the function $T_n(n)$, which will represent the number of statements with Gödel number at most $n$ provable in at most $n$ lines from the finite collection of axioms of ZFC all having Gödel number at most $n$. The relevant question then seems to be:
What behavior does the function $T_n(n)/n$ exhibit for large $n$?
EDIT: Another problem pointed out by Chris and Carl is that we don't have a canonical numbering of the formulas. To try to salvage the meaningfulness of this question, let's fix a coding that corresponds to Gödel's original numbering. In this way, we assign each symbol a Natural number and encode a formula with $n$ symbols with respective codes $c_1, c_2, \ldots c_n$ from left to right as $\prod_{i=1}^n p_i^{c_i}$ where $p_i$ represents the $i^{th}$ prime. Then to ensure that the coding is bijective, compose this function with the one with domain of valid Gödel numbers sending the $i^{th}$ least code to $i$. Of course, the question is still dependent on the rules of inference of our proof system, but fix an accordingly natural one as well.
Best Answer
You can make $T_n(n)/n$ converge to any value you like by choosing a suitably silly Gödel numbering. Partition $\mathbb{N}$ (computably) into a set $A$ of density $p$, and set $B$ of density $1-p$, and an infinite set $C$ of density 0. Arrange your numbering scheme so that $A$ corresponds exactly to the ZFC axioms, $B$ corresponds to the negations of the axioms, and $C$ corresponds to all other statements. For this numbering, $T_n(n)/n$ tends to $p$.