Is there a useful measure of density of decidable sentences in PA?

Question

Essential undecidability of PA says every complete extension of PA includes a non r.e. set of new "axioms," all undecidable in PA.  In that sense lots of sentences of PA are undecidable in PA.  And it is trivial to design a measure on, say sentences of PA with Godel number below $n$, where the set of decidable sentences has measure 1 (for all $n$ above the Godel number of the first decidable sentence, which would be 0=0 for the usual Godel numberings).  Just take the counting measure while restricting the count to decidable sentences.  Similar cheap tricks will give other uninformative results. 

But is there a useful, nontrivial way to define the density of decidable sentences in PA? 

The answer seems to be the state of the art.  It has nothing special to do with PA of course.  It holds for any incomplete theory, just using any theorem in place of $0=0$ and any refutable sentence in place of $0=1$. Chaitin's "heuristic principle" uses complexity to suggest that in fact almost all true sentences are independent in any recursive extension of PA, as cited in discussion of How many of the true sentences are provable? But people do not seem persuaded by this.

Answer 1

Asymptotic density seems a very natural measure. The density of a set of sentences is the limit as $n\to\infty$ of the proportion of those sentences of length at most $n$ amongst all sentences of length at most $n$.

(One should use a formalism that has only finitely many sentences of a given length—for example, one can use variable symbols $x$, $x'$, $x''$, and so on, where the prime counts as another symbol, instead of indices; or else just stratify the sentences as a union of finite sets, such as by Gödel codes.)

Having density 1 means that as one considers longer and longer sentences, the proportion of them in the set goes to 100%. Having density 0 means that as one considers longer and longer sentences, the proportion of them in the set goes to 0.

We similarly get a notion of lower density and upper density by using $\liminf$ and $\limsup$.

Using this measure, it turns out that the set of theorems, the set of refutable sentences, and the set of independent sentences (over some fixed theory) all have a lower density bounded away from zero and an upper density bounded away from 1.

For example, every sentence of the form $\varphi\vee( 1=1)$ is a theorem, and this is a positive density set. Every sentence of the form $\varphi\wedge (1=0)$ is refutable, and this is a positive density set. And every sentence of the form $(\varphi\vee (1=1))\wedge\psi$ is independent, where $\psi$ is some fixed independent sentence, and this also is a positive density set.