This question is in response to one of the questions asked here. The OP wanted to know if the percentage of statements provable from ZFC tended to some value, and if so, what it was. In particular, the OP seemed interested in determining a possible asymptotic density:

$\lim_{n \rightarrow \infty} \frac{T(n)}{n}$

where $T(n)$ represents the number of statements provable from ZFC with Gödel number at most $n$ where the Gödel coding is bijective between the set of Natural numbers and formulas in the language of set theory. Of course, the Gödel coding should be computable in the sense that the set of the codes for the ZFC theorems should be semi-decidable. (i.e., We should be able to list the theorems of ZFC with a computer program.)

One problem that immediately comes to mind is the possibility that ZFC is inconsistent whereby all statements would be provable making the asymptotic density trivially have value 1. Another potential problem that I can see is the fact that the provability relation is computably enumerable but not computable (unless ZFC is inconsistent).

Therefore, let's fix a proof system and instead consider the function $T_n(n)$, which will represent the number of statements with Gödel number at most $n$ provable in at most $n$ lines from the finite collection of axioms of ZFC all having Gödel number at most $n$. The relevant question then seems to be:

What behavior does the function $T_n(n)/n$ exhibit for large $n$?

EDIT: Another problem pointed out by Chris and Carl is that we don't have a canonical numbering of the formulas. To try to salvage the meaningfulness of this question, let's fix a coding that corresponds to Gödel's original numbering. In this way, we assign each symbol a Natural number and encode a formula with $n$ symbols with respective codes $c_1, c_2, \ldots c_n$ from left to right as $\prod_{i=1}^n p_i^{c_i}$ where $p_i$ represents the $i^{th}$ prime. Then to ensure that the coding is bijective, compose this function with the one with domain of valid Gödel numbers sending the $i^{th}$ least code to $i$. Of course, the question is still dependent on the rules of inference of our proof system, but fix an accordingly natural one as well.


2 Answers 2


You can make $T_n(n)/n$ converge to any value you like by choosing a suitably silly Gödel numbering. Partition $\mathbb{N}$ (computably) into a set $A$ of density $p$, and set $B$ of density $1-p$, and an infinite set $C$ of density 0. Arrange your numbering scheme so that $A$ corresponds exactly to the ZFC axioms, $B$ corresponds to the negations of the axioms, and $C$ corresponds to all other statements. For this numbering, $T_n(n)/n$ tends to $p$.

  • $\begingroup$ +1, I was writing the same response. $\endgroup$ Dec 28, 2010 at 11:55
  • 9
    $\begingroup$ Note that it's not quite any value, you need to start with a computable subset of $\mathbb{N}$ with density $p$ and an infinite complement. Given that, you can always find an infinite, coinfinite subset of the complement of density $0$ and carry out the construction. So this method only gives countably many values for $p$, but these are dense in $[0,1]$ and include $0$ and $1$. $\endgroup$ Dec 28, 2010 at 11:59
  • $\begingroup$ +1, I was thinking that the problem you mentioned was only relevant for decidable theories, but as you mention, you can always contain the statements that aren't trivially provable or refutable to have asymptotic density 0. I should have realized this. Also, Carl's point is subtle but important because we only have countably many computable functions. Anyway, one of the difficulties with this question that you show is the fact that there isn't a canonical numbering of the formulas. $\endgroup$
    – Jason
    Dec 29, 2010 at 1:02

I think if you order the formulas by increasing length, then the asymptotic density of the provable ones is zero. See: http://www.cs.auckland.ac.nz/~cristian/aam.pdf

  • 2
    $\begingroup$ Doesn't this run into the same obstacle as I brought up in the previous question? For every statement S, the statement "S or 1=1" is provable, and a positive density of all grammatical statements should be of this form. $\endgroup$ Dec 30, 2010 at 13:32
  • $\begingroup$ The post that David linked to suggests that the proof of this theorem may still be on shaky ground. But I'm confused about what is meant by ordering by increasing length because our language consists of an infinite set of variables. If by length $n$, we mean that we only allow the use of variables $x_1, \ldots, x_n$ as symbols, should $C_{n-k}/C_n$ be bounded away from $0$? $\endgroup$
    – Jason
    Dec 30, 2010 at 18:48
  • 2
    $\begingroup$ @Jason: that depends how you choose to set things up. You could go with a finite alphabet, containing symbols $x$ and $^'$, giving you infinitely many variables $x, x', x'', x'''$ etc. $\endgroup$ Dec 31, 2010 at 3:17
  • $\begingroup$ Good point, Chris. With all of these choices, I'm beginning to wonder whether we could defend any claim about a specific density as not being subject to arbitrary constraints. $\endgroup$
    – Jason
    Dec 31, 2010 at 20:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.