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

Question

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.

Answer 1

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.)

Answer 2

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.