Skip to content
Philosophy for Kids

Is 'He Is Killing All of Them' True? The Game of Model Theory

A sentence that can’t decide if it’s true

The sentence 'He is killing all of them' hides a mystery: who is he, and what is he killing?

Suppose someone says, “He is killing all of them.” Is that sentence true or false? You can’t tell — because you don’t know who “he” is, and you don’t know what “them” refers to. The words are missing their interpretation: the extra information that pins down what the words are about. If I add that “he” means Alfonso Arblaster of 35 The Crescent, Beetleford, and “them” means the pigeons in his loft today, suddenly the sentence has a definite truth. It’s true if Alfonso is killing all those pigeons; false otherwise.

In model theory, when an interpretation makes a sentence true, we call that interpretation a model of the sentence. We say the model satisfies the sentence, written with the symbol (a kind of double turnstile). So if I is the interpretation with Alfonso and today’s pigeons, and S is our sentence, we write I ⊨ S to mean “I is a model of S” — or more casually, “S is true in I.” This is model-theoretic truth: truth relative to a particular interpretation. The sentence on its own, without an interpretation, is like a question waiting for an answer.

An interpretation has to do two jobs. It must say what objects certain words point to (like “Alfonso” and “the pigeons”). And if the sentence uses words like “all” or “some” — these are quantifiers — the interpretation must say what class of things the quantifier ranges over. In our example, “all of them” ranges over the class of pigeons in Alfonso’s loft today. A structure is a package that bundles together the objects, the classes, and the labels that connect them to the right words. If the same class is used for every quantifier, that class is called the domain or universe of the structure. If different quantifiers need different classes — say “all diseases” and “all birds” — the structure is many-sorted and has several domains.

Notice that a structure includes a specific moment in time (today’s pigeons) and could be different tomorrow. Model theory can handle that too, by indexing truth to a time or a possible world. But the basic idea remains: truth is a match between a sentence and a structure.

How a sentence can define a whole class of things

Even a legal definition of a trust works like a model: it labels the people and the property in a specific pattern.

Once we see that a sentence carves its interpretations into two groups — models and non-models — we can use sentences to define classes of structures. Take the sentence: “The first person has transferred the property to the second person, who thereby holds the property for the benefit of the third person.” This sentence picks out a class of structures where the labels “first person,” “property,” “second person,” and “third person” are assigned in just that arrangement. Lawyers call that class a trust. In model theory, we write Mod(S) for the class of all models of a sentence S.

The same trick works for a set of sentences. A theory (or axiom set) is a collection of sentences, and Mod(T) is the class of structures that are models of every sentence in T. When a theory defines a class this way, we say the theory axiomatises the class. For example, here are four sentences about a world with an operation ”+”, a special element “0”, and an operation ”-”:

  • For all x, y, z: (x + (y + z)) = ((x + y) + z).
  • For all x: x + 0 = x.
  • For all x: x + (-x) = 0.
  • For all x, y: x + y = y + x.

The structures that model all four sentences, with a domain that contains 0 and is closed under + and -, are exactly what mathematicians call abelian groups. The integers with ordinary addition are one model; so are the hours on a clock face if you treat 12 as 0. The sentences don’t tell you which group you’re in — only that it must obey those rules. The symbols +, -, 0 are nonlogical constants; together with the quantifiers, they form the signature of the structure. By fixing the signature, we can talk about whole families of structures at once. This is how model theory formalises the everyday mathematical habit of saying “Let G be a group.”

There is a second kind of defining, one that works inside a single structure. Fix a structure A, and take a formula with some free variables. Assigning elements of A to those variables may make the formula true; the set of satisfying assignments defines a relation on A. In the integers with addition, the formula v₁ + v₁ = v₂ defines the binary relation “v₂ is double v₁.” This is a first-order definable relation. By weaving together sentences, axioms, and definable relations, model theory gives mathematicians a precise language for describing patterns.

Checking arguments with class diagrams

Boole showed that checking an argument's validity is like checking relationships between sets.

Before the mid-19th century, logic textbooks taught students to spot valid arguments by matching them to standard forms — a tricky business, because forms that look valid sometimes aren’t. Then George Boole (1815–1864) showed a better way. His key move was to translate an English argument into a claim about classes, and then check whether the class relationships force the conclusion.

Consider the argument:

  • All monarchs are human beings.
  • No human beings are infallible.
  • Therefore, no infallible beings are monarchs.

Boole would treat P, Q, R as the classes of monarchs, humans, and infallible beings. The premises become “P is a subclass of Q” and “Q and R have nothing in common.” The conclusion is “R and P have nothing in common.” In modern notation, this is (P ⊆ Q), (Q ∩ R = ∅) ⊨ (R ∩ P = ∅). The double turnstile here expresses model-theoretic consequence: every structure (here, every assignment of classes) that makes the premises true also makes the conclusion true. If that holds, the argument is deductively solid.

