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 

>$S$, or $1=1$

is a theorem. So the number of provable statements of length $n$ is bounded below by $C_{n-k}$, 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

>Either $S$ and $1 \neq 1$, or else $G$

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_{n-k}/C_n$ and $C_{n- \ell}/C_n$ should both be bounded away from 0.

My computation is seemingly incompatible with the [paper of Calude and Jurgensen][1] cited by [Konrad][2]. I sent some time trying to figure out why and my view is that I am right and Calude and Jurgensen are wrong but, of course, I could be doing something dumb.

<hr>

This answer is getting discussed again, so let me mention a way that one might be able to salvage this, though. There is extensive literature on the behavior of random boolean statements, of which the most common model is "random $3$-SAT". The way that this works is that you have $n$ boolean variables $x_1$, $x_2$, ..., $x_n$. A "three-term clause" is a statement of the form $p_1 \vee p_2 \vee p_3$ where each $p$ is either $x_i$ or $\neg(x_i)$ for some $i$. One samples $k$ of the three-term clauses independently at random and asks whether they can all be satisfied at once. Generally, one takes $k = cn$ for fixed $c$ and asks about behavior as $n \to \infty$.

When I first heard this problem, my intuition was that the probability would be bounded away from $1$, for the same sort of reason as this answer: Some positive density of $3$-SAT instances would be of the form $P \wedge Q$, where $P$ was some explicit finite list of incompatible $3$-term clauses. (For example, $P$ could be the AND of the eight $3$-term clauses involving $(x_1, x_2, x_3)$.) But this is wrong! Because all of the $n$ variables are equally likely, for any finite number of $3$-term clauses, the probability that they will have any variables in common goes to $0$. 

The flaw in this answer's argument, when it comes to random $3$-SAT, is the following: Because the size of our alphabet is allowed grow with the length of the statement, the number of $3$-SAT instances with $cn$ clauses and $n$ variables grows like $n^{3cn}$, not like an exponential! It is actually really important whether writing down "$x_i$" counts as $O(1)$ characters, or as $O(\log i)$ characters!

So this makes me wonder whether some similar phenomenon might occur for decidability in first order logic. I dug around a little, but I couldn't find any research.


  [1]: http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B6W9D-4F9F850-2&_user=501045&_rdoc=1&_fmt=&_orig=search&_sort=d&_docanchor=&view=c&_acct=C000022659&_version=1&_urlVersion=0&_userid=501045&md5=dde512d656cc98a3a5a0c7819de84cf9
  [2]: https://mathoverflow.net/questions/4454/how-many-of-the-true-sentences-are-provable/7856#7856