First off I know very little model theory so apologies if I say anything very dumb or offensive to logicians/model theorists. Second I should note that a lot of what I am saying here is motivated by myself trying to support a (game?) formalism philosophical standpoint for mathematics.
It seems to me that much of mathematics (group theory, topology, calculus, complex analysis, differential equations...) can be worked out entirely using the set theory axioms and proof theory. That is, you start out with a formal language (language of first order logic), a set of sentences within that language (the ZFC axioms, for example) and a syntactic proof calculus which allows one to derive new sentences from the axioms and previously derived sentences. Additionally you allow the possibility to introduce new defined symbols etc. and from all of these ingredients you should be able to define the basic structures studied in the above sub-fields of mathematics as well as prove the important mathematical results about those structures.
To me this seems like enough for mathematics to do. I understand that in addition to simply manipulating the sentences of the theory we can also put an interpretation onto those sentences to create a model for that theory. The interpretation can be thought of as assigning truth values to the sentences of the theory. I understand this can be done but I don't really see what it adds to the program I have outlined above.
As I have (probably crassly) described it here I can see that model theory could be an interesting field of study in its own right. It is also very clear that the interplay between model theory and proof theory could be very interesting. But I guess my question is: for the proving of "usual" mathematical results do we need model theory at all or can we happily get away with only dealing with syntax and proof theory?
A few more notes.
1) I have thought about some of this in the context of my trying to understand Godel's completeness/incompleteness theorems. Sometimes Godel's first incompleteness theorem is stated as saying that in certain languages there are sentences which are true but not provable. This is confusing and very troubling (but resolvable once you learn all of the appropriate background and definitions...) However, if you jettison model theory/semantics and simply worry about semantics then it seems to me like the result says that in certain languages there are sentences which have the property that neither they nor their negation can be derived from the axioms using the inference rules. This is really not that surprising (though not quite trivial so still interesting) and I would say a bit less troubling, at least on a naive reading. The reason I say it is not so surprising is because it seems to me that in general theories will not be syntactically complete and I would suspect that only very special theories are in fact complete. Is this characterization of Godel's incompleteness theorem sans semantics appropriate?
2) Related question: What is Model Theory The answers to this question do help but they get pretty mixed up in Galois theory and specific applications of model theory of which I am not familiar. I guess I am looking for an answer as to the use of model theory which is a little less technical than the answers to the linked question and specifically addresses my feeling that for many things proof theory without model theory is "good enough".
Any information or references on semantics/syntax with the flavor I am describing above will all be much appreciated!