# Asymptotic density of provable statements in ZFC

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.

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$.
• 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$. – Carl Mummert Dec 28 '10 at 11:59
• 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$? – Jason Dec 30 '10 at 18:48
• @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. – Chris Eagle Dec 31 '10 at 3:17