Model Theory

(redirected from satisfiable)
Also found in: Dictionary, Thesaurus, Legal, Wikipedia.
Related to satisfiable: unsatisfiable

model theory

[′mäd·əl ‚thē·ə·rē]
The general qualitative study of the structure of a mathematical theory.

Model Theory


a branch of mathematics that emerged as a result of the application of the methods of mathematical logic to algebra. By the second half of the 20th century, the theory of models had evolved into an independent discipline, whose methods and results have found applications both in algebra and in other branches of mathematics.

The basic concepts of model theory are the concepts of algebraic system, formalized language, and truth of a proposition in the language under consideration in a given algebraic system. A typical example of an algebraic system is the system of natural numbers together with the operations of addition and multiplication, the relation of order, and the distinguished elements 0 and 1. The simplest propositions in this system are statements of the type “x + y = z for x = 2, y = 3, and z = 5,” “x·y = z for x = 4, y = 2, and z = 8,” and “x < y for x = 2, and y = 3.” Complex propositions are obtained from simpler ones with the help of the prepositional connectives “and,” “or,” “if …, then …,” and “not,” and of the quantifiers “for all x …” and “there exists an x such that….” For example, the assertion that the numbers u and v are relatively prime can be written more explicitly in the form “for all x, y, and z, if u = x·y and v = x·z, then x = 1,” and is thus obtained from simpler assertions with the help of propositional connectives and quantifiers.

In the general case, an algebraic system is understood to be any nonempty set together with collections of relations and operations on that set, each involving a finite number of arguments. These operations and relations are said to be primitive in the given algebraic system. To each operation and relation we associate a specific symbol. The set Ω of these symbols is called the signature of the algebraic system. Usually, classes of algebraic systems having a common signature are investigated.

The most important formalized language is the first-order language. The alphabet of this language consists of (1) the set Ω of the symbols for the relations and operations; (2) the symbols &, V, →, ⌉, ∀, and ∃, which denote propositional connectives and quantifiers (see below); (3) a set of symbols called individual variables; and (4) parentheses and the comma. Moreover, each relation and operation symbol is assigned a natural number, called the place of the symbol; the natural number is equal to the number of arguments in the operation or relation. The special symbol = for the relation of equality is included among the symbols for relations. The concepts of term and of formula are defined inductively. (1) Individual variables are terms. (2) If f is the symbol for an n-place operation and g1, …, gn are terms, then f(g1, …, gn), is also a term. The simplest formulas are expressions of the form P(g1,…, gn), where P is an n- place relation symbol and the g\, … , gn are terms. More complex formulas are obtained from the simpler ones using a finite number of combinations of the latter by means of quantifiers and propositional connectives. Occurrences of individual variables in a formula are either free or bound. Bound occurrences of variables are those that occur within the scope of a quantifier in this variable; whereas all other variables that occur in the formula are free variables. For example, in the formula

(∀x) (∃y) f(x,y) = z V f(x,y) u)

the free variables are z and u, whereas x and y are bound by the quantifiers. Formulas with no free variables are called sentences. Every formula with free variables x1, …, xn defines an n-place relation on an algebraic system A with signature Ω. For example, the formula expressing the assertion that the numbers u and v are relatively prime defines on the natural numbers the relation of relative primeness, which is true for the pair (3, 5) and is false for the pair (2, 4). For the simplest formulas, the corresponding relation is in fact given by the system A itself. For more complicated formulas, the corresponding relation is defined by means of an interpretation of quantifiers and propositional connectives: (Φ1 & Φ2) is interpreted as “Φ1 and Φ2” (Φ V Φ2) as “Φ1 or Φ2,” (Φ1—Φ2) as “if Φ1, then Φ2,” ⌉Φ as “not Φ,” (∀x)Φ as “for all x, Φ,” and (∃x)Φ as “there exists an x for which Φ.” According to this definition, every sentence is either true or false in any algebraic system with a corresponding signature. For example, if the symbol f corresponds to the operation of addition on the natural numbers, then the formula (∀x)f(x,x)which asserts that 2x = 3x for all x—is false for the natural numbers, while the formula (∀x) (f(x, x) = x—f(x, x) = f(f(x, x), x))—which asserts that if 2x = x, then 2x = 3x—is true. An algebraic system A is called a model for a given set Σ of sentences if every sentence in Σ, is true in A. A class K of algebraic systems is called axiomatizable if K is the collection of all models for a certain set of sentences. Many important classes of algebraic systems, for example, groups, rings, and fields, are axiomatizable.

The study of general properties of axiomatizable classes is an important part of model theory. In many cases, certain algebraic properties of the class of all models of Σ, may be predicted from the form of the sentences in Σ. For example, the fact that homomorphic images and direct products of groups again turn out to be groups is a consequence of the fact that the class of groups may be denned as the aggregate of all models of a collection Σ of sentences such that each sentence of Σ has the form (∀x1)… (∀xn) f = g, where f and g are terms.

A fundamental result of model theory is Mal’tsev’s local theorem (1936), according to which if every finite subcollection of a collection Σ of sentences has a model, then Σ, itself has a model. A. I. Mal’tsev found numerous applications for his theorem in proving local theorems in algebra.

An important fact in the theory of axiomatizable classes is the Skolem-Lowenheim theorem: every axiomatizable class of finite or denumerable signature that contains infinite systems also contains a denumerable system. In particular, it is impossible to write down a collection of sentences all of whose models are isomorphic to a single infinite algebraic system, for example, the field of complex numbers or the ring of integers. Nevertheless, there exist axiomatizable classes in which all systems of a given infinite cardinality are isomorphic.

