How common (dense) are undecidable propositions in Peano Arithmetic?

Question

Godel, Turing Rosser et al proved they exist.
Are they more like the primes, infinite in number, but getting rarer and rarer as you go along? (Consider larger and larger propositions?)
Or are they more like the composites, becoming more and more dominant? Or don't we know? Does it make a difference if we use ZF instead of PA?
References would be greatly appreciated.

Answer 1

There is an analogy between undecidable propositions and computer programs which do not halt. The density of halting programs is called Chaitin's constant (see http://en.wikipedia.org/wiki/Halting_probability ), and it is a transcendental number; in particular it is neither 0 nor 1, so both the halting and the non-halting programs make up positive proportions of the set of programs. I couldn't tell if those results can be directly transferred to propositions in PA, but it's worth a look.