Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
an initial stub with distracting noise. I submit for your derision, Model theory
Since the bulk of your addition is about first order logic, I am wondering if that material would not better be moved to first order logic
maybe! The next example subsection should state the immediate generalization of "algebra for an operad", then Lawvere theories obviously follow, etc.
My interloper inclination, though, is to fork off an entry Tarski Truth and !include it in both places... but now I must catch-up with supervisors of various sorts, as I'm just back from overextended vacationing...
We do have lots of links to model theory, so it would be nice to have something there. Especially something that explains what a model is!
I created the literature section.
I made a correction at theory: somebody forgot to write that the axioms of a theory must not contain free variables. I expanded (in a conventional way) the idea section at model theory.
Why do you say that the axioms of a theory must not contain free variables? I would have said instead that they should be formulas in some specified context.
In every interpretation axioms should evaluate to constant truth values, thus all variables should be bound; in particular for a concept of a model one needs to be able to test for satisfaction. For example $3x+1$ can not be axiom. But $\forall x, x^2 = x$ is OK (idempotent structures). This is the conventional point of view.
Yes, I guess that is the point of view in conventional classical logic, but I don’t think it is the point of view we should take. One problem with it is that in a fragment of logic lacking the universal quantifier, a statement like $x^2=x$ (in context $x$) is a fine axiom, but $\forall x, x^2=x$ is not a formula in the logic, and so cannot be an axiom. ($3x+1$ is a term, not a formula, so no one would claim it could be an axiom.)
I edited the page to mention both viewpoints; is that okay?
I am happy with it and your comments. (specifying the context $x$ is though somewhat an analogue of binding, isn’t it ?)
Yes, one can think of it as binding $x$ in the metalanguage.
I have added to the end of the Idea-section at model theory the following brief paragraph, thanks to hints from Zhen Lin:
Model theory has strong ties with the theory of algebraic varieties and hence with the part of algebraic geometry that deals with these. It can however not deal with more global concepts such as sheaves or schemes.
Have you seen MacIntyre’s paper on model theory, Model theory: Geometrical and set-theoretic aspects and prospects:
There are various hints in the literature as to categorical foundations for model-theory [21]. The type spaces seem fundamental [28], the models much less so. Now is perhaps the time to give new foundations, with the ﬂexibility of those of algebraic geometry. It now seems to me natural to have distinguished quantiﬁers for various particularly signiﬁcant kinds of morphism (proper, etale, ﬂat, ﬁnite, etc), thus giving more suggestive ´ quantiﬁer-eliminations. The traditional emphasis on logical generality generally obscures geometrically signiﬁcant features [19].
I sense that we should be a bit bolder by now. There are many issues of uniformity associated with the Weil Cohomology Theories, and major definability issues relating to Grothendieck’s Standard Conjectures. Model theory (of Henselian ﬁelds) has made useful contact with motivic considerations, including Kontsevich’s motivic integration [6]. Maybe it has something useful to say about “algebraic geometry over the one element field” [25], ultimately a question in definability theory.
Eventually all these entries on model theory will be brought to a state of coherence. Certainly it is spiritually true that model theorists like to think of their subject as akin to classical algebraic geometry, where definable subsets are viewed as analogous to loci of equations (and there is often a well-developed notion of dimension with which one can make deep structural statements). Also algebraic varieties can provide a good testing ground for developments in model theory.
For now I’d like to change that “can” in Urs’s paragraph to “does”, because there is no telling how model theory will develop in the future.
Thanks, to you all.
What I would eventually like to see sorted out very clearly is how far model theory gets when it comes to actual modelling in “practice”, such as in formulating theories of physics.
As you may or may not know, the blunt claim that all of physics is founded on model theory is currently making a bit of a splash in some public discussion, such as in the New York Times and in various online discussions. You can see it re-iterated here.
When this started a few weeks back, I first thought this should just be ignored. But it is curious to see so very many people discuss these issues of mathematical foundations of physics… albeit at a very naive level.
I was thinking maybe we can boost the $n$Lab entries on model theory just a little bit so as to serve as sources that one could point to in order to increase the level informed data in these kinds of discussions.
It can however not deal with more global concepts such as sheaves or schemes.
This is not entirely true, MacIntyre and his students like Ivan Tomašić done important work there, including on Weyl cohomology theories etc. Of course, it is not typical and not straightforward to say something about it.
how far model theory gets when it comes to actual modelling in “practice”, such as in formulating theories of physics
Far! To an excuse, model theorists are fewer than the specialists for such specialized and odd variant of physics like quantum loop gravity. Do you expect the quantum loop gravitists to lay down foundations of a junk of important physics besides their own subject ? And they are physicists, not mathematicians specialized for a completely different field. It is like expecting quantum loop gravitists to lay foundations of strongly correlated systems. Besides, their attention is to classification, cardinality questions, compactness etc.
Maybe we need to distinguish between standard model theory and all its generalizations. I suppose in full generality considering any kind of model over any kind of theory is “model theory” and so then this subsumes everything.
But consider the standard definition as on the first pages of Hodges’ A shorter model theory. With that concept apparently we cannot say “manifold”. That makes it hard then to speak about much of physics.
But consider the standard definition as on the first pages of Hodges’ A shorter model theory.
Again: using definition of TQFT you can not say anything about normal physics, even not Kepler problem or Maxwell equations as TQFTs have trivial dynamics. Model theory is successful in its own foundational methods, if you accept wider definition then you can not do almost any classification, no compactness theorem, Lowenheim-Skolem etc. Besides, Hodges book is tailored toward the first order theories. ZIegler’s book is much more modern. For your taste, probably the categorical model theory as in works of Makkai, Zawadowski, Joyal etc. would be better to look at.
Zoran, you don’t need to convince me of anything.
I am just asking a technical question, since somebody else is making claims about this, see here:
with the definition as in Hodges’ book, how far would we get with formalizing physics?
Based on what I gather from the above discussion, I have added to the entry a section Scope which currently reads as follows. This is tentative, please fine-tune as need be:
In full generality, model theory would study all kinds of models over all kinds of theories, hence pretty much everything that is considered (in) mathematics. However, in order to find effective classification results for models, one traditionally restricts attention to very special kinds of theories only.
Traditionally the default subject of model theory (e.g. (Hodges 93)) are first-order theories (only) and their models in Set (only), these are the traditional structures in model theory. Among the celebrated classfication theorems provable in this context are the compactness theorem and the Löwenheim-Skolem theorem. (See also geometric stability theory.)
More modern developments in model theory consider also wider classes of theories than just first-order theories (e.g Ziegler).
Is that roughly right? If not, please let me know or else edit directly in the entry.
And: which book by Ziegler exactly would that be?
The sections “Examples” and “Important theorems” at model theory are a bit of a mess (apart from being very incomplete). I have tried to brush-up just the formatting of the Examples-section a bit, with some lead-in sentence such as to make it clearer what it even is that examples are given of. (But it remains a mess.)
At SEP I saw the terminology “classical model theory” for the first-order theory version, and I have used that now in the entry to distinguish cases.
I’ll stop now editing this. A model theory expert would just need 10 minutes to make this entry look much less stubby, without even expanding much. Maybe such an expert with 10 free minutes is around? ;-)
I ended up doing one more thing: tried to brush-up the References section. That had been a bit chaotic, which pointers to motivic integration preceding basic textbooks on model theory and the like. I tried to disentangle it a bit. But please feel invited to do more or to re-organize.
Zoran, you don’t need to convince me of anything.
I am not convincing you but giving you wider scope and comparison; model theorists to whom I communicate are mainly beyond first order theories. I think that I am giving some (new to you in some cases) information about some wider scopes.
One should also notice that it is not the same to have the definitions in some order logic then to have practical reasoning within the same order. Say in topology, you do not quantify only to elements in a topological space, you quantify over open sets of elements, you quantify over families of such (say covers), over families of families, say when you do refinements and so on. Even the higher order model theory is mostly successful when keeping strict control how far you go.
Katrin Tent (Universität Münster, Germany) Martin Ziegler (Albert-Ludwigs-Universität Freiburg, Germany), A course in model theory, in series Lecture Notes in Logic, Cambridge University Press, April 2012
Just came across this article today, and I am generally curious about the following passage:
Operads, Monads and Lawvere theories
Structures from universal algebra, higher algebra and categorical logic that conveniently allow tospeak about theories and their models are operads, monads and Lawvere theories. Each of these may be understood as characterizing a theory. Its models then are the corresponging algebras, see at algebra over an operad, algebra over a monad and algebra over a Lawvere theory, respectively.
In all likelihood my questions are already answered on some pages on the nlab, maybe even this page, so I am just looking for some guidance on where to start.
Is there a more general or fundamental setting in which to define theories and models? Is there a way to define these concepts that is structural, as opposed to material? (The sort of definition of “theory” I am familiar with is something horrendously ad hoc and I find a bit unsatisfying. Is the internal logic of a topos the general setting I am looking for? Or does that only account for the logic as opposed to the full “theory”, which is as an extension of the underlying logic? I am generally confused about this distinction, and the relationship between the internal logic of a topos vs. a theory conceived as a monad/operad/Lawvere theory.
In what precise sense are monads and operads theories? How can one be recovered from the other?
I am new to the concept of operad and have only recently learned about monads, but I see that every operad gives rise to a monad. Is the sense in which the resulting monad is a theory the same as the sense in which the original operad is a theory? Is it true that monads and operads are different beasts entirely, or are they two heads of the same beast?
Checking it out, thanks.
As you may have seen, there is also relevant discussion at MO:q/303847.
(One would think that this point is extensively discussed on $n$Lab pages, but apparently it’s not. I remember that it was the subject of many discussions on the forum. But maybe nobody really wrote it out in any $n$Lab page.)
1 to 29 of 29