How can there exist theorems like Goedel's Completeness theorem or Incompleteness theorem? They all make some statements about logical theories, but don't we need a certain logical scheme first to be able to actually derive or even define anything in the first place?
Specifically I want to ask which type of logic Goedel used in order to prove his theorems.
The set of all possible theorems $T$ matching a grammar (like first order logic grammar) is countable. So there is trivially a bijection $M$ between theorems and natural numbers.
An inference is a computable function that (usually) inputs 0 or 1 or 2 theorems and outputs a (new) theorem. So for each inference $I: T^k \to T$, there is a dual computable function $I^*: \mathbb N^k \to \mathbb N$ such that (for example) $I(T_1,~ T_2) = T_3 \iff I^*(M(I_1),~M(I_2)) = M(I_3)$.
Consequently, a statement in the language of theorems (such as "this set of axioms never implies a contradition" or "every theorem is provable or disprovable from axioms") are true if and only if a certain statement about natural numbers is true. It is possible to algorithmically convert the theorem-grammar statements into natural-number-grammar statements because computable bijections are demonstrable.
This is how Godel is able justify statements like "no logic is able to decide all statements over a grammar that includes (all properties of) natural numbers unless the logic itself is inconsistent". He is mechanically proving a statement about natural numbers, and leaving it to the reader to accept that since the mapping of the statement is about theorems that the theorems statement must also be true. This is pretty acceptable since the mapping is algorithmic, so the mapping itself should not depend on any idiosyncracies of any specific logic.
Ultimately a meta theorem relies on some intuition. Sometimes the original proof is given in a descriptive manner that is absolutely convincing but outside any real formal system, and other times the proof is more formal. However, no matter how formal the proof is, the association between a theorem in a formal system and a truth about formal systems in general requires some intuitive notion that the theorem relates to the universe of formal logic in the way it is claimed to relate. For example, Godel's Incompleteness Theorem associates theorems in first order logic with natural numbers. That association is an interpretation that, however straightforward, is not strictly expressible in a first order theory. The statements correlate in an obvious, unquestionable way, but the correlation itself is an observation made with human intuition.
A meta theorem requires an intuitive understanding that what is formally proved actually does relate to formal systems in general. A meta theorem may even be proven entirely by intuitive argument. A good example of this is the Completeness Theorem.
I can't remember Godel's version of the proof well enough to talk about it specifically, but I do freshly remember another version that is very similar. Actually, no proof I have seen deviates from the following in any really fundamental way (including Godel's, I do remember that much).
You basically try to create a universe of discourse satisfying an arbitrary statement. First, you write your statement in prenex normal form (a string of quantifiers followed by a quantifier free expression). Then you assume the existence of a single element in the universe of discourse. Then you fill each universal quantifier with that element, and assume each existential quantifier is a unique element not yet considered. Then you repeat - in a systematic way, you give each element you have found a chance to play every possible role as a universally quantified variable, and in every combination with other elements already found, and the existential variables are always satisfied by new elements. If you are in first order logic without equality (which is just a couple axioms away from first order logic with equality), then this works because you can clone elements without changing what statements are true for a given universe of discourse. So, even if you have already listed a given existential variable, you can list a new one and call it a clone.
Now, as you introduce these new elements, to have a well defined universe of discourse, you need to define how these elements relate to existing elements. So, basically, at each introduction of a new element, the process branches for each possible decision, for each relation with each listed element. Some branches will make choices that doom the process to end in contradiction - there will come a set of universally quantified variables that does not allow any choice for existentially quantified variables.
So, as you continue on in this fashion, you say one of two things must be true. Either all branches will eventually reach contradiction, or there is some sequence of relation choices that can always avoid contradiction. In the first case, you have a proof of the negation of the statement, by way of contradiction. In the second case, you have a universe of discourse satisfying the statement, and so the statement can not be false. Thus every false statement can be identified, as a statement where all branches die must be such that all branches die in a finite number of steps, yielding a proof in first order logic. As an immediate corollary, all true statements can be proven so (i.e., by proving their negations false).
That is obviously not a proof, but you can see how you could work out the details and present this proof outside any formal system in a totally convincing way. That is basically why the proof works. It really comes down to us just logically thinking about the process described, and seeing that it works. Any meta statement, though it may require technical work within a given formal system, always requires an intuitive step to be connected to any assertion outside of all formal systems.
For example, the completeness theorem could alternatively be presented as a statement in a formal system, but you would need to intuitively establish that the formal statement actually represents the completeness theorem. So, either way, there is intuitive reasoning involved.
Another example is Turing's proof that the halting problem is not computable. You simply explain the Turing machine that acts as a contradiction. A formal system really doesn't help with that. You could state it in a formal system, but then you would need to intuitively argue that your formal system actually represents Turing machines in the intended way. Again, either way, there is an intuitive argument to be made.
Godel's Incompleteness Theorem is more technical. But, like I said before, there still is that intuitive step. In particular, the statement "This system is consistent" is not actually possible to state in any formal system. A statement about the natural numbers can be made, which has the meaning "This system is consistent", but that statement about the natural numbers only has that meaning because you have intuitively interpreted the natural numbers as having a particular association with the statements in the theory. That interpretation needs to be accepted on intuitive grounds (not to say it is at all doubtful, but it still needs to be accepted).
So, in short, meta proofs can be simply totally convincing intuitive arguments. The Completeness Theorem and the Halting Problem are both very well approachable in this way. You can also state the problem in the language of a formal system, and prove it in that system. However, you still rely on intuition to know that you have correctly translated your meta statement into that formal statement in the first place. Either way, you simply have a totally convincing intuitive argument - either comprising the entire proof, or just the crucial step of expressing the statement being proven in a formal system. Without an intuitive step like that, there are no meta theorems.