Boole’s insight reshaped logic textbooks. Instead of memorising dozens of fallacies, students learned to formalise arguments and test for consequence. But there is a catch: if you formalise an argument poorly, the consequence test might fail even though the original argument was genuinely valid — you just missed the deeper meaning of the concepts. An old example runs: “There is a father; therefore there is a child.” If you write it as ∃x Father(x) → ∃y Child(y), the consequence doesn’t hold, because the symbolisation ignores the built-in relationship. To make the validity visible, you must analyse the meanings of “father” and “child.” Model theory gives a clean test, but it depends on having captured the right structure in the first place.

Playing games to tell structures apart

In the back-and-forth game, Spoiler tries to find a difference, Duplicator tries to match it — if Duplicator always wins, the two structures are logically identical.

If you have two databases that look similar, how can you prove that a certain question can’t tell them apart? Model theory answers with a family of tools for measuring expressive strength — the power of a language to distinguish different structures. The most playful of these tools is the back-and-forth game, invented by Andrzej Ehrenfeucht and Roland Fraïssé.

Imagine two structures, A and B, and two players: Spoiler and Duplicator. Spoiler wants to show that the structures are different; Duplicator wants to show they are alike. On each turn, Spoiler picks an element from either structure, and Duplicator must pick a matching element from the other structure. After n turns, they have two small sequences of elements. If those sequences satisfy exactly the same atomic relationships (for example, if one pair is less-than another), Duplicator survives that round. If she has a strategy to survive any number of turns no matter what Spoiler does, then no first-order sentence can distinguish A from B.

These games are remarkably flexible. They work equally well on finite structures (like database states) and infinite ones, and they can be adapted to many non-first-order languages. A famous theorem by Per Lindström (1969) used such games to characterise first-order logic itself: it’s the unique logic that can capture complex finite patterns yet is hopeless at discriminating one infinite size from another. The expressive-strength toolkit helps computer scientists design query languages that can ask exactly the questions a database can answer, no more and no less.

Inventing impossible numbers that actually work

Infinitesimals are numbers greater than 0 but smaller than every fraction — they only exist in special models of arithmetic.

In the 1600s, Gottfried Wilhelm Leibniz (1646–1716) built calculus using infinitesimals — numbers that are greater than zero but smaller than 1/2, 1/3, 1/4, and every other positive fraction. There was just one problem: no real number has that property. By the 19th century, mathematicians had replaced Leibniz’s infinitesimals with limits, a method that felt clunky but was logically sound.

Then Abraham Robinson (1918–1974) found a way to bring infinitesimals back. He started with the structure of the real numbers ℜ, including all the usual operations and named constants. He wrote down the complete first-order theory of ℜ — every true sentence. Because first-order logic is too weak to express “there are no infinitesimals,” Robinson could add a new constant ε and a set of sentences saying “ε > 0” and “ε < 1/n” for every positive integer n. The compactness theorem (a property of first-order logic) guarantees that if every finite subset of this enlarged set of sentences has a model, the whole lot has a model. And indeed they do: the structure ℜ* that emerges is a model of exactly the same first-order truths as ℜ, but it contains infinitesimals.

Robinson showed that you can do calculus with ℜ*‘s infinitesimals using Leibniz’s simpler, more visual arguments, then translate the results back to ℜ. Because the translation preserves truth, the theorems hold for ordinary real numbers. This nonstandard analysis makes many proofs easier to grasp and has even been used to mechanise parts of Newton’s Principia.

Why interpretation games matter in your world

Model theory helps design the queries that find exactly the right information in a database.

You’ve probably never held a pigeon while shouting “He is killing all of them!” But you use interpretation every day. When you read a text, listen to a friend, or write a search query, you rely on an invisible background of assumptions about what the words refer to and what classes they range over. Model theory makes those assumptions explicit.

Computer scientists use model-theoretic ideas to build database query languages that can tell what a question means just by looking at the structure of the data. The back-and-forth games that compare expressive strength are not just for logicians — they help decide whether one query language is powerful enough for a real-world task. Even in cognitive science, researchers debate whether our mental representations work like little model-theoretic structures, helping us reason about possibilities.

So the next time a sentence puzzles you because something crucial is missing, you’re doing model theory. You’re asking: what structure would make this true? And that question is at the heart of logic, mathematics, and the way we make sense of the world.

Think about it

  1. Suppose you hear someone say, “That’s not fair!” but you don’t know what situation they’re talking about. Can you decide whether the sentence is true? What extra information would you need?
  2. If two computer databases contain exactly the same facts but organise them differently, can a cleverly written question ever tell them apart? How would you test it?
  3. Leibniz found infinitesimals incredibly useful, but mathematicians said they didn’t exist. Is it okay to use an “impossible” object if it helps you discover true things about real numbers? Where would you draw the line?