Logic — page 4

A walk that beats trying everything

To decide whether clauses of three letters can all be satisfied, the obvious method tries all 2ⁿ assignments. Uwe Schöning's method, from 1999, starts at a random assignment and wanders: pick a clause that is false, flip one of its letters at random, and repeat three times as many times as there are letters. A single try usually fails, but it succeeds with chance at least about (3/4)ⁿ, so about (4/3)ⁿ tries are enough — and the reason is a walk on a line that goes the wrong way two times in three.

The squares that answer every request

Rado's graph has, for any finite sets U and V, a vertex joined to all of U and none of V. A finite graph can only answer the small requests, and the Paley graphs — residues modulo a prime, joined when their difference is a square — are the classic way to build one. Checking every request exactly finds the thresholds: 13 residues answer every request of two, 29 every request of three, 89 every request of four. The theorem that guarantees it asks for 64, 576 and 4,096. Coin-toss graphs of the same sizes almost never manage it.

A letter the clauses already decide

Set the letters of a formula one at a time, in a random order, and guess each one with a coin — unless some clause has already had its other two letters set to false, in which case the clause decides. A try succeeds when every guess is right, so what matters is how many letters get guessed. On a formula with one solution, every letter has a clause that forces it in at least one order out of three, so at most two thirds of the letters are guessed on average, and about 1.587ⁿ tries suffice. It is slower than the random walk. Refined, it is the fastest method known.

The formula that cannot share

A circuit computes the parity of n letters with a chain of n − 1 exclusive-or gates. A formula in and, or and not, which may use each result only once, needs n² letters at least — a bound Khrapchenko proved by counting the cube's edges between true and false — and exhaustive search over every formula of four letters finds parity sitting exactly on it.

The machines that need a reason never to stop

Run every three-state machine on a blank tape and the ones that halt announce themselves: the longest stops after 21 steps. The work is in the others. Each needs a reason it will never stop, and four simple kinds of reason settle all but 27 of them — machines that sweep back and forth over a growing tape and defeat every check that looks for a repeat.

Dominoes that no algorithm can match

Emil Post's puzzle has no machines and no programs in it: a handful of dominoes, each with a string on top and a string underneath, and the question whether some row of them, repeats allowed, spells the same word along both edges. No algorithm can answer it for every set of dominoes, because a set can be built whose only matches are a machine's run written out twice, one step out of phase — and three dominoes with strings of three characters already need thirty-six in a row before the edges agree.

The zigzags a formula can draw

Let truth be any number from 0 to 1, and Łukasiewicz's connectives turn every formula in one variable into a graph. Every graph that appears is a zigzag of straight pieces with whole-number slopes, ending at 0 or 1 — and McNaughton proved in 1951 that every such zigzag appears. A logic of degrees of truth turns out to be a theory of piecewise-linear functions with integer coefficients.

A contradiction that stays where it is

In classical logic one contradiction proves everything: from p and not-p, any q at all. Add a third truth value — both true and false — and count it as holding, and the explosion stops. The classical laws all survive as laws; what goes is exactly the reasoning that carries a contradiction somewhere it was not. Run the other way, the same three tables make a logic of gaps instead of gluts.

The choice inside a countable union

A countable union of countable sets is countable: list each set, then walk the grid of all their members along its diagonals. The proof is two lines and every student meets it early. It also makes infinitely many arbitrary choices at once — one listing for each set — and without the axiom of choice the theorem can fail: there are consistent worlds in which the real numbers are a countable union of countable sets, and worlds in which countably many pairs of socks cannot be counted.

A spanning tree for every graph

Every connected graph has a spanning tree: a set of its edges that joins every point and closes no loop. For a finite graph the proof is a greedy pass over the edges. For an infinite graph the greedy pass has to keep going past the end of every list, and the statement turns out to be exactly as strong as the axiom of choice — Zorn's lemma supplies the tree, and the existence of spanning trees in every graph gives back the whole axiom.

What a proof about numbers can compute

The proofs of (o → o) → o → o without detours are the whole numbers, one for each count of how often the assumption is used. A proof of the implication from that formula to itself therefore takes a number and returns one, and removing its detours computes the answer. Enumerating all 14,659 such proofs up to size 16 finds 299 different functions — sums, products, squares, cubes, tests on zero — and not one of them subtracts. The predecessor, n − 1, is not among them, and a single line about polynomials says it never will be.

One type up

A numeral is an iterator, and the formula it proves fixes what it may iterate. At the lowest type it can only repeat the successor, and every function it computes is a polynomial — no predecessor. Let the same numeral iterate a function on functions and 2ⁿ appears; let it iterate a function that takes a function and returns a value, and the predecessor appears at size 15; let it iterate a pair of values, and the predecessor, halving and parity all arrive at size 16. The trick is Kleene's, from 1932, and an exhaustive search finds it without being told.

What a formula keeps when letters are fixed

