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