Model-theoretic semantics

Model-theoretic semantics is the study of how formal languages map onto mathematical structures — how the symbols, sentences, and inference rules of a logical system acquire meaning through interpretation in a domain of objects. In this framework, a language is not merely a system of rules (as in proof-theoretic semantics); it is a tool for describing possible worlds, mathematical universes, and structured domains. The meaning of a sentence is its truth conditions: the conditions under which it is true in a given model.

The approach was pioneered by Alfred Tarski in the 1930s with his truth-definition for formalized languages, and it has become the dominant framework for logic, linguistics, computer science, and foundations of mathematics. Where proof theory asks "what can be derived?" model theory asks "what can be true?" — and the gap between these questions is precisely the territory where Gödel's incompleteness theorems operate.

The Basic Architecture

A model-theoretic interpretation requires three components: a formal language (with syntax specified by a grammar), a domain of discourse (a set of objects), and an interpretation function that maps symbols to objects and relations in the domain. A sentence is satisfied in a model if the objects and relations assigned to its constituent symbols stand in the configuration the sentence describes.

This architecture makes semantics compositional: the meaning of a complex expression is built from the meanings of its parts through the syntactic structure that combines them. The sentence "Every cat sleeps" is true in a model just when every object in the domain that satisfies the predicate "cat" also satisfies the predicate "sleeps." Predicate logic provides the canonical formalism for this construction, though natural language semantics in the tradition of Richard Montague extends the framework to handle intensional contexts, modal operators, and quantifier scope ambiguity.

Model Theory and the Foundations Crisis

Model-theoretic semantics emerged from the same foundational crisis that produced logicism, formalism, and mathematical intuitionism. When Bertrand Russell and David Hilbert sought to ground mathematics in formal systems, they needed a way to connect those systems to the mathematical structures they were supposed to describe. Tarski's truth definitions provided the bridge: a formal system could be studied not only by what it proves (proof theory) but by what it can be true of (model theory).

This bridge has structural implications that go beyond technical convenience. The compactness theorem and the Löwenheim-Skolem theorem — fundamental results of classical model theory — show that first-order logic cannot pin down infinite structures with complete precision. Any first-order theory with an infinite model has models of every larger infinite cardinality, and if every finite subset of a theory has a model, the whole theory has a model. These theorems are not curiosities; they are constraints on what formal languages can capture. They imply that no first-order formalization of mathematics can uniquely determine the intended model — a result that fuels mathematical platonism (there are many models, but we somehow pick the right one) and formalism (the model doesn't matter, only the syntax does) alike.

Beyond First-Order Logic

The limitations of first-order model theory motivated the development of richer frameworks. Possible worlds semantics, introduced by Saul Kripke and developed by Montague, extends model theory to handle modal operators ("necessarily," "possibly") by evaluating sentences not against a single model but against a set of possible worlds connected by accessibility relations. Intensional logic, in this framework, assigns to each expression not just an extension (what it refers to in the actual world) but an intension (a function from possible worlds to extensions).

In computer science, denotational semantics applies model-theoretic methods to programming languages, treating programs as functions from input domains to output domains. The Curry-Howard correspondence blurs the line between proof theory and model theory by treating proofs as programs and propositions as types — a synthesis that suggests the proof-theoretic/model-theoretic distinction may not be as fundamental as the twentieth century assumed.

The Systems View

Model-theoretic semantics is rarely discussed as a systems framework, but it is one. A model is a system — a structured domain with relations, functions, and constraints. A formal language is a description language for that system. The interpretation function is the interface between description and described. The enterprise of model theory is, at bottom, the enterprise of building interfaces between symbolic systems and structured worlds.

This systems perspective exposes a blind spot in standard presentations. Model-theoretic semantics typically assumes a fixed, pre-given domain of interpretation. But in complex systems, ecosystems, markets, and distributed systems, the domain itself is dynamic — the objects, relations, and even the ontology of what exists changes as the system evolves. Standard model theory has no native apparatus for handling ontological change during interpretation. Dynamic semantics and game-theoretic semantics are partial responses, but the integration of model theory with genuinely dynamic, self-modifying systems remains incomplete.

The deeper challenge: if model theory is the study of how formal descriptions map onto structured domains, then a self-modifying system — one where the domain changes in response to the descriptions applied to it — requires a model theory of second order. Not a model of a system, but a model of a system that models itself. This is where model-theoretic semantics touches circular causality, autopoiesis, and the foundations of any system capable of representation.

_Model theory assumes that structures sit still while we describe them. The most interesting structures do not._