We know from Gödel's First Incompleteness Theorem that there are true statements in the natural numbers that have no proof. Obviously we know of many that do ("theorems").
Are results known about the relative sparsity of these two sets? For instance, perhaps one could order statements by the number of characters N, and look at true statements. Do we know if "most" true statements are theorems, or the opposite, and does the fraction depend on N? Are Gödel's examples rare jury-rigged freaks, or do they actually become the rule?

  • 2
    $\begingroup$ Related: mathoverflow.net/questions/421707/… and math.stackexchange.com/questions/1491438/… $\endgroup$ Commented Jun 1, 2022 at 1:34
  • 2
    $\begingroup$ Also see cs.auckland.ac.nz/~cristian/aam.pdf $\endgroup$ Commented Jun 1, 2022 at 1:52
  • 2
    $\begingroup$ I left an answer a long time ago arguing that, under any reasonable grammar, a positive density of sentences are of the form "1=1 or S", and are therefore provable mathoverflow.net/a/7902/297 . I wish someone would explain to me how my model differs from Calude and Jurgensen's. $\endgroup$ Commented Jun 1, 2022 at 2:09
  • 2
    $\begingroup$ Of course, the answer there basically says that the space of true sentences is filled with a lot of junk. Doesn't help with what we'd "really" like to know - "real" theorems vs. distinct true statements w/o proofs. Hmm. $\endgroup$
    – Mike Arrh
    Commented Jun 1, 2022 at 2:43
  • 1
    $\begingroup$ @DavidESpeyer As Konrad pointed out in your previous answer, I think there's just an error in the Calude-Jurgensen proof - what they actually prove (in the proof of Theorem 5.2 on p.11) is that "the probability that a random string of $n$ logical symbols represents a provable sentence $\to 0$", so they are not conditioning this string being a well-formed grammatical sentence. $\endgroup$ Commented Jun 1, 2022 at 6:14


Browse other questions tagged or ask your own question.