The conclusion is what survives the erasing

Lewis Carroll spent his last years on logic, and the puzzles he wrote for it are still the best way in. Here is one of the shortest, from Symbolic Logic of 1896:

Babies are illogical. Nobody is despised who can manage a crocodile. Illogical persons are despised.

What follows? Nothing about logic, or crocodiles, or contempt on its own; the answer relates the two classes that each appear only once — babies and crocodile-managers — and it is babies cannot manage crocodiles. A chain of premises like this is a sorites, and twenty-four out of two hundred and fifty-six set it aside as “a chain of two syllogisms, outside the 256”. It is also exactly the kind of argument that one thing in each region is enough showed the regions of a diagram can decide. What is new is not whether it can be decided but how the conclusion is found: by drawing every class, and then rubbing out the ones the conclusion is not about.

Four classes on one picture #

Four classes need sixteen regions, and four circles cannot do it: the most they manage is fourteen. Four ellipses can, and the figure uses the arrangement that essay found, with every one of the sixteen combinations present as a single region.

Each premise is a statement that some regions are empty. Babies are illogical empties every region that is inside B and inside L — four of them, one for each way the other two classes can go. Nobody is despised who can manage a crocodile empties the four regions inside both M and D. Illogical persons are despised empties the four regions outside both L and D, and one of those is the region outside every ellipse: the premises say there is nobody who is neither logical nor despised. Twelve regions named, one named twice, eleven shaded.

The conclusion is a statement about regions too. Babies cannot manage crocodiles says that every region inside both B and M is empty — the four filled in red. And all four are already shaded. The conclusion was on the page the moment the premises were, as a fact about four regions; the question the puzzle poses is how to see it without knowing in advance which regions to look at.

For four classes it can be checked outright. There are $2^{16} = 65{,}536$ ways of occupying sixteen regions, and every one that respects the premises leaves the B-and-M regions empty. That is the verdict of the one-per-region method, and it establishes the conclusion. It does not find it — the search had to be told what to test.

Rubbing out a class #

Carroll’s own method, and Boole’s before him, is elimination. The conclusion mentions B and M and nothing else, so L and D are middle terms — present in the premises to link things, absent from the answer. Erase them one at a time and see what remains.

Erasing a class merges regions in pairs. Every region of the three classes B, D and M is two regions of the full picture — the part inside L and the part outside it — and after L is erased they are one region. The merged region is empty only if both halves were. If either half could hold something, then something could be in the merged region, and a diagram without L has no way to say which half it would be in.

The middle panel is the result, and it says two things no premise stated. Every region of B outside D is shaded: every baby is despised, because a baby is illogical by the first premise and an illogical person is despised by the third. And every region where M and D overlap is shaded, which is the second premise carried over unchanged. The region of babies who are despised and cannot manage crocodiles stays clear — its illogical half was never ruled out — and the rule found all of this without any reasoning in words: it asked, for each merged region, whether both halves had been empty.

Erase D next and the right-hand panel appears: two circles, B and M, with a single region shaded — their overlap. That is the conclusion, and it arrived without being guessed. Erase every class the question is not about, and what remains is everything the premises say about the rest.

Why both halves must be empty #

The rule has an algebraic form, and it is Boole’s. Write a class as a variable that is 1 for things in it and 0 for things outside, and a set of premises as a single condition $f = 0$, where $f$ is 1 on exactly the regions the premises rule out. Boole showed in 1854 that from $f(x, \ldots) = 0$, the strongest consequence not mentioning $x$ is

$$f(1, \ldots)\, f(0, \ldots) = 0.$$

The two factors are the two halves — the premises with $x$ set to “inside” and with $x$ set to “outside” — and their product is 1 exactly where both halves are ruled out, so the equation says that those merged regions, and only those, are empty. That is the rule in the figure, written as arithmetic, and it is the reason the method is complete: nothing true about the remaining classes is lost, because a region of them is empty only when both halves are.

