a question for the logicians here

[gusl]

What is model theory good for? Is it relevant for practical mathematics? I am trying to figure out if I should take this class. I know it's essential if you want to be a logician, but since I am skeptical of much mathematical logic (for instance, set theory beyond the basics a working mathematician needs, seems to me useless and about nothing) and not interested in abstract mathematics for its own sake (unless it's beautiful, in which case it relates to something I already know), I wonder what value I can get from it.

Today I had my first class on constructivism. One of the systems seems very much like the "good foundation" I would want for mathematics: a mathematical structure only exists if it can be computed (hence, there only exist countably many numbers, although they didn't say this out loud).

Another question is: does classical mathematics (ZFC, I guess) give you any more real-world, USEFUL theorems than this constructivist theory (I forget which one)? I am including theorems about number theory here.

Also, it seems that in one of these constructive systems, something is true only if it's provable. In that sense, it seems to be "trivially complete".
In general, if you interpret formulas in models, you can check whether they are either valid / satisfiable. What do models of constructive theories look like?

Comments

[easwaran.livejournal.com]

I'm not sure if ZFC gives you any more "useful" theorems than constructivism, except that everything related to the Intermediate Value Theorem in analysis exists only in a much weaker form (that is, you can find inputs that make the output arbitrarily close to zero, not that you can find an input that makes the output exactly zero). However, proofs in ZFC are often _much_ easier to come by than constructive proofs. Of course, they have some conceptual complexities that may make up for this.

As for model theory, I hear that it's quite useful in algebraic geometry. From what I know, it seems that model theory is a good general framework to have around when doing category theory, so you know just what your categories are. (Most categories seem to have as objects exactly the structures that model a particular theory.)