Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Gödel's Theorem says that I can construct a mathematical statement like "f(x1,x2,...,x_n)=0 has no integer solution", where it is impossible (in a certain system of axioms) to formally prove that it's true, and also impossible to formally prove that it's false.

I have often heard a school of thought that goes like "Well, in reality, we know that this particular statement is true. Why? Because if f has an integer solution, then it would obviously be possible to prove that f has an integer solution. (Plug it in and check it.) Yet I just constructed f in an elaborate way to ensure that no such formal proof exists."

Although this isn't a formal axiomatic proof that the statement is true, it is still a "proof" using meta-reasoning. (Is that a fair description?)

If this is correct so far, is there some generalization of Gödel's Theorem that says "There are statements which cannot be "proven" true, nor "proven" false, nor "proven" formally undecidable, even if the word "proven" is taken more broadly to allow any kind of "meta-reasoning" that mathematicians are capable of?

Makes my head spin to think about it. Thanks in advance!

share|improve this question
add comment

1 Answer

Yes, for most reasonable meanings of the words, there are statements that can neither be proved nor disproved nor proved to be independent.

However, "any kind of meta-reasoning that mathematicians are capable of" is slightly too fuzzy to work as a reasonable meaning here. Some mathematicians are capable of reasonings that other mathematicians consider faulty, for example.

Generally Gödel-like results always work particular proof systems, which are presumed to be "sane" in the sense that:

  • Any valid proof or disproof can be encoded as a sequence of bytes.

  • (Consistency): there is nothing that has both a proof and a disproof.

  • One can write a computer program that reads a sequence of bytes and then tells us whether it encodes a valid proof or disproof -- and if so, what it proves/disproves.

The last of these conditions fail if you try to make "provability" mean something non-operational such as "whatever will convince most real-life mathematicians". And it happens to be an essential technical part of the arguments.


One way to see there must be a sentence thar is neither provable nor disprovable nor provably independent is to consider all sentences of the form "$P$ halts" for all programs $P$ in your favorite programming language. If they are all either provable or disprovable, you could decide the halting problem by searching simultaneously for a proof and a disproof. So some of then (we don't know exactly which) must be neither provable nor disprovable. But if all of those could be proved independent, then we could solve the halting problem by searching simultaneously for a proof or a disproof or a proof of independendce. (If we know that the program's halting sentence is independent, then it cannot actually halt, because everything that halts does so provably).

share|improve this answer
add comment

Your Answer

 
discard

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.