Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F.

So why can't you have a finite amount of Formal systems F2...FN that prove all the statements (or otherwise a considerable amount) which can't be proven within themselves?

If not doesn't this prove that some statements can't be proven at all under any formal systems?

Initially I thought this might be because F2 and F assuming consistency might be treated as one system and then therefore are incomplete much the same together.

I reasoned that this would then on the other-hand imply that there is a perfect formal system that proves as much as is feasible.

However this then made me think about the possibility of doing this with a weaker formal system and a stronger formal system (W1 and F), proving or otherwise simplifying the statements that F can't prove on its own. Why is this not feasible? To be precise I wondered why you can't combine formal systems without using them as a new formal system in this context? For example using W1 or F2 to prove statements in F (which F can't prove) without referring directly to F.

  • Welcome to SE Philosophy! Thanks for your contribution. Please take a quick moment to take the tour or find help. You can perform searches here or seek additional clarification at the meta site. Don't forget, when someone has answered your question, you can click on the checkmark to reward the contributor.
    – J D
    Commented Feb 1, 2020 at 3:20
  • 2
    Any statement can be made provable by making it an axiom. One can remove some axioms from F and then add some statements unprovable in F to get W1, but why bother with removing and not just add them to get a stronger F1? The problem is that one can only add finitely many statements this way while keeping F effectively axiomatizable. Otherwise, we could just pick any model of F and make every statement true in it an axiom.
    – Conifold
    Commented Feb 1, 2020 at 7:00

1 Answer 1


Short version:

No, this doesn't work.

First, note that you haven't stated Godel's theorem correctly - rather, it is:

Every consistent computably axiomatizable theory "containing enough arithmetic" is incomplete.

"Computably axiomatizable" here basically means that the theory isn't so complicated as to be impossible to describe; for example, taking a Platonist stance for simplicity the set of all sentences true about the natural numbers is consistent, complete, and trivially "contains enough arithmetic."

This won't become relevant until the end of my answer, but it's important to point out.

For simplicity, going forwards all theories are consistent, computably axiomatizable, and "contain enough arithmetic."

Every proposition can be decided in some theory. As a silly example, if p is logically invalid then it is disproved by the empty set of axioms, and if p is not logically invalid then {p} is a consistent set of axioms which proves p. Less stupidly, assuming (say) ZFC is consistent then one of ZFC+p and ZFC+~p is consistent, or both, and whichever is consistent clearly decides p.

(Note that it's that bolded case which is crucial here: if only one of ZFC+p and ZFC+~p is consistent, then ZFC alone decides p already.)

So that addresses one of your questions: "If not doesn't this prove that some statements can't be proven at all under any formal systems?"

Now let's look at what happens when we try to use multiple theories to circumvent incompleteness.

If we have theories T1, ..., Tn which don't disagree on anything, then their union T is also a theory to which Godel's theorem is applicable; the resulting Godel sentence g(T) is a fortiori undecidable in each of T1,...,Tn.

(Actually, as a technical point here we should use the Rosser sentence instead, but meh.)

What if we allow disagreement? Well, to start with this throws the whole idea into chaos - if there is disagreement between the Tis (say, T1 proves p but T2 disproves p) then it's hard to say how the collection of theories T1,...,Tn could fairly be said to decide anything - but it turns out that even allowing disagreement doesn't help:

If T1, ..., Tn are each theories to which Godel's incompleteness theorem applies (= consistent, computably axiomatizable, and containing enough arithmetic), then there is some sentence undecidable in each of T1,..., Tn.

(I've put this in giant font since I think it's really the most important result mentioned in this answer.)

This is surprisingly tricky to prove; a couple old answers of mine (1, 2) handle the case of two theories (the second dispenses with an unnecessary assumption used in the first), and the general case is messier but fundamentally the same. Specifically, the point is that we can't have a "consistency loop" where one theory proves the consistency of another theory which proves the consistency of yet another theory which ... which proves the consistency of the original theory, but if every sentence is decidable in one of our theories then such a "consistency loop" is impossible to avoid.

Finally, your statement

I reasoned that this would then on the other-hand imply that there is a perfect formal system that proves as much as is feasible

runs afoul of the computable axiomatizability requirement in Godel's theorem. Even ignoring the issue of finding a mechanism for picking the "right" theory deciding a given sentence which we haven't decided so far, we can't get around the problem that the union of infinitely many computably axiomatizable theories need not be computably axiomatizable.

It's at this point that computability theory becomes very relevant: it turns out that we can quantify how complicated a consistent complete theory containing enough arithmetic must be. The answer is technical, but the point is that this is something we can rigorously attack and develop a good understanding of.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .