I always was wondering: Godel proved his theorem regarding formal systems described in Principia Mathematics. In my understanding this is some higher level logic with recursive functions.
But how this can be extended to the whole universe of all possible formal systems? Who guarantee that there will be no some new system with quantum-oracle-operator, which will not be affected by incompleteness theorem, and can self-proof self-consistency?
Even well known m-recursive functions (which are essentially Turing machines) are wider class than primitive recursive functions used in the proof..
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.
> 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..
> 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.)
> 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.
If you want to see a relatively brief video of a somewhat drunk Scott Aaronson talking about many interesting possible consequences of the no-cloning theorem, including Godel's Incompleteness Theorems (iirc), enjoy this one from a quantum crypto conference - https://www.youtube.com/watch?v=Z-fa669IR7I
It says "any system which includes the Peano axioms is either inconsistent or incomplete." So having a wider class doesn't help, if it contains the Peano axioms.
Proof was made within specific framework, with very specific quantors and type of inference, I still don't understand how it prevents existence of more powerful frameworks with different quantors and inference where incompleteness theorems wouldn't work.
You can construct a new Incompleteness Theorem for any more powerful formal system. To really get syntactic completeness, you would need an infinite tower of Goedel Statements as axioms, where the truth of each one is a completely independent mathematical fact not reducible to any other axiom ever.
Effectively, syntactic completeness in logic is equivalent to the Halting Problem in computing, via bijective proofs.
Let me give you example.
At first you have predicate calculus, and Godel completeness Theorem.
Now you add new tool: existence predicate, and you got first order logic, which allows you to prove Godel's incompleteness Theorem.
What is the guarantee exactly that more advanced systems can't exist? Say system with new 'quantum hack' operator.
You can't prove formula from Godel's proof? 'Quantum hack' under some conditions covers missing gap in proof path by building continuum truth table and give you tool to check if formula from Godel's proof actually provable, or it is false.
Goedel's Completeness Theorem is for semantic completeness, and still applies to first-order logic. It says, "every theorem which is semantically true for its theory (true in all models of that theory) is syntactically provable." Goedel's Incompleteness Theorem applies to syntactic completeness. Syntactic completeness would mean, "Every syntactically-valid formula is either provable or refutable." Instead, what Goedel's Incompleteness Theorem tells us is: "Some syntactically-valid formulas are neither provable nor refutable, because they're true in some models (standard models) but not in others (nonstandard models)."
Again, this applies to any given formal system. Goedel's Incompleteness Theorem is parametric over formal systems, with first-order Peano Arithmetic being one of the weakest, most standardized systems in which it applies. The real condition for the Theorem is, "Any formal system sufficient to describe Turing machines."
>Say system with new 'quantum hack' operator.
That operator is called a Turing Oracle, and it's physically impossible. Possessing a Turing Oracle is equivalent to reversing the Second Law of Thermodynamics and refuting Heisenberg's Uncertainty Principle. It's physically wrong.
> Goedel's Incompleteness Theorem is parametric over formal systems, with first-order Peano Arithmetic being one of the weakest, most standardized systems in which it applies.
It is parametric over formal systems described in Principia Mathematics. That's it. It doesn't take into account other possible types of formal systems. At least I didn't notice this when reading actual proof.
> That operator is called a Turing Oracle
I think it may be very different thing. I just gave you a quick example. That operator can be something very different. You can set measure on space of proofs, and derive concept of asymptotic proof, and say if proof is asymptotic, then it is proof. There can be many variations around possible formal systems.
> and it's physically impossible
This is very strange argument. Turing machine contains infinite amount of memory, and likely is physically impossible.
But how this can be extended to the whole universe of all possible formal systems? Who guarantee that there will be no some new system with quantum-oracle-operator, which will not be affected by incompleteness theorem, and can self-proof self-consistency?
Even well known m-recursive functions (which are essentially Turing machines) are wider class than primitive recursive functions used in the proof..