A formula is a corner of a cube

A formula built from three letters says something about eight cases, and nothing else about anything.

That sentence is the whole of propositional logic and it is worth slowing down over, because it is much stronger than it looks. It does not say a formula is summarised by its table. It says a formula is its table, in the sense that any two formulas with the same last column are interchangeable everywhere: substitute one for the other inside any larger formula and no row of any table anywhere changes. Whatever else a formula might seem to carry — how it was written, which connectives it used, how long it is — none of it survives into the only thing that can be asked about it.

Why the table is a complete answer and not a summary #

Compare this with almost every other object on this site. A circle is not its circumference; a graph is not its degree sequence; a number is not its residue modulo seven. In each of those, the invariant throws information away, and throwing information away on purpose is what makes it useful.

Here nothing is thrown away. The table is not an invariant of the formula, it is a transcription of it into a form with no redundancy left. Two formulas with the same table cannot be told apart by any question the language can ask, because every question the language can ask is a bigger formula, and a bigger formula’s value is computed from its parts’ values row by row.

That is a property of the connectives rather than of formulas. Each of ∧, ∨, ¬, → is truth-functional: the value of the whole is a function of the values of the parts, with nothing else consulted. English is full of connectives that are not. “He fell because he was pushed” is not determined by whether he fell and whether he was pushed; “she believes it is raining” is not determined by whether it is raining. Ordinary language works with those and this system does not, and that restriction is exactly what buys the finite table.

So the first thing to notice is that the subject begins by choosing a small language on purpose. Everything provable here is provable because the language was made narrow enough to enumerate.

Eight rows, and the shape they make #

A list of eight rows is correct and almost unreadable. The rows are in an order — counting up in binary — and that order says nothing about which rows are near which.

The fix is to stop treating an assignment as a row number and start treating it as a position. Three letters, each true or false, is a point in a three-dimensional grid of two positions per axis, which is to say a corner of a cube.

The edges now carry meaning that the table’s row order did not. Two corners joined by an edge differ in exactly one letter, so an edge is the question what if this one changed and nothing else did. That is the question every piece of reasoning about a formula actually asks, and in a list of rows it is scattered: row 3 and row 7 are neighbours in this sense and four rows apart on the page.

Look at the filled set in the figure. It is a face of the cube with one corner missing — not a random four corners out of eight but a shape with a description. Formulas that can be written shortly have simple shapes here, and that is a fact about the shapes rather than about the writing, which is the subject of the map that puts neighbours side by side.

Two things that show up immediately #

Once a formula is a set of corners, two of the field’s central questions become properties of a set.

A tautology is all the corners. A formula true in every row is one whose set is the whole cube. Nothing about the picture privileges it; it is one of the $2^8 = 256$ possible subsets of an eight-corner cube, and it happens to be the one with everything in it.

A contradiction is no corners at all, and the empty set is just as ordinary a subset as the full one. Everything between is a formula that is sometimes true and sometimes false, which is nearly all of them: there are $2^8 = 256$ formulas of three letters up to equivalence, of which exactly one is a tautology and exactly one is a contradiction.

That last count is worth pausing on, because it is the first place this subject does something unexpected. There are exactly 256 distinct formulas in three letters. Not 256 short ones, or 256 worth studying — 256 altogether, forever, however long a formula is allowed to get. Every formula anyone could write in the letters $p$, $q$, $r$ is equal to one of those 256, because it has a table and there are only 256 tables. Length is unbounded and meaning is not.

The consequence: every formula can be written the same way twice #

If a formula is a set of rows, then a formula can be rebuilt from its set of rows, and rebuilding is mechanical.

Take the rows that came out true. Each one describes a single assignment completely — $p$ true, $q$ false, $r$ true, say — and that description is itself a formula: $p ∧ ¬q ∧ r$, which is true at that row and nowhere else. String the descriptions of all the true rows together with ∨, and the result is true exactly where the original was.

That is disjunctive normal form, and the argument for it is a paragraph long because the table did all the work. Every truth function of $n$ letters is expressible, so the language is not missing anything: whatever function of eight rows anyone can imagine, some formula has it.

The figures on this page check the same fact from the other direction. Each one computes its column twice — once by walking the parsed formula, once by rebuilding the disjunctive normal form from the rows that came out true and evaluating that — and asserts they agree on every row. Two implementations agreeing across all eight rows is a check; a table compared with itself is not.

There is a mirror-image construction from the false rows giving conjunctive normal form, and the pair of them is the first instance of a habit this field has: the same object described by what it includes and by what it excludes, with the two descriptions the same length and neither preferred.

An aside on what “and” is doing here #

There is a step in all of this that is easy to walk past, and it is the step a first reader usually objects to.

Writing $p ∧ q$ for and looks like a definition of a familiar word. It is not. It is a decision to replace the familiar word with a function of two truth values that agrees with it in the cases where the familiar word is clear, and to work with the replacement afterwards. The two come apart quickly. Ordinary and is sensitive to order — “she got dressed and went out” is not the same claim as “she went out and got dressed” — while $p ∧ q$ and $q ∧ p$ have the same column and so are the same formula.

The same is true, more sharply, of $→$. Read as if … then, the row where $p$ is false and $q$ is true comes out true, which says that a false antecedent makes the whole conditional hold. Nothing in ordinary usage supports that: “if the moon is made of cheese then the Queen is a hatstand” is a joke rather than a truth. But once the connective has to be a function of the two columns, every row needs an entry, and any other choice makes $→$ into one of the fifteen other connectives — which is not a repair, it is a different word.

