What is the purpose of Semantics/Model theory in Mathematical Foundations?

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!

• "there are sentences which have the property that neither they nor their negation can be derived" this is a weaker claim than G.I.T. GIT establishes a predicate $P$ such that for each $n$ there is a proof of $P(n)$, but there is no proof of $\forall n .P(n)$. "True but not provable". GIT was originally a syntactic proof, not semantic at all. Here is a syntactic derivation plato.stanford.edu/entries/goedel-incompleteness – DanielV Jan 21 at 23:23
• Ooh, that is a very cool comment and clarifies my understanding of the syntactic consequences of GIT. I will need to spend some time with the reference you gave. My other questions regarding a pure syntax approach to mathematics still remain. – Jagerber48 Jan 21 at 23:31
• @DanielV "GIT was originally a syntactic proof, not semantic at all." Well, that's debatable - is $\omega$-consistency a fully syntactic property? In my opinion it wasn't until Rosser's improvement that a completely syntactic argument was arrived at. (Of course Godel's argument was vastly more syntactic than semantic, and Rosser's trick wasn't much of a surprise, but it is still an interesting detail worth mentioning.) – Noah Schweber Jan 21 at 23:40
• To the OP, model theory is no different from, say, group theory: we can view "doing model theory" as "proving things about first-order logic (or etc.) inside ZFC (or related)." So it's no more essentially semantic than anything else. – Noah Schweber Jan 21 at 23:42
• The standout aspect of model theory, foundationally speaking, is in my opinion the fact that it pays attention to the relationship between syntax and semantics. A group theorist need not care at all about the theory of groups per se; to a model theorist, however, the fact that the class of groups is precisely the class of models of the theory of groups is an instance of the all-important Godel's completeness theorem (not a typo!). And all of that can itself be embedded in a theory as per usual. – Noah Schweber Jan 21 at 23:51

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.

• Your statement that "You are right when you say that one can do mathematics inside the logic of set theory" seems to answer my main question. When you say one could consider a different theory do you mean one could take the assumption of different axioms than those of ZFC or something? If so then yes, I also don't want to go into that, I want to assume some appropriate axioms are chosen and fixed for the discussion. – Jagerber48 Jan 22 at 0:57
• @Jagerber48 Noah's point, I think, is that you might as well be asking "why do we need algebraic topology at all when formal syntax alone would do just fine?" – spaceisdarkgreen Jan 22 at 3:08
• @Jagerber48 Spaceisdarkgreen is right, but I'd say even more. Our confidence in the formalizability of mathematics-as-practiced comes from model theory itself: mathematics as practiced is very semantic (basically nobody actually writes formal ZFC proofs), and a priori there's no reason to believe that a formal system need exist which would faithfully capture all that semantic gibberish. Model theory provides the argument that such a thing does exist, via the completeness theorem. The formalist (speaking as one) shouldn't be especially hostile towards model theory, but rather (cont'd) – Noah Schweber Jan 22 at 3:53
• should become less skeptical of mathematics-as-practiced as a consequence of learning basic model theory. So in my opinion your criticism of model theory is oddly inverted: you seem to be saying that model theory introduces an element of semantics where none existed before, but that's simply untrue. (Arbitrary first-order structures, or interpretations, are in no way more or less abstract/semantic than arbitrary groups.) – Noah Schweber Jan 22 at 3:55
• That said, it is worth saying that your suspicion that model theory helps package purely formalist results (e.g. statements like "Theory $T$ does/doesn't prove sentence $\varphi$") is definitely true. For example, proving using model theory that the theory of groups doesn't prove "$\forall x,y(x*y=y*x)$" is easy - just exhibit a single nonabelian group - but establishing this just by working with the combinatorics of first-order proofs themselves would be quite hard. But I really think this misses the important bits. – Noah Schweber Jan 22 at 3:58