I am posting my comment from this question as a separate question, as was recommended to me.

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 which system are we "proving" 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?