Is there a natural measure on the set of statements which are true in the usual model (i.e. $\mathbb{N}$) of Peano arithmetic which enables one to enquire if 'most' true sentences are provable or not? By the word 'natural' I am trying to exclude measures defined in terms of the characteristic function of the set of true sentences.

It seems to me that the probability that a statement is provable and that it is undecidable should both be bounded away from 0, for any reasonable probability distribution. Let $C_n$ be the number of grammatical statements of length $n$. For any statement $S$, the statement
is a theorem. So the number of provable statements of length $n$ is bounded below by $C_{nk}$, where $k$ is the number of characters needed to tag on "or $1=1$". On the other hand, let $G$ be an undecidable sentence, and $S$ any sentence. Then
is undecidable. So the number of undecidable sentences of length $n$ is bounded below by $C_{n\ell}$, for some constant $\ell$. For any reasonable grammar, the ratios $C_{nk}/C_n$ and $C_{n \ell}/C_n$ should both be bounded away from 0. I am currently trying to figure out why my computation is seemingly incompatible with the paper of Calude and Jurgensen cited by Konrad. I suspect that the answer is hidden in the definition of prefix free, on page 4, but I am trouble understanding it. Any help? 


Update: in response to comment below, I'm not sure anymore the probability in question was 0. Let's try the measure that gives an equal weight for any true statement of fixed length $N$ (written in mathematical English). Then we have statements of the form "S or 1+2=3" which form more then $1/10^{20}$th of all true statements of a given length. On the other hand, the statements "S and Z" (where So, yes, for the measure described above the measure of provable statements is within some positive bounds $[a, b]$ for any $N$ greater than some $N_0$. But that measure is proportional, for a fixed $N$, to the characteristic function of the set of all true statements, so, no, my answer doesn't give a "natural" measure. I think the probability of "a random true statement is provable" is 0 in any good formalization of your problem. Here's the reasoning: consider a true undecidable statement
The proof can be done by considering the random strings of the form (chunk 1)(chunk 2)...(chunk 


Ilya had the right idea in his answer. Firstly, the natural measure that is usually used when you have a discrete set of objects, each of some finite "complexity" n, and with only finitely many of complexity n, is to consider the probability for fixed n, and then let n go to infinity (cf. the theory of Random Graphs). Secondly, the probability of a true statement of length n being provable indeed tends to 0 as n goes to infinity. This has been shown by Cristian Calude and Helmut Jürgensen (Adv Appl Math 35 (2005), 115). Thank goodness our job is not to prove random statements! Caveat: this holds for sound and consistent theories in which Peano arithmetic can be formalized. 


There are an infinite number of true provable theorems in PA and an infinite number of true unprovable theorems. So any measure must go to zero for all but a finite number of sentences I think there will be a problem with knowing p in that one can search all the lower weighted sentences and find the percentage of true sentences so that a point may be reached where some sentences may have to be undecidable to make the probability work. If this is the case then then knowledge of the probability would make some sentences decidable so the probability can't be known and the proof would have to be nonconstructive that it exists which could cause problems with some philosophies of mathematics like intuitionism. I recall a similar question about quantum computers in which the answer was 1/2. I have found a reference that says that no halting probability is computable. If proof could be made into a process that either succeeds or never halts then that would provide evidence that the probability of an undecidable theorem is uncomputable http://en.wikipedia.org/wiki/Chaitin%27s_constant#Interpretation_as_a_probability 

