# What percentage of formulas is unprovable in a given axiomatic system?

I am trying to use language I am not familiar with, so bear with me. If I make no sense, I try to be clearer.

Assume we are given a formal language. Assume $S$ is the set of every well-formed formula that can be made in this language.

What is the cardinality of $S$?

I would assume that it is $\aleph_0$, because every statement is a result of finitely many parts, and if every symbol is given a natural number as representation and we take a formula and convert it to a natural number by pasting the numbers for symbols together, we always get a different natural number for every formula and we always stay within the naturals.

Assume we are given a set $A$ of axioms, ie. formulas that we assume to be true.

A formula is true if there is a finite sequence of axioms and other formulas that are true that imply the formula in question. If there is no such sequence, a formula is false. A given formula is either true or false.

A proof of a formula is a demonstration that such a sequence exists or doesn't exist.

We know that given any sufficiently powerful set of axioms, there are formulas that are unprovable, ie. there is no way within the axioms to show there exists a required sequence or that there is no such sequence.

As far as I know, continuum hypothesis is an example of such a formula.

I ask, given $A$, is there a way to estimate what percentage of formulas are unprovable?

If we add an independent axiom to $A$, how does the space of all formulas change? Does it reduce the number of unprovable formulas? Does it add to the number of unprovable formulas?

edit:

Let me add one final (independent) question. Is there a way to increase the number of axioms in such a way that all formulas will become provable?

-
If you add an independent axiom without changing the language, the set of unprovable formulas must decrease. So whatever probability notion we use, the probability of undecidability cannot increase. – André Nicolas Feb 20 '13 at 22:29
If the language is countable (the typical case,) then $S$ is countably infinite. The set of provable statements, the set of refutable statements, and the set of independent statements are all countably infinite as well. So an answer to this question would first require a notion of percentage for infinite sets. – Trevor Wilson Feb 20 '13 at 22:29
True. Both make sense. – Valtteri Feb 20 '13 at 22:31
You wrote that a formula is true if there is a proof of it from the axioms. But "true" is a semantical value, whereas you are looking for "provable". In a model of $\mathsf{ZFC+V=L}$ the continuum hypothesis is true, but there is no finite collection of axioms of $\mathsf{ZFC}$ which proves the continuum hypothesis. – Asaf Karagila Feb 20 '13 at 22:32
To add to Asaf's comment, your definition of "provable" should really be called "provably provable"---this is the same as "provable", but not the same as "true". – Trevor Wilson Feb 20 '13 at 22:35

You are correct that the number of well formed formulas is $\aleph_0$. The number of provable formulas (in PA, for example) is also $\aleph_0$, as all finite addition facts are provable and these are countably infinite. It is hard to define a percentage of formulas in this case.
Also the number of provably false formulas (take negations of provables) is $\aleph_0$. And (given a theory where Gödel applies) the number of unprovable formulas is $\aleph_0$. – Hagen von Eitzen Feb 20 '13 at 22:37