I am posting my comment from this questionthis question as a separate question, as was recommended to me. (EDIT: I'm sorry if it ended up being too similar a question, I just wanted to phrase it in the terminology I think of it in)
First, let me mention that I agree with Hilbert's formalism - when we make the claim "X is true", it is really a shorthand for: "If we label certain strings of symbols 'true', and we label certain rules for symbol manipulation 'truth-preserving', then we can manipulate our initial strings using our rules to reach X". If someone disagrees with our choice of initial strings, or our choice of manipulation rules (which, together, I'll call a "system"), then they will obviously come to some different conclusions. Now, mathematicians happen to have preferences about which systems to study, and those preferences are often motivated by apparent analogies between those systems and the real world, but no system is "right" or "wrong".
I realize that this is not everyone's view of mathematics, but I wanted to explain my reasoning before asking my question:
In what system do logicians usually "prove" metamathematical theorems - i.e., claims about systems? As I mentioned, all theorems, metamathematical or otherwise, are really of the form "In the system Y, X is true." The potential problem I feel with some results like Godel's theorems is that X is a claim about systems which are not necessarily consistent with Y - how does this make sense?