Replies

Actually he showed it for the axioms of Peano arithmetic. It hasn't even been successfully extended to the axioms of set theory, let alone any formal system.

Sure it has. Gödel's Incompleteness Theorem applies to any axiom system at least as strong as Peano arithmetic, as long as that theory is consistent and is recursively axiomatizable (which means that there is a computer program that would list precisely the axioms of the system, if allowed to run forever -- in other words, it means that you actually can tell what the axioms are). In fact, there are weak subsystems of Peano arithmetic that will do.

Anyway, this applies to Zermelo-Fraenkel set theory, for example, as well as any common variant, extension, etc. If ZF is consistent, then the sentence that asserts "ZF is consistent" is neither provable nor disprovable in ZF.

Sure it has.

That's what I thought too.
Incidentally
I've never understood why G's theorem is thought to be profound.
To paraphrase it slightly
it simply says that certain chess positions can not be reached
by a series of legal moves.

Nobody knows whether set theory with its typical extensions is consistent. And nobody knows whether operations like choice on transfinite sets always have strictly enumerable sense - the typical assumption is that they don't (which may mean they make nonsense, or may not). If you can do an infinite number of constructionist steps in one go, e.g., then you might answer every Turing halting problem one per step, and thus answer formally non-computable questions. If you can't be put in one to one correspondance with universal computations you are beyond the enumerables and the proof won't go through.

This doesn't happen with arithmetic because you can enumerate the theorems of arithmetic. If you try to enumerate the theorems of set theory in the same way, you hit a snag once you have sets of cardinality greater than the integers and start having theorems about each element of them. Sure you can set up some enumeration scheme, based on applying whatever operations are allowed in some definite order. But this enumeration won't be "onto" for the possible theorems of set theory.