So the honest description is that this language is not an analysis of ordinary reasoning. It is a replacement for the fragment of ordinary reasoning that survives being made truth-functional, adopted because that fragment can be settled completely. What is lost is real, and two later essays are about people who went back for some of it: a logic that refuses to assume every question is already decided, and the frames that give necessarily a meaning the truth tables cannot.

How many connectives there are, which is also finite #

The same counting argument applies one level down. A binary connective is a function of two truth values, and a function of two truth values is a choice of output for each of four inputs.

Only about five of these have names anyone uses, and six of the sixteen ignore at least one of their inputs entirely — the two constants, $p$, $q$, $¬p$ and $¬q$. The others are the interesting ones, and it is worth noticing that the familiar names are not a natural class. ∧, ∨, → and ↔ are the ones ordinary language has words for; ↑ and ↓ are the ones with the most mathematical structure; and one of them is enough on its own, which is not something the list of names would suggest.

The count also settles a question that sounds open. Are there connectives nobody has thought of? No — not “none have been found”, but none exist, for two arguments, because sixteen tables is all the tables there are. A proposed new connective is a proposal to write one of these sixteen a different way.

The map, which is the table with the rows moved #

There is a third arrangement of the same eight rows, and it is worth meeting here because it is the one that makes the shape usable rather than merely visible.

The trick is the column order: $00$, $01$, $11$, $10$ rather than $00$, $01$, $10$, $11$. Counting order puts $01$ next to $10$, which differ in two letters; this order never does. It is a Gray code, and its only property is the one being used — consecutive entries differ in one place, including the wrap from the last back to the first.

What that buys is that the cube’s edges become adjacency on a flat grid. The picture is the cube with its surface cut open and laid out, so a face of the cube is a rectangle on the page, and the eye can see a rectangle. The satisfying set above is one $1×2$ block plus a $1×2$ block, and each of those blocks is a two-letter conjunction — which is the covering problem promised earlier, made visible.

The three arrangements are the same eight rows and they are good for different things: the table for deciding, the cube for understanding why adjacency matters, the map for actually finding a short formula. None is more correct than the others and the site treats all three as one object, which is why they come out of one generator with the same assertions behind them.

What the picture is for #

It is fair to ask what the cube adds, given that the table already decides everything.

Three things, and they get more important as the field goes on.

It makes locality visible. The interesting operations on formulas — simplification, resolution, the search a solver does — all move between assignments that differ in one letter. In the cube those are steps along edges. In the table they are jumps of varying length with no pattern.

It makes size a shape. A conjunction of $k$ literals picks out a subcube: fix $k$ coordinates, leave the rest free. So a short formula is a large flat piece, a long one is a small piece, and “find a short equivalent formula” becomes “cover this set with few big flat pieces” — a covering problem with a geometry, which is exactly what the next-but-one essay does with it.

It scales in the way the reader’s intuition should. Four letters is a cube of cubes and sixteen corners; ten letters is 1,024, and by twenty the set of corners is larger than anything that can be drawn or listed. The picture stops being drawable long before the problem stops being real, and knowing which structure the picture had is what survives past the point where it can be drawn.

That last figure is worth a second look, because it is the counterexample to the optimism of this essay. Exclusive-or’s set of corners is exactly as large as any other formula’s could be, and it contains no face, no edge, no flat piece bigger than a single corner. Every method that works by finding big flat pieces fails on it, and there are eight such formulas on four letters — parity and its negation, with the four-letter versions of each — sitting in a space of 65,536.

The scale of “all of them” #

The counting in this essay has been generous with the phrase all of them, and it is worth saying what it costs, because it is the reason none of this is the end of the story.

A truth table for $n$ letters has $2^n$ rows. That is fine at three and manageable at ten. At a hundred letters — which is a small formula by the standards of anything a computer is asked about — the table has more rows than there are atoms anyone has counted, so the method that settles every question in this essay settles nothing at all in practice.

So the field divides here, and the division is worth naming before it arrives. There is the question of what is true, which the table answers completely and finitely, and the question of what can be found out, which it answers only in principle. Everything in this collection’s logic field is on the first side of that line: a tableau closing, a syllogism being valid, an axiom holding on a frame. What it costs to actually decide any of them belongs to a different subject, with a different rule and a different kind of evidence — a cost is measured on a named machine rather than asserted — and this field is careful not to claim it.

What the table does give, and gives permanently, is a standard of correctness. Whenever something later in this field produces a verdict by another route — a proof tree, a diagram, a search — the honest test is whether it agrees with the table on the cases where the table can be computed. Every figure in this field is written to be checkable that way, and several of them are checked exactly that way as they are drawn.

Where the certainty comes from #

There is one more thing to take from this essay, and it is about the shape of the arguments rather than their content.

Everything settled above was settled by going through all the cases. Not by an insight, not by an algebraic manipulation, and not by a general theorem — by enumeration. Sixteen connectives, eight rows, 256 formulas. It is the least sophisticated method available and it is completely conclusive, because the thing being quantified over is finite and was made finite on purpose.

That is a trade, and the rest of this field is the story of what it buys and what it costs. When a question stays inside a finite space — which of the 256 syllogisms are valid, which regions a family of curves cuts the plane into — the answer is available by exhaustion and is not open to argument. When the question escapes the finite — is every real number on this list, does this proof system prove everything true — enumeration is unavailable, and something else has to be found. What is found in those cases is nearly always the same trick, and it is not a bigger enumeration.