An important specific collection of sentences is the collection that defines the concept of set. This concept can be described in a first-order language whose signature consists of a single symbol—the symbol for a binary relation—which is interpreted as “x is an element of y.” There exist several variants of these descriptions, each of which is realized with the help of its own particular collection of sentences. These collections are called axiom systems for set theory. The development of model theory has shown that it is impossible to select an axiom system for set theory that satisfies all the requirements of mathematics.

The central part of contemporary model theory is the study of elementary theories, that is, theories that can be described in a first-order language. However, increasingly more attention is being given to the study of theories that are described with the help of richer languages.

History. The basic concepts of model theory appeared in mathematics in the 19th century, mainly in works on the foundations of geometry. N. I. Lobachevskii, in his works on geometry, came close to the concept of a model for a given set of sentences. This concept fully emerged in the works of E. Beltrami and F. Klein, both of whom constructed models for Lobachevskian geometry. Modern formulations of the basic concepts of model theory were evolved by D. Hilbert and A. Tarski and their schools. Model theory emerged in the early 1930’s as a result of application of the methods of mathematical logic to algebra, a field in which A. I. Mal’tsev was one of the initiators.


Mal’tsev, A. I. Algebraicheskie sistemy. Moscow, 1970.
Robinson, A. Vvedenie v teoriiu modelei i metamatematiku algebry. Moscow, 1967. (Translated from English.)


Model theory

The body of knowledge that concerns the fundamental nature, function, development, and use of formal models in science and technology. In its most general sense, a model is a proxy. A model is one entity used to represent some other entity for some well-defined purpose. Examples of models include: (1) An idea (mental model), such as the internalized model of a person's relationships with the environment, used to guide behavior. (2) A picture or drawing (iconic model), such as a map used to record geological data, or a solids model used to design a machine component. (3) A verbal or written description (linguistic model), such as the protocol for a biological experiment or the transcript of a medical operation, used to guide and improve procedures. (4) A physical object (scale model, analog model, or prototype), such as a model airfoil used in the wind-tunnel testing of a new aircraft design. (5) A system of equations and logical expressions (mathematical model or computer simulation), such as the mass- and energy-balance equations that predict the end products of a chemical reaction, or a computer program that simulates the flight of a space vehicle. Models are developed and used to help hypothesize, define, explore, understand, simulate, predict, design, or communicate some aspect of the original entity for which the model is a substitute.

Formal models are a mainstay of every scientific and technological discipline. Social and management scientists also make extensive use of models. Indeed, the theory of models and modeling cannot be divorced from broader philosophical issues that concern the origins, nature, methods, and limits of human knowledge (epistemology) and the means of rational inquiry (logic and the scientific method).

Models are usually more accessible to study than the system modeled. Changes in the structure of a model are easier to implement, and changes in the behavior of a model are easier to isolate, understand, and communicate to others. A model can be used to achieve insight when direct experimentation with the actual system is too dangerous, disruptive, or demanding. A model can be used to answer questions about a system that has not yet been observed or built, or even one that cannot be observed or built with present technologies.

Specific models developed in different disciplines may differ in subject, form, and intended use. However, basic concepts such as model description, validation, simplification, and simulation are not unique to any particular discipline. Model theory seeks a formal logical and axiomatic understanding of the underlying concepts that are common to all modeling endeavors.

General and mathematical systems theory have stimulated many of the important developments in model theory. Mathematical models are particularly useful, because of the large body of mathematical theory and technique that exists for the study of logical expressions and the solution of equations. The power and accessibility of digital computers have increased the use and importance of mathematical models and computer simulation in all branches of modern science and technology. A great variety of programming languages and applications software are now available for modeling, computational analysis, and system simulation. See Digital computer, Simulation, Systems analysis, Systems engineering

References in periodicals archive ?
Selman, "Generating satisfiable problem instances," in Proceedings of the 17th National Conference on Artificial Intelligence (AAAI '00), pp.
It is shown in Meuss and Schulz [1998] that every consistent tree query is satisfiable if we do not restrict the interpretation of relation symbols in R.
Hence, an expression E over R is satisfiable if and only if the expression E' over S obtained from E by replacing each occurrence of R by [[pi].
If f is satisfiable, the decision procedure constructs a tableau from which a model M of f can be constructed.
Remarkably, computational experiments by Selman and his coworkers recently showed that in 2-SAT problems, the transition from satisfiable to unsatisfiable is continuous.
92) As for the cognitive and volitional prongs, the Model Penal Code test essentially restates the satisfiable cognitive prong of the M'Naghten test and the satisfiable volitional prong of the irresistible impulse test.
In many cases either or both of these assumptions may not be satisfiable.
If there are one or more satisfiable calls on available objects handled by a given processor, one of them will proceed.
The experiences related here are the result of a collaborative project carried out by staff at Frost Electroplating and the School of Computing and Information Technology at Wolverhampton polytechnic, following identification of an advanced systems need which was not satisfiable by normally used techniques.
This case, when added to prior loan cases, leads to the conclusion that the shareholder will be deemed to receive a direct benefit if the inter-corporate transfer eliminates a liability satisfiable from shareholder funds.
SPARKBridge preview for Windows SPARKBridge - a bridge between the SPARK tools and Satisfiable Modulo Theories (SMT) solvers - was initially introduced as a GNU/Linux-only preview in SPARK Pro 9.
2) THN:* typed higher-order form nontheorems (axioms with a countersatisfiable, that is, unprovable conjecture, and satisfiable axiom sets.