Sign up ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|cite|improve this question
See… –  David Speyer Dec 28 '10 at 14:42

2 Answers 2

up vote 18 down vote accepted

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$.

share|cite|improve this answer
+1, I was writing the same response. –  Carl Mummert Dec 28 '10 at 11:55
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
+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. –  Jason Dec 29 '10 at 1:02

I think if you order the formulas by increasing length, then the asymptotic density of the provable ones is zero. See:

share|cite|improve this answer
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. –  David Speyer Dec 30 '10 at 13:32
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
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. –  Jason Dec 31 '10 at 20:40

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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