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

[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