Probabilistic "proof" that a sentence is provable (proof "density"). Is it possible to (or even useful) to calculate the probability that a certain statement is provable?
I had this idea that any two statements say A and B could be compared to each other by comparing the probability that either of them has proof. 
Given a sentence $\varphi$ in the theory and a statement $A$, let $P_A(\varphi)$ be defined to equal $1$ if $\varphi$ is a proof of $A$ and $0$ otherwise. let $|\varphi|$ denote the length of the sentence $\varphi$ and consider the limit:
$$D(A) =\lim_{n \to \infty} \frac{\sum_{|\varphi| <n} P_A(\varphi)}{n}$$
If $A$ is unprovable then $D(A) = 0$. (maybe $n$ should be replaced with $n!$ or other function of $n$ to make this calculation meaningful)
The preceding construction can work only if $A$ is known to be provable (otherwise the calculation would prove that it is provable or unprovable). So this is the method i have in mind:
Suppose we we’re given a statement $B$ and asked if it's provable. First we assume $B$ is provable. Then we carry out the calculation of $D(B)$. 
Now if $D(A) < D(B)$ we can say something like: "$B$ is probably true".
Where are the potential faults in this construction? Where are the (logically) impossible steps?
 A: In principle you could compare the probabilities of sentences being theorems, if the set of axioms you're allowed to prove things from is random.
However, once the axioms are fixed, your sentence either is a theorem or isn't. There's nothing random about it, and hence speaking about probabilities is pointless.
A: For the revised question:
You probably want the denominator in your definition of $D(A)$ to be "the number of symbol strings of length $n$", which could be something like $2^n$ or $26^n$ depending on exactly which kind of formal proofs you're working with.
Then $D(A)$ becomes the limiting density of proofs of $A$ among all symbol strings, if the proof system is not completely crazy, $D(A)$ will be $0$ exactly when $A$ is not provable. If $A$ is provable, then I think $D(A)$ will be positive, but it's not completely trivial to exclude the possibility that the limit doesn't exists at all.
The main problem with your plan is now that you say "carry out the calculation of $D(B)$", when you have not in fact specified a calculation that can be carried out. What you have is a definition of $D(-)$, but it's not effective -- even in principle you can't just plug in a formula and crank the handle to get a precise answer in finite time. The limit depends on infinite many values of the fraction, which you don't have time to calculate all of.
If the proof system is consistent and otherwise sane, $D(A)$ is uncomputable as a function of $A$, and it feels very likely to me that for every provable $A$ the exact value of $D(A)$ is in fact independent of ZFC.
It is certainly true that $D(A) < D(B)$ implies with certainty that $B$ is provable and therefore true. But this is not a very useful fact -- since we cannot compute $D(B)$ explicitly, the only way to establish $D(A)<D(B)$ is to show that $A$ is not provable but $B$ is -- and then your observation tells us nothing we don't already know.
