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!
Best Answer
I guess that you are half right, assuming I have understood you correctly.
You are right when you say that one can do mathematics inside the logic of set theory (although one could consider a different theory, but I do not want to go in this now).
Indeed model theory falls in this way of doing things. Model theory is done in set theory, its objects (interpretations, languages, theories etc) are made out of sets, and results of model theory follow from the axioms of set theory (for instance compactness theorem require axiom of choice, or at least dependent choice).
Nevertheless we can observe that much of the work done in algebra is actual model theory in disguise, indeed lots of results in model theory are clever generalization of algebraic techniques.
Finally we can say that model theory provides techniques to prove independence result (i.e. results that prove that some statements cannot be proven by certain set of axioms) which cannot be proven without it (at least at the best of my knowledge).
Edit: looking to the comments below I think that probably I should some other things.
It seems to me that you see syntactic and semantics in logic as two ways to prove statements. In the appropriate technical context of formal logic this could be true but it seems to me that you are thinking to something different.
Allow me to explain. When "doing" mathematics we only have one way to prove statement inside mathematics, and that is by writing down proofs.
Both proof theory and model theory, and any other field of mathematics, are about doing proofs via inference rules.
From this point of view mathematics is just a syntactic activity. But of course in choosing the axioms and how to apply the inference rules we are guided by the intuition of the "intended models" for our formulas. So mathematics is just a syntactic activity but nevertheless its formulas are not just meaningless strings (despite what some common folks may think), they are statements regarding structures of some sort.
With this in mind we can say that the actual practice of mathematics, finding proofs by reasoning about structures that satisfy some axioms, is much closer to the underlying idea of model theory than proof theory.
Indeed syntactical methods are methods where you find proofs of theorems reasoning about the proofs themselves instead of the mathematical objects described by the formulas and I argue that rarely people do real mathematics in this way.
So one could say that mathematics is more model theoretic than proof theoretic.
Of course in various fields of maths one does not necessarily have to use all the results of model theory, but it is also true that the same holds for the results of proof theory.
I hope this helps.