I'll keep this short and sweet.

Construct Axiomatic System A in which we can do math.
Gödel Sentence G = G is unprovable in A.

Gödel's Argument (I)
If G is provable then there's proof that G has no proof. Contradiction!

If G is unprovable then no (auto-)contradiction.

Either G is provable or G is unprovable.


G is unprovable (in A)


Hypothetical Argument (K)

Argument I has to be outside A for Gödel's theorems to be true.
Argument I uses logic (even though it doesn't use any of the axioms in A).
Axiomatic system A also uses logic.
How can something that employs logic (argument I) be outside something that too uses logic (axiomatic system A). At the very least they overlap in utilizing logic.
Steel manning: Gödel has used axiomatic system A to prove G that claims it does not use axiomatic system A. Contradiction!

Is argument K any good? Have an awesome day.


(A big thank you to Conifold and Scott Rowe)

Note that G is true in(side) axiomatic system A. Argument I (Gödel's argument) is outside axiomatic system A (re Conifold's comment) then. How is this possible? I'm stumped. Gödel didn't use any of the axioms of A and proved that there's a true statement in A that isn't provable from the axioms of A.

How does one define as being in(side) axiomatic system A? I would say, naïvely perhaps, that for a theorem or proposition to be in(side) axiomatic system A, it would need to be derived/proved from the axioms of A.


If G is in(side) A (G has to be inside axiomatic system A for Gödel's proof) then it has to be provable from the axioms of A. That's what being in(side) an axiomatic system means, conventionally.

But Gödel's argument G claims it is not provable from the axioms of the axiomatic system A.

This is a contradiction.



The Gödel sentence G has to be

  1. Constructible
    But, analogoulsy, E = Aliens exist, is also constructible, but this has no aletheic import. E can be true/false. Likewise G can be true or false. So much for being constructible.
  2. True
    According to articles that I read on Gödel's eponymous theorems, the only "proof" we have that G is true is G itself: G asserts G is true. Isn't this a circulos in probando akin to the Bible Fallacy: The Bible is true "because" The Bible asserts The Bible is true??


  • 1
    I swear by vitamin k myself. (in other words, I have given up the quest for knowledge in favor of health)
    – Scott Rowe
    Sep 17, 2023 at 2:18
  • That's like a true muni. There is hope, after all! Please continue. Sep 17, 2023 at 2:39
  • 1
    Gödel's argument applies to a restricted formal system (like ZFC or Peano arithmetic) and is "outside" of the system itself, it is a meta-argument. Axiomatic system in which we can do all of math (it was Russell's dream) does not exist, it would be inconsistent for Gödelian reasons. Argument K is no good.
    – Conifold
    Sep 17, 2023 at 6:56
  • 1
    To edit: the undecidable statement G is not true "inside" the system; we prove that the system can neither prove it nor refute it. Sep 17, 2023 at 10:22
  • 1
    The unprovable statement G is not provable in the system S but it is true wrt to the usual domain of numbers. Conclusion: for formal systems of a specifiad type not all true statements are provable. This is the gist of GIT. See Godel Incompleteness Theorems. Sep 17, 2023 at 17:22

1 Answer 1


The problem lies with your definition of G. Your G is explicitly self-referential and says of itself that it is not provable. There are many objections to doing this, including the simple one that it violates the Tarskian hierarchy by attempting to be both a sentence in the object language and a sentence in the metalanguage. It has to be in the object language, otherwise it cannot be a sentence in the language of A; but it is also trying to be a sentence in the metalanguage by saying of an object language sentence that it is unprovable. The proof of Gödel's theorem does not actually use such a sentence. So your G is wrong and your argument (I) is not a correct account. At best it is a kind of high level explanation, but it is potentially misleading.

A better account might go something like this.

  1. Let's represent the natural numbers as 0, s0, ss0, etc., where s is the successor function. Let's use ⌜n⌝ to denote the representation of the number n in this way. I'll assume we are familiar with the concept of Gödel numbering, and we will use #(ϕ) to denote the Gödel number of the formula ϕ.

  2. We can construct an arithmetic formula U(x) whose argument is an expression that represents a number. I.e. we can substitute x with something that looks like sssssssssss0 for some definite quantity of s's. The formula U(x) is constructed in such a way that, U(⌜#(ϕ)⌝) holds if and only if ϕ is not provable from the axioms of A. So we can think of U(x) as saying that the formula whose Gödel number is represented as x is unprovable in A.

  3. We now find a particular number n such that U(⌜n⌝) holds within A if and only if U(⌜#(U(⌜n⌝))⌝). The Diagonal Lemma assures us that such an n exists.

  4. The sentence U(⌜n⌝) is our Gödel sentence G. We might say that G in a very indirect way says of itself that it is unprovable, but it does not literally do so. It literally speaks only of numbers and functions on numbers. It is just a sentence within the object language of A and it is not self-referential. If you want to see an example of what a Gödel sentence looks like, take a look at the answer to this question: https://math.stackexchange.com/questions/1472769/what-does-a-godel-sentence-actually-look-like

So Gödel's proof does not involve any contradiction. A properly constructed G sentence is a sentence within the language of A. It is true in the standard model of arithmetic, but is unprovable in A. Gödel's proof uses the axioms of A, since we need those to construct U(x) and n. Gödel's original proof was for the system set out in Principia Mathematica but it generalises.

When you speak of what is inside and what is outside A, I think you can understand that as the distinction between what is stated within the language of A about numbers, and what is stated about the sentences of A. It is the U(x) function and the system of Gödel numbering that allows us to correlate these. The term 'inside' is uncomfortably vague though. When you say:

If G is in(side) A (G has to be inside axiomatic system A for Gödel's proof) then it has to be provable from the axioms of A. That's what being in(side) an axiomatic system means, conventionally.

You are confusing being a sentence within the language of A, and, being a theorem of A. G is a sentence within the language of A but not a theorem.

  • Point 1: It seems that the problem starts with G being constructible (there's a Godel number n for the Godel sentence G). A parallel in natural language is E = Aliens exist. E is constructible, but that has no logical import i.e. just because E (mutatis mutandis G) is constructible it doesn't follow that E or G is true. One down, one to go. Sep 18, 2023 at 1:51
  • Point 2: G has to be true for Gödel's theorem to mean anything and last I checked the only "proof" of that is G itself (it asserts its own truth). Isn't this a circulos in probando? G is true because G claims G is true. Reminds me of the Bible fallacy: The Bible is true because the Bible says the Bible is true. Sep 18, 2023 at 1:52
  • Strictly speaking, we don't have to say that G is true. At bottom, Gödel's first incompleteness theorem proves that there exists a pair of sentences G, ¬G such that neither is provable. That is all we need to establish incompleteness. We may also say that G is true in the standard model of arithmetic. There is a helpful discussion of the significance of this in the responses to this question: mathoverflow.net/questions/405805/…
    – Bumble
    Sep 18, 2023 at 10:08
  • 1
    G does not assert its own truth, or its own falsity for that matter. What it does in an entirely indirect way is to say of itself that it is unprovable. But it does this only indirectly via an encoding within arithmetic. It would be better to say that G is true if and only if it is unprovable. Better still to say that the G sentence for the formal system A is true in the standard model if and only if G is unprovable within A.
    – Bumble
    Sep 18, 2023 at 10:09
  • That G is unprovable has to be true. How do we know that? Sep 18, 2023 at 10:28

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .