[chowells]

Godel's technique is a constructive proof that depends on two things to work. One, the logic needs to be at least strong enough to express the Peano axioms. Two, it needs a finite formalism of the logic to construct the proof out of.

If you have those two things, Godel's technique works. The details vary greatly based on the formal logic in use, but part of the process is encoding the formalism in Peano arithmetic.

So no, adding more things doesn't break it, because the construction takes those additional things into account.

Unless you want your logic to be infinite, of course. In that case, the method would break down. But it has to be infinite in the sense of having no finite representation, rather than the much weaker sense of having some infinite representation.

[crypto5]

See my comment about what do I mean: https://news.ycombinator.com/item?id=14039104

> Unless you want your logic to be infinite, of course. In that case, the method would break down.

Godel numbering is infinite, because it is just natural numbers. Nothing prevents you to build the same proof for infinite number of axioms, rules, functions, variables..

[chowells]

> Godel numbering is infinite, because it is just natural numbers. Nothing prevents you to build the same proof for infinite number of axioms, rules, functions, variables..

That's kind of a non-sequitor. Second-order logic, the logic required to express Peano arithmetic, consists of a finite number of axioms and inference rules. The number of statements that can be generated with those rules is irrelevant. The logic is finite.

Godel numbering requires assigning a number to each logical axiom and inference rule. The mechanism of Godel's numbering implies that every derivation has a unique number as well, but that number is derived, not assigned. The difference is important. It means that the information required to construct the system is finite. If the supply of axioms and inference rules was infinite, with no finite alternate encoding, it would mean Godel numbering would fail because the process of assigning numbers to each axiom and rule would never complete.

But that's all a bit of an aside. To get back to your original question...

Godel's proof provides a mechanism to construct a statement that refers to itself in any logic that can express Peano arithmetic. Once you can make a statement refer to itself, the game is over. You've lost.

But Godel's approach is even more clever. Not only can a statement refer to itself, it can refer to proofs in its own formal system.

So it constructs "This statement has no proof within the formal system it's expressed in."

That's far more subtle of a statement than you give it credit for. It makes no claim about other formal systems. But once you start addressing it from a different formal system (or an informal metalogic) the statement no longer refers to the logic system in which you are examining it.

So sure, you can say that Godel statement G0 constructed in formal system L0 is provable (or disprovable!) in formal system L1. But that doesn't prove anything about the completeness or consistency of L1, because G0 is a statement about L0. And if L1 happens to be strong enough to encode Peano arithmetic, you can construct a statement a Godel statement G1 which refers to logic L1.

This is always applicable. Whatever your G0 and L1 are, G0 says nothing about L1, but the existence of L1 is irrelevant to the statement G0, and very probably also allows the existence of G1. (I've spent lots of time discussing when it doesn't, and won't belabor the point further.)

[crypto5]

> If the supply of axioms and inference rules was infinite, with no finite alternate encoding, it would mean Godel numbering would fail because the process of assigning numbers to each axiom and rule would never complete.

I strongly disagree with that. There is no evidence of that.

> And if L1 happens to be strong enough to encode Peano arithmetic, you can construct a statement a Godel statement G1 which refers to logic L1.

As I said before, Godel proved that your G1 is unprovable in specific framework of Principia Mathematics, which is first/second/higher theory/logic (consist on quantors, functions, predicate, variables, rules).

I don't see evidence that there can be no other framework even with Peano arithmetic inside which can't deliver consistent theory. You started speculating about framework with infinite set of axiom, and I disagreed with that, but there can be other type of infinite framework, say when you allow proofs of infinite length, then Godel numbering may be impossible, and it can be example of such framework.