A model theory for a particular logic typically works within a given universe, and specifies a notion of structure for a language, and a definition of truth. Logic is typically specified by language (function symbols, relations symbols and constants); formulas (formed from symbols, variables, Boolean operations and quantifiers). Language together with a choice of a set of formulas without free variables (viewed as axioms) is called a theory. A structure is an interpretation of a language via a given set together with interpretation of the symbols of the language. A model of a theory in the language is an L-structure which satisfies each formula in .
The two main problems of model theory are
In all memorable examples, the collection of structures for a language will form an interesting category, and the subcollection of those structures verifying a given collection of propositions in the language are an interesting subcategory again.
See also/first theory.
Caveat Lector. This may duplicate/contradict other nLab accounts of FOL, e.g. theory; it is present here for illustrative purposes only. We attempt to obviate the trouble of quantifier scope by using addressing rather than naming of variables; specifically, the variable occurs bound in a formula if it is nested within more than quantifiers, and otherwise free.
Notable subsets of include , generated by , the suboperad of parametrized words, and , the elements of types in the suboperad generated by .
The Tarski Definition of Truth is a natural extension of the -algebra to an -algebra, such that
(Again, this really should be written more clearly, but it’s a start.)
JCMcKeown: is there some nicer way to say the quantifier nonsense? I’m thinking along the lines
there are two actions of on : one shifts all the variables by 1, the other adds a quantifier; and the Tarski extension is the one that makes these commute somehow
ibid: maybe it’s more right to say that should be the boolean algebra ? This again has that natural action of on it
An -structure , as an -algebra with extra properties, defines a complete first-order theory , that subset of which interprets as , or true. Conversely, given a collection of elements of of type , we say that , or in words is a model of the theory whenever . There is an obvious Galois connection between theories and the collections of -structures that are models. Much of deeper model theory studies the fine structure of this connection.
Focusing on the obvious words “operad” and “algebra”, it’s popular in local quarters to simply understand “operad” for “theory”, and “algebra” for model. See operad for more.
Remaining within Set, we can also generalize beyond first-order logic to various higher-order logics.
((insert your favourite variant here))
The following are closely interrelated, and depend on having a suitable universe . We can view them as theorems of or as (relatively mild) conditions on .
(… clarify …)
Given a first-order theory in some language , is consistent iff there is a model of in — that is, iff for some .
Under the same hypotheses, is consistent iff every finite subset of is consistent; expressed semantically, a theory has a model iff every finite subset of has a model.
(…think of a good way to state this…)
It follows that first-order theories are quite permissive; or in other words that they’re inefficient at pinning down particular structures.
For example, consider the complete first-order theory , and any total order . If one expands the language (coresponding to an injective morphism of operads) to include constant symbols for , then for any subset of of finite size , one has
so that the finite extensions of by suborders of are all consistent; by compactness, the fully extended theory is also consistent; thus by completeness there is a structure such that
By a similar argument, (if ZFC is consistent) there are models of classical set theory satisfying the (higher-order) property that the natural numbers object of includes your favourite total order as a suborder — of course, isn’t allowed to know this — notably, there is no object in such that .
Chen Chung Chang, H. Jerome Keisler, Model Theory. Studies in Logic and the Foundations of Mathematics. 1973, 1990, Elsevier.
Wilfrid Hodges, Model Theory, Cambridge University Press 1993; A shorter model theory, Cambridge UP 1997
R. Cluckers, J. Nicaise, J. Sebag (Editors), Motivic Integration and its Interactions with Model Theory and Non-Archimedean Geometry, 2 vols. London Mathematical Society Lecture Note Series 383, 384
David Marker, Model Theory: An Introduction Graduate Texts in Mathematics 217 (2002)
C U Jensen, H Lenzing, Model theoretic algebra: with particular emphasis on fields, rings, modules (1989)
Boris Zilber, Elements of geometric stability theory, lecture notes, pdf; On model theory, non-commutative geometry and physics, (survey draft) pdf; Zariski geometries, book, draft pdf; On model theory, noncommutative geometry and physics, conference talk, video
Valentin Goranko, Martin Otto, Model theory of modal logic, pdf
John T. Baldwin, Fundamentals of stability theory
H. Keisler. Model theory for infinitary logic, North-Holland, Amsterdam, 1971.
Gerald E Sacks, Saturated model theory, Benjamin 1972
wikipedia model theory