Generator

A tableau for (p → q) → (¬q → ¬p)

A generator in the logic library, called 65 times across 13 essays. Below: what it draws with nothing chosen and at each mode an essay asks for, what it checks while drawing, and everywhere it is used.

tree is one function. Everything below came out of it during this build, at parameters taken from the essays rather than invented for this page — so a figure here is the same figure a reader meets in an essay, and if the generator changes, this page changes with it.

With nothing chosen

A tableau for (p → q) → (¬q → ¬p). A branching tree of formulas, each branch ending in a contradiction or in a description of a counterexample.

Tseitin's clauses on the complete graph on four vertices

The parity demands of the complete graph on four vertices as a matrix

A violated vertex that can be moved and never removed, on the cube

The smallest failed search for Tseitin's clauses

A failed search on four clauses, read as a resolution refutation

What it checks while it draws

Collected by running the family and recording what it asserted, not written here. The count is how many separate times the claim was put to the test while these drawings were made.

the term for x1 written out has 2^(k+1) − 1 symbols ×10
the chain on 2 variables is refuted by a search of 5 nodes ×6
the clauses for 2 pigeons in 1 holes ×6
at 1 instances there is still a model, so the search has not finished ×5
the assumption h2 is open where it is discharged ×3
at 1 instances there is still a model ×2
the assumption h1 is discharged somewhere below it ×2
the variable h1 is bound where it is used ×2
a conjunction is introduced from two derivations ×1
a conjunction is taken apart from one derivation ×1
a disjunction is introduced from one derivation ×1
a disjunction is used by considering both halves ×1
A implies B on every assignment ×1
A implies the interpolant ×1
a longer cycle needs a larger search ×1
a negation is introduced from a derivation and its denial ×1
a path of two to five vertices starting at the charged one ×1
a term starts with a name ×1
a variable shares a component with its negation exactly when no assignment works ×1
a vertex of degree d contributes 2^(d−1) clauses ×1
an assumption has nothing above it ×1
an implication is introduced from one derivation ×1
an introduced implication is an implication ×1
and both cases reach the same conclusion ×1
and every assumption it made has been discharged ×1
and it is discharged as (p -> q) & (q -> r) ×1
and it is discharged as p ×1
and it is discharged as p -> p ×1
and it is discharged as p & (q | r) ×1
and it is discharged as q ×1
and it is discharged as r ×1
and it is the conjunction of what they derived ×1
and its antecedent is the discharged assumption ×1
and its argument has the antecedent's type ×1
and its consequent is what was derived ×1
and once it closes it stays closed ×1
and the count of models is positive at every stage drawn ×1
and the drop is sharper for more variables ×1
and the formula it proves is true in every row of its table ×1
and the goal follows from the lemma ×1
and the goal is true in every row of its table ×1
and the interpolant implies B ×1
and the lemma the other proof uses is not a subformula of the goal ×1
and the named half is the conclusion ×1
and the named half is what was derived ×1
and the negated assumption is the conclusion ×1
and the second is its antecedent ×1
and the sweep contains both kinds ×1
arguments close with a bracket ×1
between two and seven stages ×1
both cases have the same type ×1
cases are taken on a disjunction ×1
consecutive path vertices are joined by an edge ×1
each arrow along the chain resolves with the clause built so far ×1
each extra hole multiplies the search by more than the last one did ×1
each substitution adds one symbol and removes no variable ×1
every assignment violates an odd number of vertices ×1
every column of the incidence matrix has two ones, so the rows add to zero ×1
every drawn step is the resolvent of the two clauses above it ×1
every formula in the cut-free proof is a subformula of the goal, or its negation ×1
every formula of the derivation with no detour is a subformula of the goal ×1
every label is falsified by the assignments on its own path ×1
every leaf of the formula is a variable ×1
every level has a node that reaches the bottom ×1
every literal names a variable of the clause set ×1
every literal names a variable of the set ×1
every opening bracket in the formula is closed ×1
every order of the six variables ×1
flipping an edge moves the violation to its other end ×1
it closes exactly when the universal has been used 3 times ×1
modus ponens takes two derivations ×1
no arrow leads from a true literal to a false one ×1
no assignment satisfies every vertex ×1
no fixed order beats the best search that chooses afresh at each node ×1
no label is a tautology ×1
no node has more children than the branching factor ×1
no variable shares a component with its negation ×1
only a disjunction is taken apart by cases ×1
only a pair is projected ×1
only a term of implication type is applied ×1
removing a detour leaves the proved formula unchanged ×1
resolution and the truth table agree on every one of the sets ×1
resolution reaches the empty clause exactly when no assignment satisfies the set ×1
resolution refutes A together with the negation of B ×1
shared as a graph it has k + 1 distinct nodes ×1
so the conclusion is its consequent ×1
so the count of unsatisfiable sets and the count of refuted sets are one number ×1
the algorithm refuses x = f(x) by the occurs check ×1
the assignment satisfies every clause ×1
the assumption f is discharged somewhere below it ×1
the assumption x is discharged somewhere below it ×1
the assumption y is discharged somewhere below it ×1
the branching factor is a whole number between 2 and 3 ×1
the case assumption h2 is open ×1
the chain from x to y ends in the clause ¬x ∨ y ×1
the chain length is a whole number between 4 and 12 ×1
the charges add to one ×1
the clashing literals unify ×1
the clause set is one the arrow views know ×1
the clause set is one the family knows ×1
the conclusion of →I is an implication ×1
the conclusion of ¬I is a negation ×1
the conclusion of ∨I is a disjunction ×1
the cut-free proof closes, so the formula is a theorem ×1
the depth drawn is a whole number between 3 and 7 ×1
the derivation ends at its goal ×1
the derivation ends at the stated goal ×1
the derivation had at least one detour to remove ×1
the derivation is one of contraposition, transitivity, distribute ×1
the derivation is one of contraposition, transitivity, distribute, identity, swap ×1
the derivation is one of identity, swap ×1
the derivation uses only implication, conjunction and disjunction, where every step has a term ×1
the derivation's term has the goal as its type ×1
the expansion does close, at some stage this figure reaches ×1
the first derivation gives a disjunction ×1
the first is an implication ×1
the first resolvent keeps one variable ×1
the formula and its disjunctive normal form agree on every row ×1
the formula has between one and five variables ×1
the formula is a non-empty string ×1
the graph is one the family knows ×1
the graph is small enough to check every assignment ×1
the interpolant uses only atoms the two formulas share ×1
the last term contains no detour ×1
the lemma is itself a theorem, so it may be cut in ×1
the literals resolved have opposite signs ×1
the most holes is a whole number between 3 and 6 ×1
the pair is one the family knows ×1
the path passes through one node per level ×1
the propagating search only runs on unsatisfiable sets ×1
the pruning parameter is a whole number between 2 and 9 ×1
the question is one of reaches, never ×1
the reduction finishes within a dozen steps ×1
the root's label is the empty clause ×1
the rounds drawn is a whole number between 2 and 5 ×1
the search only runs on unsatisfiable sets ×1
the second resolvent is the empty clause ×1
the set has a variable in its negation's component ×1
the sets with a variable in its negation's component are the unsatisfiable ones ×1
the short form agrees with the extracted interpolant on every shared assignment ×1
the smallest unsatisfiable set of two-literal clauses needs four of them ×1
the specific substitution is also a unifier ×1
the specific unifier factors through the most general one ×1
the strongest interpolant implies the one read off the refutation ×1
the substitution found makes the two terms identical ×1
the sweep is over three variables ×1
the table has one row per assignment ×1
the tableau and the truth table reach the same verdict ×1
the tableau stays small enough to draw ×1
the tableau tests validity or satisfiability ×1
the term's type at this node is the formula the derivation has there ×1
the tree drawn actually reaches the bottom row ×1
the trials per point is a whole number between 20 and 400 ×1
the truth table, resolution and the components agree on every set ×1
the two derivations are a formula and its denial ×1
the two formulas share at least one atom ×1
the two formulas use at most six atoms between them ×1
the two unit clauses resolve to the empty clause ×1
the variable f is bound where it is used ×1
the variable h is bound where it is used ×1
the variable k is bound where it is used ×1
the variable x is bound where it is used ×1
the variable y is bound where it is used ×1
the view is one the family draws ×1
the walk always has a surviving child to step to ×1
the whole formula is consumed by the parser ×1
the whole string is one term ×1
the whole term is closed, because every assumption was discharged ×1
there are twelve two-literal clauses on three variables ×1
this pair unifies ×1
this view draws a refutation, so the set has to be unsatisfiable ×1
two to four numbers of variables from 10 to 2000 ×1
unification finishes ×1
which derived a conjunction ×1
which implies the weakest ×1
with every edge false only the charged vertex is violated ×1
with few clauses nearly every random set can be satisfied ×1
with half as many clauses again as variables, the largest sets almost never can ×1
x is still there after every round ×1

Where it is called

Every figure on this list is drawn by the same rule, so a change to the rule changes all of them at once. That is why the list is published.

Logic

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

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

A lemma, and the proof that never mentions one

Proving something by first proving a lemma is what makes mathematics readable, and it is exactly what makes a proof system impossible to search — because the lemma can be any formula at all. Gentzen proved the step can always be removed, and the removal is not free.

Logic

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

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

Every derivation is a term

Write a variable for each assumption, an abstraction where one is discharged, and an application where an implication is used, and a natural-deduction derivation becomes a term. The formula it proves is the term's type, and checking the one is checking the other. A detour in the proof — a lemma introduced and at once used — is a term that simplifies, and simplifying it is removing the detour.

Logic

The assumption a proof pays back

A tableau assumes the opposite once and takes it apart. Natural deduction assumes things freely, uses them, and then withdraws them — and the withdrawal is what turns a derivation of a consequence into a proof of an implication.

Logic

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

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

The sentence that says it has no proof

Number every sentence and every proof, and a formal system can talk about itself. Then the diagonal is available one more time, and what it builds is a sentence that is true exactly when it is unprovable.

Logic

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

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

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.

The whole library · What the figures prove