It is also why the order of erasing does not matter. Erasing L then D leaves a region of B and M empty when all four of its lifts to the full picture were empty; erasing D then L leaves it empty on exactly the same condition. The middle panel changes with the order, and the last one does not. Erasing D first gives a different middle picture, on B, L and M: babies are illogical, which is the first premise again, and every crocodile-manager is logical, which is new — a crocodile-manager is not despised, and anyone not despised is logical. Erasing L from that leaves the same overlap of B and M shaded. The two orders are the chain of reasoning read from its two ends: from babies forward to their being despised, or from crocodile-managers backward to their being logical, meeting in the middle at the conclusion.

And existence runs the other way. A premise such as some babies are logical puts a mark in a region rather than shading one, and after erasing a class the merged region is occupied if either half was — a thing in one half is a thing in the merge. Emptiness needs both halves; occupancy needs one. That asymmetry is the whole difference between universal and existential premises, and it is the diagrammatic form of the rule that a universal statement becomes weaker under projection while an existential one survives it.

Carroll’s board and counters #

Carroll did not use Venn’s circles. In The Game of Logic of 1887 he drew a square divided into quarters for two classes and a smaller square inside it for a third, so that every combination was a rectangle, and he played the premises onto it with counters — a red counter for “something is here”, a grey one for “nothing is here”. A syllogism was a board with premises set out on it; the conclusion was read by taking the counters off the middle term’s square and seeing what the remaining rectangles held.

The rule for taking counters off is exactly the erasing rule. A rectangle of the two remaining classes gets a grey counter only if both of the small rectangles it contains had grey counters; it gets a red counter if either had a red one. Carroll stated it for his board, Boole had stated it as algebra thirty years earlier, and the diagrams above state it for ellipses. The three are one rule, and Carroll’s contribution was to make it a game that children could play — which he did, at a girls’ school in Oxford, with the board printed in the book and the counters in an envelope at the back.

His squares also answer the problem that stops circles at three. A square divided in half by each class in turn — left and right, top and bottom, then smaller squares inside — gives every combination as a rectangle for any number of classes, at the cost of the symmetry and the single closed curve per class that make Venn’s diagrams easy to read. It is the same trade the map that puts neighbours side by side makes for truth tables: give up curves, keep a grid, and every combination has somewhere to go.

The same deduction written as clauses #

Every premise of this kind says “every X is Y”, which is the same as saying that each thing is not X, or Y. Written that way the three premises are three clauses: $\neg B \vee \neg L$, $\neg M \vee \neg D$ and $L \vee D$. And a proof with one rule describes exactly one thing to do with clauses: take two that disagree about a single letter and combine them into one that forgets it. $\neg B \vee \neg L$ and $L \vee D$ disagree about L, and combine into $\neg B \vee D$. That and $\neg M \vee \neg D$ disagree about D, and combine into $\neg B \vee \neg M$ — babies are not crocodile-managers.

Each resolution step is one erasure. Resolving on L produces exactly the consequences that survive erasing L, and the figure’s erasures were checked against that. The correspondence is not a coincidence of this puzzle: Davis and Putnam built a procedure for satisfiability on it in 1960, eliminating one variable at a time by resolving every clause containing it against every clause containing its negation — Boole’s elimination, a century on, run by a computer. Carroll’s sorites was the same algorithm, run by a mathematician with a pencil and an ellipse.

A second puzzle, and a path through it #

Carroll’s ducks puzzle has the same shape with the classes rearranged: no ducks waltz; no officers ever decline to waltz; all my poultry are ducks. The middle terms are ducks and waltzers, and the answer relates poultry and officers: my poultry are not officers.

Read as implications, the premises form a chain: poultry are ducks, ducks do not waltz, and anyone who does not waltz is not an officer — the contrapositive of officers waltz. $P \to D \to \neg W \to \neg O$. The conclusion is the two ends of the chain. The crocodile puzzle is a chain too: $B \to \neg L \to D \to \neg M$.

