# Is the negation of the Gödel sentence always unprovable too?

The incompleteness theorem says that certain theories+deduction system contain at least one sentence (the Gödel sentence "$G$"), which can't be proven (in the system in which it holds).

(i) Is this theorem (incompleteness theorem) a statement formulated within the system of which the statement is about or is the theorem formulated in a meta language?

(ii) As soon as the theorem is established, is there readily the implication that "$\neg G$" is also not provable? And again, is this then a statement of the meta language?

(iii) In case that a mega language is crucial, what are the minimal requirements for it's logic?

(The thread here, "Is it always possible to decide if either a statement or its negation is provable in a given axiomatic system?" is related.)

For me this question is kind of a follow up to Aftermath of the incompletness theorem proof. I don't understand the notion of "A sentence $p$ is true in $\mathbb{N}$" if $p$ is neither an axiom nor provable by a deduction system. My ansatz was to establish "$G$ not provable","$\neg G$ not provable" while $G\lor\neg G$ is true, which would directly imply that one of them ($G$ or $\neg G$) is proven to be true and not provable in the investigated system. If the proposed conditions are always satisfied for the Gödel sentence and the meta language, then I could comprehend the formulation "it's true but unprovable", because "true" wouldn't come from outside.

• (i) The unprovable statement in is within the system, the unprovability is within the meta-system. (ii) Yes, that's the idea. Unprovable statements whose negation is provable are trivial to obtain "$\exists x: x\neq x$." – Michael Greinecker Aug 15 '12 at 19:04
• Isn't the point of the Gödel sentence that it can't be assigned a truth value? Assigning a truth value to $\neg G$ would also assign one to $G$. – axblount Aug 15 '12 at 19:05
• In fact, any statement of the pure form '$X$ is not provable' can only be proven by a metasystem, because a statement's unprovability implies the consistency of the original system (an inconsistent system will gladly prove anything), and so by Godel's second cannot be shown within the system. Instead, the canonical way of internally formulating unprovability is '$\mathrm{Con}(S)\implies \neg B_S(G)$', where $B_S$ is the provability predicate for the systrem $S$. – Steven Stadnicki Aug 15 '12 at 19:13
• @MichaelGreinecker: Okay, that should answer (i). I don't get why you bring the example for (ii), does the existence of such provable statements help me say anything about $\neg G$? – Nikolaj-K Aug 15 '12 at 19:24
• On one level, it's Platonism – some people believe there is one "true" model of arithmetic, called $\mathbb{N}$. On another level, we're just thinking about provability in a bigger system. As I said before, don't read too much into the word "true". – Zhen Lin Aug 16 '12 at 1:10

To take your three questions in turn:

(i) The incompleteness theorem for theory $T$ is a theorem about what can't be proved in $T$. If $T$ is e.g. a pure theory of arithmetic, its language is about numbers, not about $T$-proofs. The theorem won't even be stateable in $T$'s language: rather is stated in e.g. mathematical English.

Of course, by the trick of Gödel coding we can produce in $T$ a sentence which codes up the claim that if $T$ is consistent then a Gödel sentence for $T$ is unprovable, to get $\mathsf{Con} \to \neg\mathsf{Prov(\overline{\ulcorner{G}_{\mathit{T}}\urcorner})}$. And that sentence will itself be provable in $T$ on very modest assumptions. So we might say that $T$ can itself prove the incompleteness theorem for $T$: but really that is rather careless talk. To repeat, if $T$ is a theory of arithmetic whose interpreted language is about numbers, then its theorems are strictly speaking about numbers and numerical properties, not about proofs.

(ii) No. There are consistent theories $T$ with a Gödel sentence $\mathsf{G}_T$ such that $T$ proves $\neg\mathsf{G}_T$. For example take $T$ to be the consistent but $\omega$-inconsistent theory you get by adding to PA the negation of a standard Gödel sentence for PA. (The unprovability of the negation of the Gödel sentence does indeed require we are dealing with an $\omega$-consistent theory.)

