# In Godel's first incompleteness theorem the Godel sentence G is true otherwise it contradicts itself, however its truth implies it is not provable .

How can this be? I understand there are two basic definitions of truth in mathematics, one being the formalist definition which includes excluded middle and the second form being the intuitionist in which truth is based only on deductive provability. it just seems that informally if a theory is unprovable yet true, being able to explicitly state such a theory would constitute non trivial knowledge of a higher level of provability or computation?

• I always understood it so that $G$ is undecidable in the corresponding first order logic. You can add the negation of $G$ as an axiom and still have a consistent theory. It is only true in some "intuitive meaning", especially if you have a "standard model" of arithmetics in mind. (But I'm not an expert so I might be wrong) Aug 3, 2014 at 21:40
• @PeterFranek: See math.stackexchange.com/a/1873544/21820. Jul 29, 2016 at 6:49

When we say "true" about statements in the language of arithmetic, we often mean "true in the standard model". In general, "true" is a semantic property and a statement is true in a particular interpretation or it is false there. Without talking about a model, or a structure, the term "true" is utterly meaningless.

In the incompleteness theorem we construct a statement which is true in the standard model of the natural numbers, but does not have to be true in other models. And recall that as a first-order theory, Peano axioms have a myriad of different models.

Also if we stay with your awkward simplification, G's Incompleteness Th is no problem for intuitionism.

You are right in saying that for "the intuitionist [...] truth is based only on [...] provability", but this must not be read as "provability into a formal system".

G's proof is perfectly "sound" for an intuitionist : it shows "constructively" how to build up a formula of the formal system which is not provable in the system itself.

Thus, the proof of the existence of formulae unprovable in the formal system is intuitionistically "correct".

• Can you answer me this, can godel's proof only exist in an initial frame work of logic, containing another formal system, then his proof proves a statement in the later formal system? So really the proof is valid in the 'world system' for the contained formal system. but inharently that statement can not be proved inside of the contained formal system alone.? Mar 6, 2015 at 1:36
• If so I think this best helps explain my original question or rather misconception. Mar 6, 2015 at 1:37
• @marshalcraft - yes; in a sense, we can say that as well as for the "classical" mathematician G's Th proves that "mathematical truth" cannot be fully "captured" by a single formal system, so fo the "intuitionist" mathematician it proves that "mathematical knowledge" (acquired through proofs) cannot be fully captured by a single formal system. Mar 6, 2015 at 14:28
• Just to clarify I understand your answer, the statment g is not verifiable in intuitionist logic obviously however the fact that the statement g can be generated for any formal system complex enough to contain the integers is. Further that is the completeness theorem and it really doesn't concern formalism. the completeness theorems are still a problem and negative answer to hilbert's agenda in both formalist and intuition based lines of reasoning. May 9, 2015 at 4:43
• intuition based reasoning, merely would not require an finite or infinit enumerable set of axioms rather uses inclusion based upon it's provability, seemingly the next weakest method. May 9, 2015 at 4:46

You need to be very careful when you talk about truth. Usually it means true in the standard model. There will be nonstandard models where it is false. It is best to think about the incompletness theorems purely in terms of provability.