Gödel's Incompleteness Theorem

Question

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.

Ergo,

G is unprovable (in A)

QED

---

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.

---

EDIT 1 START

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

So,

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.

EDIT 1 END

---

EDIT 2 START

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??

EDIT 2 END

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.