(iii) The proof of Gödel's theorem doesn't require excluded middle: it goes through intuitionistically. (It only involves the intuitionistically acceptable version of reductio.)

• In your (ii), you add $\neg G_T$ to be part of the peano axioms. Doesn't that imply that the sentence $G_T$ is false and so it can't be a Gödel sentence, as that sentence is supposed to be "true, while unprovable"? And yeah, meanwhile I'm less sure if the things I asked in (iii) have a significant impact. – Nikolaj-K Aug 16 '12 at 7:45
• In (ii), the $G_T$ you start out with would not be a Gödel sentence for the extended theory; in other words $G_{T+\neg G_T}$ is different from $G_T$, and would still be independent of $T+\neg G_T$. So neither $T$ nor $T+\neg G_T$ has the property you claim. – Henning Makholm Aug 16 '12 at 12:54
• @HenningMakholm No, $PA + \neg G_{PA} \vdash \neg G_{PA + \neg G_{PA}}$. That's consistent with Gödel, because $PA + \neg G_{PA}$ is not $\omega$-consistent. As I say, a standard textbook result. – Peter Smith Aug 16 '12 at 17:49
• @Peter: I emphatically disagree with the assertion $L_A$ that has semantics: it is an inherently a purely syntactic object! Formalizing a language is the thing we do when we specifically want to manipulate a language at a purely syntacic level! (I disagree that pure syntax is "devoid of meaning" but that's a side topic.) Of course, our disagreement only emphasizes why it's important to separate syntax and semantics, even in English. While we are both making statements according to the same syntax, we are clearly applying very different semantics! – Hurkyl Aug 16 '12 at 20:56
• @NickKidman I suspect you need to read a textbook or two that gives a good presentation of Gödel's incompleteness theorems. There are plenty out there. For some recommendations see logicmatters.net/students/tyl – Peter Smith Jun 10 '13 at 8:34

There are two things to be aware of here.

The first one is that the Godel sentence is independent of the theory. It's specifically constructed so that neither G nor not G is a theorem.

The second one is that if one considers a particular model of the theory, then either G is true under that interpretation, or not G is true.

The "unprovable but true" version of Godel's incompleteness theorem only makes sense when the speaker is implicitly referring to a particular model -- usually the particular set of natural numbers that is implicitly part of the theory of formal logic.

• $\neg G$ won't be a theorem of the relevant theory $T$ so long as $T$ is $\omega$ consistent. But if $T$ is $\omega$ inconsistent we can have $T \vdash \neg G$. – Peter Smith Aug 16 '12 at 7:40
• @HenningMakholm Sorry, I'm afraid you are doubly wrong. (i) it is a standard textbook result that $T = PA + \neg\mathit{Con(PA)}$ proves $\neg G_T$. See §25.6 of my book for the proof. – Peter Smith Aug 16 '12 at 17:42
• @HenningMakholm (ii) Sure, $T$ won't prove the negation of its own Rosser-sentence. But that's irrelevant, as $T$'s Gödel sentence and its Rosser sentence are not equivalent in $T$. – Peter Smith Aug 16 '12 at 17:45
• @HenningMakholm The original poster said "(the Gödel sentence "G")", and that is what I certainly assumed was under discussion. After all, when people talk of "the Gödel sentence" they surely don't usually mean "the Rosser sentence"! – Peter Smith Aug 16 '12 at 19:18
• @PeterSmith: My impression is that "Gödel sentence" is usually used as an imprecise term for "some sentence that is systematically constructed to be independent of a particular axiomatic theory, following techniques similar to those introduced by Gödel". After all, each author seems to have his own particular way to fill in the details of the construction (understandably enough, because they want it to match the particular formalization of FOL they work with). – Henning Makholm Aug 16 '12 at 19:24