Why Do Logicians Sort the World into Kinds?
Euclid’s Puzzle: Two Kinds of Things
Over two thousand years ago, the Greek mathematician Euclid wrote a rule that sounds obvious: “A straight line can be drawn joining any two points.” But if you try to squash that rule into the tight symbols of logic, you immediately hit a problem. Points and lines are different kinds of things. A point isn’t a tiny line, and a line isn’t a stretched-out point. If you treat them as the same kind of object, you start saying nonsense — like asking how long a point is.
Logicians call these different kinds sorts. When you keep sorts separate, a point variable (let’s call it x) lives in its own world, and a line variable (call it X) lives in another. You can then write Euclid’s rule in a clean way: “For any two distinct points, there is exactly one line joining them.” In the background, you silently remember that “joining” only makes sense between a line and two points — never between two lines or a point and a banana. That’s the heart of many-sorted logic, a way of organizing reasoning so that every term knows what sort it belongs to.
This sorting isn’t just fussy. Without it, logic becomes a dangerous game of mixing apples and oranges — and in mathematics, that can lead to real mistakes.
Sorts: The Labels on Your Logic Box
Imagine you’re playing a video game. The inventory holds swords, shields, and health potions. Some actions only work with certain sorts of items — you can’t drink a sword, and you can’t equip a potion. The game’s code avoids crashes by keeping the sorts distinct. Many-sorted logic does the same for reasoning: it gives every variable and every function a sort-tag, like a label on the bottom of a toy.
In standard first-order logic, there’s just one big bucket for everything. Variables range over a single universe of all things. That’s fine when you’re talking only about numbers, but most interesting problems involve different kinds. Want to talk about a book sitting on a shelf? You need a sort for physical objects, a sort for locations, and a relation on that pairs the right sorts. Mix them up, and you might unknowingly ask whether “on” can hold between two locations, which is nonsense.
Many-sorted logic lets you declare these boundaries. A structure in many-sorted logic has one non-empty domain for each sort. A predicate symbol like “existsAt” might connect an object and a time — its rank spells out the allowed sorts. This sounds technical, but it’s just the rulebook for who can dance with whom.
The mathematician Hao Wang (1921–1995) first laid out the rules for many-sorted logic in the 1950s. He showed that you can take any argument involving multiple sorts and give it a clean, formal shape without cheating. A bit later, Leon Henkin (1921–2006) proved something startling: many-sorted logic isn’t a wild new beast. It’s as well-behaved as the ordinary one-sorted logic you learn in an intro class. And that turns out to matter a great deal.
The Proof That Many Sorts Are Safe
Logicians love guarantees. They want to know that if a sentence is true in every possible structure you can imagine, then there is a step-by-step proof of it using the basic rules of the game. This property is called completeness. Ordinary first-order logic has it. But when Hao Wang and others started playing with many-sorted logic, a worry crept in: would the extra sorting break completeness? Would there be true sentences about points and lines that no proof could ever catch?
Henkin answered with a careful construction that is still taught today. He showed that a consistent set of many-sorted formulas can always be beefed up to a “maximal” set that contains witnesses — terms that stand for the objects the formulas talk about. From that maximal set, you can build a tiny universe for each sort, just by looking at the names the set provides. The result is a model made of words — a structure where every true statement has a proof.
Why does this matter? Because completeness also gives you other powerful guarantees: compactness (if every finite chunk of a theory has a model, the whole infinite theory has one) and Löwenheim-Skolem (if a theory has a model, it has a countable one). These properties mean many-sorted logic is as safe and trustworthy as the single-sort version. You lose nothing by sorting.
In fact, Henkin’s work revealed a deeper point: many-sorted logic is not a genuine extension of first-order logic. You can translate any many-sorted sentence into an ordinary one-sorted sentence by adding unary predicates to label the different sorts. For example, you rewrite “For every point x…” as “For every x, if x is a point then…” The translation yields the same consequences. So many-sorted logic is really a more convenient way of writing down the same underlying ideas — like using a stencil instead of drawing freehand.
A Master Key for Other Logics
One of the most powerful features of many-sorted logic is that it can act as a translator for other logics. Philosophers and computer scientists have invented dozens of special-purpose logics over the years: modal logic for necessity and possibility, propositional dynamic logic for computer programs, and second-order logic that lets you quantify over properties, not just individuals. Each of them comes with its own symbols, its own rules, and its own puzzles about completeness.
Many-sorted logic swallows them all. The trick is to add new sorts that capture the extra ingredients. Take basic modal logic. In a modal model, you have a universe of possible worlds and a relation of accessibility between them. The sentence “Necessarily, it is raining” means “In every world you can reach from here, it is raining.” By giving worlds their own sort and using a membership relation, you can translate every modal formula into a many-sorted first-order formula whose truth conditions match exactly. The same strategy works for propositional dynamic logic, where you need a sort for binary relations representing computer programs.
Second-order logic, which on the surface seems much stronger than first-order logic, also submits to this treatment. You introduce a sort for individuals and a family of sorts for relations of various arities. Then you add a membership predicate to connect them. When you restrict the universes for relation sorts to those closed under definability — the so-called general semantics — second-order logic becomes a complete theory inside many-sorted logic. Leon Henkin pioneered this approach in the 1950s, and it remains the standard way to study second-order logic without losing the nice logical properties.
This unifying power means that a single theorem prover that knows many-sorted logic can check arguments from all these other logics. Instead of building a new proof engine for each new logic, researchers can translate the problem into many-sorted form and let a single tool do the work. The theorem provers LEO-II and LEO-III, for instance, use exactly this trick to cooperate with first-order reasoning tools.
Why Sorting Still Matters Today
You might think that sorting is a dusty, academic idea — useful only to logicians in tweed jackets. But it’s baked into the software that surrounds you. Every time a search engine reasons that “Paris” could refer to a city, a person, or a movie, it must keep those sorts from bleeding into one another to avoid absurd answers. Artificial intelligence systems that plan tasks or understand language rely on type systems descended straight from many-sorted logic.
Back in the classroom, Euclid’s ancient division between points and lines isn’t just a math lesson. It’s a habit of mind. When you sort your thoughts — when you ask yourself, “What kind of thing am I talking about?” — you’re doing what many-sorted logic does on paper. The next time you argue with a friend about whether a video game character “deserves” a second chance, you’re already using sorts: you’re distinguishing a fictional agent from a real person, a decision from a consequence. Logic is the art of drawing those boundaries so clearly that confusion has no place to hide.
Henkin and Wang showed that you can draw those lines with perfect safety. You don’t weaken your reasoning by sorting; you strengthen it. And with that guarantee, many-sorted logic has become the quiet foundation under a lot of modern science — not the flashiest idea, but one that stops the whole structure from wobbling.
Think about it
- If you invented a new board game with wizards, potions, and spells, what sorts would you need, and what mixing rule would be most important to keep the game from falling apart?
- Suppose a computer could translate every sentence you say into many-sorted logic before answering. What everyday misunderstanding might it clear up?
- Why do you think mathematicians resisted sorting for so long, even though they constantly talked about points, lines, and numbers as different kinds of things?