That is not how every set of premises looks, but it is how every set of “every X is Y” premises looks, because each is a clause of two letters, and two literals make an arrow: a two-letter clause is an implication, and a set of them is a directed graph on the literals. A sorites is a path in that graph, and its conclusion is the arrow from the start of the path to its end. Finding the conclusion is finding the path, which takes time proportional to the number of premises, however many classes there are. The diagram needs $2^n$ regions for $n$ classes; the path needs $n$ steps.

What the ellipses cannot hold #

Four classes is the end of the drawing. Carroll’s own puzzles go much further — the best known has ten premises about the animals in a house and concludes that its narrator always avoids a kangaroo — and a diagram for eleven classes would need 2,048 regions in a single connected picture. Four circles cannot do it shows that curves exist for any number of classes, but no reader could shade one. The elimination works there anyway, on the clauses, and the diagram is where the method is understood rather than where it is used.

The erasing is exact, the drawing of it is not. Each shaded region was computed from the premises, and the merges from the rule; the regions themselves are traced contours of ellipses at a finite resolution, and the thinnest of the sixteen are thin enough that shading them is a matter of a few pixels.

And elimination is cheap only here. For premises of the form “every X is Y” the clauses have two letters and resolution never makes them longer. For richer premises — “everything that is X and Y is Z” — clauses grow as letters are eliminated, and eliminating one letter can square the number of clauses. Davis and Putnam’s procedure was abandoned for exactly that reason within two years, in favour of a search that branches instead of eliminating — and a failed search is a proof shows that the branching search, when it fails, has built a resolution proof all the same.

The growth is easy to see in a small case. Add the premise every logical person who is despised is a baby — a clause of three letters, $\neg L \vee \neg D \vee B$. Resolving it against $L \vee D$ on L gives $D \vee \neg D \vee B$, which says nothing; against $\neg B \vee \neg L$ it cannot be resolved on L at all, since both contain $\neg L$. Three-letter premises produce resolvents of up to four letters, those produce longer ones, and the diagram’s version of the same fact is that erasing a class from a picture with many shaded regions can leave a pattern with no short description.

Still open: whether anything beats trying every assignment #

The branching search that replaced elimination — the DPLL procedure, the ancestor of every modern satisfiability solver — still takes time exponential in the number of variables on the worst inputs. So does every other known method. For clauses of three letters the best algorithms run in about $1.31^n$ steps rather than $2^n$, but for clauses of unbounded length nothing is known that beats $2^n$ by more than a vanishing margin.

The strong exponential time hypothesis, stated by Impagliazzo and Paturi in 2001, says that nothing can: for every $\varepsilon > 0$ there is a clause length at which no algorithm runs in time $2^{(1-\varepsilon)n}$. It is unproved, and a great deal of modern complexity theory is conditional on it. Carroll’s chains are the easy corner of the problem — two letters per clause, a path in a graph — and the rest of it is where elimination blows up, branching guesses, and nobody knows whether anything fundamentally better exists.

The clauses that make the question hard are known by example. More things than boxes writes the pigeonhole principle as clauses — each pigeon in some hole, no two in the same — and every resolution proof that they are contradictory has exponential length. Elimination and branching both fail on them for the same reason, and no premise of Carroll’s kind appears anywhere in them.

Rubbing out what is not asked about #

The conclusion of a set of premises is not a separate thing to be discovered. It is the premises themselves, with every class the question is not about erased — and erasing is mechanical: a region survives as empty when both its halves were. On a diagram that is a merge of shaded regions; in Boole’s algebra it is setting a variable to 1 and to 0 and multiplying; in clause form it is resolution; and for premises of Carroll’s kind it is walking a path of implications from one end to the other.

The picture and the calculus earn their keep differently. The diagram makes it obvious why the rule is right — a merged region can hold something if either half can — and useless beyond four classes. The clauses make the rule mechanical and scale to any number of classes, and hide why it works. Carroll’s board sits between them, which is perhaps why it was written for children and used by nobody else.

When the answer is about fewer things than the question, eliminate the rest — and look for the rule that says what survives an elimination. Here it is one line, the same line in four notations, and the puzzle about babies and crocodiles is simply its smallest non-trivial case.