Fix half the letters of a formula at random and most of its leaves become irrelevant: on the sixteen-leaf formula for the parity of four letters, two fixings leave four. How fast formulas shrink under random fixings is the whole engine behind the best lower bounds anyone has proved for formula size — Subbotovskaya's 3/2 in 1961, Håstad's 2 in 1998 — and the reason that engine stops at n³.

Three models and never two

Take the theory of a dense order and add constants c₀ < c₁ < c₂ < … running upward for ever. The theory is complete — it decides every sentence — and yet it has exactly three countable models, told apart only by what lies above all the constants: nothing, a least point, or a gap with no least point. Vaught proved in 1961 that no complete theory has exactly two, and the proof builds this theory's third model out of its other two.

Resolving one letter away at a time

Davis and Putnam's procedure of 1960 decides a set of clauses by removing its letters one at a time, replacing every clause that mentions a letter by all the ways of resolving it away. On a cycle the clauses never multiply; on a grid they swell by a factor of three and a half for each extra row, and on the 4 × 4 grid each extra unit of the order's width doubles the peak exactly. The cost is not the size of the formula but how wide it is.

One block of quantifiers, read off an algebra

Which properties of words can be stated with existential quantifiers alone — 'there are positions, in this order, carrying these letters' — and Boolean combinations of such statements? Imre Simon answered in 1975: exactly those whose syntactic monoid is J-trivial. Of the 57,068 languages that automata of up to four states recognise, 848 pass the test, and every one of them is decided by which words of length three or less it contains as scattered subwords.

The order that keeps elimination narrow

Eliminating letters one at a time costs whatever the widest step costs, and the least width any order can achieve is the treewidth of the formula's graph. Finding it exactly is NP-hard, but a search over sets of letters instead of sequences finds it for small graphs, and a greedy rule that adds the fewest new edges finds it on 566 of 600 random graphs and misses by more than one only once. On Tseitin's 6 × 6 grid that rule forms twenty-four times fewer resolvents than sweeping row by row. What it cannot do is prove that its order is the best.

No way to hand out true and false

Birkhoff and von Neumann read the propositions of quantum mechanics as subspaces, with "and" the intersection and "or" the span. Three lines in a plane already break the distributive law. Kochen and Specker proved something stronger: the propositions cannot be called true and false at all, if every complete measurement is to have exactly one true outcome. Cabello's eighteen directions in four dimensions show why in one line of arithmetic — nine bases, each direction in two of them, and nine is odd — and a search of all 262,144 assignments confirms it.

Five axioms and fifteen logics

Five familiar axioms of modal logic can be added to the basic system in thirty-two combinations. Only fifteen different logics come out, because the axioms are properties of arrows between worlds and some properties force others. Checking every frame with up to four worlds finds the fifteen, the order among them, and the small pictures that tell each from its neighbours.

Truth tables up to renaming

There are 256 truth functions of three letters, but many differ only in which letter is called what, or whether a letter or the answer is negated. Counted up to such renamings there are fourteen. For four letters there are 222, for five 616,126 — and almost every function of many letters is changed by every renaming, so the count settles into a simple division.

Thirty-one directions nobody can label

In four dimensions eighteen directions are enough to show that quantum measurements cannot have answers waiting in advance, and a parity count does it in a line. In three dimensions, where Kochen and Specker first proved it, no parity count works and the smallest known set has thirty-one directions. Peres's thirty-three can be checked by hand; Conway and Kochen's thirty-one fall out of a search through every direction with coordinates between −2 and 2; and whether thirty or fewer could ever do is still being settled by exhaustive computation, which has so far ruled out everything up to twenty-four.

One type for every use

In the simply typed calculus a numeral must be told in advance what kind of thing it will iterate, and with input and output of one type it computes only polynomials with tests. Let a single type stand for every type — a numeral is then a term of type ∀X. (X → X) → X → X, used at whatever type each occasion needs — and the same few symbols compute subtraction, exponentials and Ackermann's function, which grows faster than anything built from primitive recursion. Every run still finishes, and the proof that it does lies just beyond the reach of second-order arithmetic.

The second letter breaks the pattern

In one letter the constructive logic has infinitely many formulas, but they climb in a column two wide, four new ones for every step a state of knowledge can take. Add a second letter and the pattern is gone: sixteen formulas at the last step, 265,454 one step back, and more than two to the power 265,428 one step further. Every one of those is a genuine formula, and the reason the two-letter lattice has never been drawn is that each layer of the model is about as large as the number of formulas the layer above can tell apart.

The sizes at which a sentence can come true

Write a sentence about a relation and ask for which numbers of points some relation makes it true. "Every two points have exactly one common neighbour" comes true at every odd size and no even one, and every graph that satisfies it is a windmill of triangles. "Every two players are both beaten by some third" fails for every tournament of two to six players and holds from seven on. A search can settle one size at a time; only a proof settles all of them, and the two sentences need different kinds.