Andris said…
I thought this discussion died… Ok, let me try to clarify myself the last time.
Let’s take a computational rather than mathematical perspective, as this may be more natural at least to programmers. One can see (if squinting enough, a part of) the (first) Goedel’s theorem as a program, which accepts a definition of your formal system as an input, and provides a sententce in the language of this formal system that says that in this system this sentence cannot be proven.
Then the metatheory (meaning we are already reasoning out of scope of this formal system) kicks in - we say, either this sentence is true, and then the formal system contains some true but unprovable sentences, or this sentence is false, and then the formal system contains some false but provable sentences.
My gripe is exactly with this last step - for example, why do we think there are exactly two alternatives? Because our metatheory says so. This part of the reasoning is independent of the formal system we used as input, it is in a way hard-coded, so it is incorrect to say that it we can fully parameterize the theorem by any formal system we choose.
Anyway, there are so many simple impossibility results in computability and logic, that splitting hairs is not too useful (except as an exercise). For example, the number of all imaginable predicates on natural numbers (and this is almost the simplest functions that can be imagined) is uncountable, so only a tiny fraction of them can be expressed as a program of finite size (no matter how big).