[crypto5]

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.

[eli_gottlieb]

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.

[crypto5]

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