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.)

[jcreed.livejournal.com]

Well, a model of constructive propositional logic looks like the following. (It has a lot to do with models of modal logics)

A model consists of a set W of "worlds", a binary "accessibility relation" R on worlds, and a "valuation" V which is a function which takes a pair consisting of a world x and proposition variable p to V(x,p) in {true,false}. Think of xRy as "y is accessible from x" or "in x, one can imagine a world y", or "state x might evolve to state y". We demand of the relation R that it is transitive and reflexive. Think of V(x,p) as being "whether p is true at world x". We require that V is "monotone increasing": if p is true at x, then it is true forever after, in all future worlds accessible from x. That is, for all x, y, p, if V(x,p) = true and xRy, then V(y,p) = true.

So that's what's required to be a model. We recursively interpret sentences in the propositional language consisting of propositional letters p, AND, OR, IMPLIES, and NOT. "M, x |= A" means M models A at world x where M = (W, R, V).

M, x |= p means, V(x,p) = true
M, x |= A AND B means, M, x |= A and M, x |= B
M, x |= A OR B means, M, x |= A or M, x |= B
M, x |= A IMPLIES B means, for any y such that xRy and M, y |= A, we have that M, y |= B
M, x |= NOT A means, there is no y such that xRy and M, y |= A

mod th?

[jozefpronek.livejournal.com]

consider the question of _decidability_ of the complex numbers (given a sentence phi written with +,*,0,1, is phi valid in the complex numbers?). I know two solutions to this question (that you may think is "very practical" math): without model theory and with.

Without model theory, it is a fairly complicated argument.

With model theory, it is an immediate consequence: the theory of alg. closed fields of char. 0 is categorical (Steinitz), thus complete (by easy model theory)...

-

the previous is just an example of a very classical "application". Others include a very good analysis of Hilbert's Nullstellensatz (if Hilbert's Nullstellensatz is not practical, then I don't know what is - it is at the base of comm. algebra and alg. geometry - which are finding their ways even to robotics, regardless of their central status in math)

-

as easwaran commented, recently model theory has provided solutions to longstanding open questions in alg. geometry and number theory (the Mordell Lang theorem is the most famous)

-

Boris Zilber (Oxford) has recently found strong connections between advanced model theory (the so called excellent classes) and questions on complex exponentiation - the Schanuel conjecture

-

I frankly don't know what do you expect from a model theory class - I daresay one big advantage is to learn from the big change in perspective that model theory provides: instead of looking at ONE structure, you look at a whole CLASS OF STRUCTURES that end up giving you information on the original one, more (or less) controlled depending on the situation.

Model theory also introduces strong QUALITATIVE distinctions inside and between classes. In many respects, model theory is more a part of mainstream mathematics than of logic.

Recent model theory has become ever more independent of logic, in the following precise sense: instead of focussing in Mod(T), the models of a first order theory T, the focus may be shifted to a class of models (not necessarily of the form Mod(T)) and the way they "sit inside each other". That is a growing subject (Model Theory for Non Elementary Classes).

[rdore.livejournal.com]

One of my favorite cute uses of elementary model theory (originally due to I think James Ax in the 60s) is that for polynomial functions from C^n to C^n injectivity and surjectivity are equivalent. This fact has a fairly short, straightforward proof accessible to someone who's taken perhaps half a semester's worth of model theory. In contrast it was not proven without model theory until about 10 years ago. I'm not personally knowledgeable, but I've heard that model theory has given some substantial results in algebra. What's interesting is that for a long time, people said that more sophisticated model theory ideas were useless, and only within the last few years have they been shown to be quite useful.

RE: constructivism. In most areas I think It's possible to get by constructively, but it becomes a much more horrendous mess. But you do lose even some pretty basic facts just throwing out the axiom of choice, such as the fact that every ideal in a ring can be extended to a prime ideal, or that every vector space has a basis. Another good example is the Hahn Banach theorem, which is a nice statement about extending norms in certain contexts.

Actually, the real reason I don't like constructivism is because it throws out the very notion of a model. I mean if you actually have ANY model in some language, it's going to make either A or ~A true. (Admittedly, this is assuming the same principle in the meta theory). I look at constructivism a lot like NF, sure it's a cool system, and in a certain weird sort of way it makes some sense. But it seems more like a toy and doesn't really model how we argue mathematically.

In any case, I think logic really had the effect of telling mathematicians something they didn't want to hear, which is that just like everything else, mathematics is relative.

Re:

[jcreed.livejournal.com]

Don't get me wrong, I'm not really a constructivist at heart, but I don't think it's right to say that constructive logics don't have a model theory. They just have a different model theory, one where the definition of satisfaction doesn't look the same. And indeed you don't get A v ~A all the time, even when it's true in the ambient meta-logic. See my above comment, for instance. A model with three worlds x, y, and z, with z and y accessible from x, where P holds at z alone, satisfies neither M, x |= P nor M, x |= ~P.

Re:

[gustavolacerda.livejournal.com]

perhaps then I should think of constructive |= as "|= []", where "[]" means "provable"?

Re:

[gustavolacerda.livejournal.com]

Actually, the real reason I don't like constructivism is because it throws out the very notion of a model.

I speculated in class that constructive theories wouldn't have models, but Troelstra responded that they do, they are just non-standard models.

But to me, if formulas are defined to be true iff they can be proven, then we have a purely syntactic theory, with no models.

I am experiencing a communication gap... maybe because the experts can't talk down to my level.

Re:

[jcreed.livejournal.com]

Sadly, I can't remember the translation off the top of my head --- I don't think it's as simple as just tossing a [] out front --- but I'm certain I've read somewhere of a nice relationship between constructive logic and the modal logic of provability. Just a guess, looking at the semantics, is that it should be something like

(A AND B)* = A* AND B*
(A OR B)* = A* OR B*
(A IMPLIES B)* = [](A* IMPLIES B*)
(NOT A)* = [](NOT A*)
p* = p

but your basic intuition is right.

Re:

[rdore.livejournal.com]

This just seems like another toy to me. Further, I find constructive logic (and admittedly proof-theory-esque stuff in general) to be very clunky feeling. When I see a cool result in model theory, it's somehow as if someone has clearly understood the tools or structure of something, and found a clever way to use them. Proof theory stuff seems to be an excercise in picking the right induction hypothesis based on messy details of formulas and such.