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
show 9 more comments

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
@NickKidman No, adding $\neg G_{PA}$ as an axiom doesn't make it true! The resulting theory $PA + \neg G_{PA}$ is indeed unsound, which is why we can derive falsehoods in it (like the negation of its own canonical Gödel sentence!). –  Peter Smith Aug 16 '12 at 17:53
@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
show 9 more comments

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
show 7 more comments

The whole point of a Godel sentence is that it is true, but not provable. So, for instance, the statement of Godel's incompleteness theorem might be "There exists a number $x$ which is the Godel number of a sentence $\sigma$ which is true in $\mathbf N$ but not provable in $T$", where $T$ is some theory.

This cannot be formalized within the theory $T$ itself, though. Although $T$ can probaby talk about provability (even weak theories, such as Robinson's $Q$, can define this), there is no first-order formula which can express that $x$ encodes a true sentence. This is Tarski's theorem of the undefinability of truth.

What this means is that Godel's theorem can not even be formulated in the context of the original theory, let alone proved in it.

-
That depends a lot on which formulation of Godel's theorem you use; '$G$ is true but unprovable' can't be formalized, but 'neither $G$ nor its negation is provable' can be (and indeed, IIRC this was the brunt of Godel's effort); the statement '$\mathrm{Con}(T)\implies(\neg B_T(G)\wedge\neg B_T(\neg G))$' is, IIRC, provable within $T$ itself (for sufficiently advanced systems $T$, of course). –  Steven Stadnicki Aug 15 '12 at 19:29
But doesn't $G$ in Gödel's theorem basically say "this theorem cannot be proven"? If you could prove inside $T$ that you cannot prove $G$, then wouldn't you have proven $G$? –  celtschk Aug 15 '12 at 20:23
@celtschk You don't prove that you can't prove $G$; you only prove that the consistency of $T$ implies that $G$ is unprovable. This is, in fact, where the second incompleteness theorem comes in: if $T$ could prove $\mathrm{Con}(T)$ then it could prove $G$; ergo, if $T$ is consistent then it cannot prove its own consistency. –  Steven Stadnicki Aug 15 '12 at 20:58
@StevenStadnicki: I see. But that means in reverse that if you can prove the consistency inside $T$ then $T$ is inconsistent, so the consistency proof is actually a proof of inconsistency. Nice concept: "I've proven it, therefore it's wrong." :-) –  celtschk Aug 16 '12 at 9:11
@celtschk This is, roughly, true - but on the flip side, if you can prove $T$'s inconsistency inside $T$ it doesn't necessarily imply that $T$ is inconsistent! There are systems that are consistent but can prove their own inconsistency; they're just inaccurate - not everything that they prove is true (but they never prove a statement and its negation)... –  Steven Stadnicki Aug 16 '12 at 15:02
show 1 more comment