Matpic
mathematics, in pictures
Concept

Satisfiability

The property of a formula for which some assignment of values makes it true. Deciding it for a formula in many variables is the model hard search problem, since the assignments to try double with each variable.

Named by 12 essays across one field — each of them below, with the objects they name alongside it.

(p ∨ q) ∧ ¬r, drawn on the cube of 8 assignments. The assignments as corners of a cube, joined when they differ in one variable, with the satisfying corners filled.

A formula is a corner of a cube

A formula about three letters is a set of eight rows. Written as a table that is a list; drawn on a cube it is a shape — and the shape is what almost every later question in this field turns out to be about.

logic · Truth functions A tableau for ((p → q) ∧ (q → r)) → (p → r). A branching tree of formulas, each branch ending in a contradiction or in a description of a counterexample.

The tree that closes

To prove a formula, assume it false and take it apart. Every branch ends in a contradiction, or one of them describes exactly how it could have been false — and either way the tree is the answer, drawn.

logic · Proof systems A tree branching at most 3 ways, to depth 4, and the path through it. A tree drawn level by level, with the nodes that die out faint and a highlighted path that always steps to a node with descendants at the bottom.

An infinite tree has an infinite path

A tree that goes on forever, in which every node has only finitely many children, must contain a single branch that goes on forever. The proof is a rule for walking, and the rule is the whole of why finite information can decide an infinite question.

logic · Models A resolution refutation of four clauses on three variables. A derivation tree: the given clauses at the top, each later clause obtained by cancelling one variable between two clauses above it, ending in the empty clause.

A proof with one rule

Two clauses that disagree about exactly one variable can be combined into a third that forgets it; repeat, and if the clauses cannot all be true the empty clause eventually appears — a complete proof system with a single move.

logic · Resolution Closed after 3 uses of the universal. The Herbrand expansion of a first-order question at 5 stages, with the number of remaining models at each. It reaches nought after 3 instantiations.

The instance that has to be guessed

Every rule of a propositional tableau replaces a formula by shorter ones, which is why it stops. The rule for a universal claim does not replace it — it keeps it and adds an instance — and one word changing turns a decision procedure into a search that may run forever.

logic · Proof systems A implies B, and r ∨ s sits between them. A = ((p ∨ q) ∧ (p → r)) ∧ (q → s) implies B = (r ∨ s) ∨ t. A resolution refutation of A with the negation of B yields the interpolant r ∨ s. It uses only the shared atoms r, s, follows from A and implies B, and lies between the strongest and weakest interpolants.

The sentence between a premise and its consequence

When one formula implies another, something sits between them written only in the words the two have in common: a sentence the first implies and that implies the second. A refutation of the first together with the denial of the second hands such a sentence over, and every possible one lies between a strongest and a weakest that can be computed outright.

logic · Proof systems 5 two-literal clauses drawn as 10 arrows. The literals of four variables arranged in a circle with an arrow for each implication a two-literal clause contains, the arrows forming a path from one literal to its negation and back highlighted, beside the list of clauses and their arrows.

Two literals make an arrow

A clause of two literals, p ∨ q, says that if p is false then q is true, and if q is false then p is true — two arrows. A set of such clauses is a directed graph on the literals, and it is unsatisfiable exactly when some variable and its negation reach each other. Each of those two paths is a chain of resolution steps, and finding them takes time proportional to the size of the input.

logic · Resolution A failed search on four clauses, read as a resolution refutation. A binary search tree branching on variables, each branch ending at a clause the partial assignment makes false, with every branch point labelled by the resolvent of the clauses below it, the top label being the empty clause.

A failed search is a proof

Search for an assignment by branching on variables and backing up whenever a clause turns false. If every branch fails, the tree the search leaves behind is itself a resolution refutation: write at each branch point the resolvent of the clauses below it, and the top of the tree is the empty clause. So every limit on short refutations is a limit on every such search — and the pigeonhole clauses, whose refutations are long, defeat them all.

logic · Resolution A smallest model of ∀x (Ax → ∃y (By ∧ ¬Cy)) ∧ ∃x (Ax ∧ Cx) ∧ ∀x (Bx → ¬Ax). Three overlapping circles with some regions shaded as empty and a single dot in each occupied region, forming a model of a sentence of monadic first-order logic.

One thing in each region is enough

Give first-order logic its full apparatus of nested quantifiers but only one-place predicates, and every question about truth is still settled by the regions of a diagram. A predicate cannot tell apart two things in the same region, so no model ever needs more than one thing per region — and with three predicates there are only 255 models to try.

logic · Class diagrams Carroll's babies and crocodiles, on four ellipses. Four overlapping ellipses labelled with the four classes of a sorites, the regions emptied by its premises shaded, and the regions its conclusion requires to be empty outlined.

The conclusion is what survives the erasing

Lewis Carroll's puzzles give three premises about four classes — babies, logical people, the despised, crocodile-managers — and ask what follows. Draw all four, shade what the premises rule out, then erase the classes the conclusion is not about: a region survives as empty only if everything above it was. What is left is the conclusion, and erasing a class turns out to be exactly one step of resolution.

logic · Class diagrams Tseitin's clauses on the cube. the cube with a variable on each edge and a charge of 0 or 1 at each vertex, exactly one vertex charged 1. The parity demands give 32 clauses that cannot all be true.

A contradiction that is only a sum

Put a variable on every edge of a graph and ask each vertex for an odd or an even number of true edges, with the demands adding up to odd. Add all the demands and every edge is counted twice, so the left side is zero and the right side is one: the contradiction is a single sum. Resolution cannot add. It has to reach the same conclusion clause by clause, and on a graph where every group of vertices has many edges leaving it, that takes exponentially long.

logic · Resolution Unifying f(x, g(x)) with f(h(y), g(z)). Three term trees: f(x, g(x)), f(h(y), g(z)), and their common instance f(h(y), g(h(y))) under the most general unifier x ↦ h(y), z ↦ h(y).

Two terms made equal, and no more

Resolution with variables needs two literals to clash, and they clash only after something has been substituted for their variables. There are infinitely many substitutions that would do. One of them is the most general — every other is it followed by something more — and an algorithm of four rewriting rules finds it or proves there is none. That single computation turns the search for instances from guessing into arithmetic.

logic · Resolution

Named alongside it

The objects these essays reach for when they reach for this one.

Proof systemRefutationResolutionExhaustive searchCompletenessComplexityDecision procedureLiteralNormal formQuantifierImplicationSoundness

All concepts