We can absolutely reason formally from outside a formal system, by embedding it in a larger one, and this is a very standard and normal technique that anyone working seriously in this area does all the time. E.g. you work in ZFC + some large cardinal assumption that allows you to construct a model of ZFC inside that system, and then reason formally about ZFC there.
> WE can give an interpretation to formal sentences but when we interpret a given sentence as referring to "itself" doesn't it really refers to the interpretation, not to "itself" but its interpretation?
Indeed it can't - see e.g. Löb's theorem. A formal system can manipulate a set of rules that might happen to be its own rules, but it can never "know" that those are in fact its own rules. Which makes sense when you think about it.
Yes, very interesting point. It can not know that they are its own rules. BUT we can know that. Therefore we the meta-level can reason about the subject more than it can of itself. For example the subject-system can not mechanically prove that it is looking at its own ruleset.
So the term "unprovable" should probably best be always qualified with: in which system.
There are facts about systems which the system itself can not prove. Statements like that can be expressed in some formalized subset of English and proven following the rules of that formalized English. What is that "formalized English" that we use in our reasoning? Or does it not matter?
> There are facts about systems which the system itself can not prove. Statements like that can be expressed in some formalized subset of English and proven following the rules of that formalized English. What is that "formalized English" that we use in our reasoning? Or does it not matter?
Again, the normal, routine thing is to just use a slightly larger formal system to work with them. But it really doesn't matter.
> WE can give an interpretation to formal sentences but when we interpret a given sentence as referring to "itself" doesn't it really refers to the interpretation, not to "itself" but its interpretation?
Indeed it can't - see e.g. Löb's theorem. A formal system can manipulate a set of rules that might happen to be its own rules, but it can never "know" that those are in fact its own rules. Which makes sense when you think about it.